Handling communications in process algebraic architectural description languages: Modeling, verification, and implementation

摘要

Architectural description languages are a useful tool for modeling complex software systems at a high level of abstraction. If based on formal methods, they can also serve for enabling the early verification of various properties such as component coordination and for guiding the synthesis of code correct by construction. This is the case with process algebraic architectural description languages, which are process calculi enhanced with the main architectural concepts. However, the techniques with which those languages have been equipped are mainly conceived to work with synchronous communications only. The objective of this paper is threefold. On the modeling side, we show how to enhance the expressiveness of a typical process algebraic architectural description language by including the capability of representing nonsynchronous communications in such a way that the usability of the original language is preserved. On the verification side, we show how to modify techniques for analyzing the absence of coordination mismatches like the compatibility check for acyclic topologies and the interoperability check for cyclic topologies in such a way that those checks are valid also for nonsynchronous communications. On the implementation side, we show how to generate multithreaded object-oriented software in the presence of synchronous and nonsynchronous communications in such a way that the properties proved at the architectural level are preserved at the code level.