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 cor-rect by construction. This is the case with process algebraic architectural description languages, which are process calculi enhanced with the main ar-chitectural concepts. However, the techniques with which those languages have been equipped are mainly conceived to work with synchronous commu-nications only. The objective of this paper is threefold. On the modeling side, we show how to enhance the expressiveness of a typical process alge-braic architectural description language by including the capability of rep-resenting 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. Key words: software architecture, architectural description languages, process algebra, synchronous and nonsynchronous communications, system modeling and verification, code generation. Preprint submitted to Journal of Systems and Software February 19, 2010 1