Writing and verifying interoperability requirements: Application to collaborative processes

Interoperability analysis is highly correlated with interoperability requirements, the ability to grasp, structure, author and verify such requirements has become fundamental to the analytical process. To this end, requirements must be: (1) properly submitted in a suitable and usable repository; (2) written correctly by stakeholders with relevance to the studied domain; and (3) as easily verifiable as possible on various models of the system for which interoperability capabilities are being requested. The purpose of this article is to present both a structured repository for interoperability requirements and a Domain Specific Language to write and verify interoperability requirements - within a collaborative process model - using formal verification techniques. The interoperability requirements repository, which serves to structure interoperability requirements and make them available, is itself structured through abstraction levels, views and interoperability life cycle dimensions. Additional parameters detailing the requested information and the known impacts of requirements on behavior of the studied system have also been included. The Domain Specific Language provides the means for writing interoperability requirements. Afterwards, these requirements − more specifically the temporal requirements − are re-written into properties by transforming the temporal logic TCTL to allow for their effective verification by using the model checker UPPAAL. The overall approach is illustrated in a case study based on a collaborative drug circulation process. The article also draws conclusions and offers an outlook for future research and application efforts