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

Architectural description languages are a useful tool for modeling complex 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 ab...

• Type: Journal
• Year: 2010
• Where: JSS
• Authors: Marco Bernardo, Edoardo Bontà, Alessandro Aldini
• Keywords: Algebraic Architectural Description, Architectural Description Languages, JSS 2010, Nonsynchronous Communications