Title :
Using Monterey Phoenix to Formalize and Verify System Architectures
Author :
Jiexin Zhang ; Yang Liu ; Auguston, M. ; Jun Sun ; Jin Song Dong
Author_Institution :
Sch. of Comput., Nat. Univ. of Singapore, Singapore, Singapore
Abstract :
Modeling and analyzing software architectures are useful for helping to understand the system structures and facilitate proper implementation of user requirements. Despite its importance in the software engineering practice, the lack of formal description and verification support hinders the development of quality architectural models. In this work, we develop an approach for modeling and verifying software architectures specified using Monterey Phoenix (MP) architecture description language. Firstly, we formalize the syntax and operational semantics for MP. This language is capable of modeling system and environment behaviors based on event traces, as well as supporting different architecture composition operations and views. Secondly, a dedicated model checker for MP is developed based on PAT verification framework. Finally, several case studies are presented to evaluate the usability and effectiveness of our approach.
Keywords :
formal verification; programming language semantics; software architecture; specification languages; MP architecture description language; MP operational semantics; MP syntax formalization; PAT verification framework; architecture composition operations; model checker; monterey phoenix architecture description language; system architecture formalization; system architecture verification; Computer architecture; Connectors; Grammar; Object oriented modeling; Semantics; Software architecture; Syntactics;
Conference_Titel :
Software Engineering Conference (APSEC), 2012 19th Asia-Pacific
Conference_Location :
Hong Kong
Print_ISBN :
978-1-4673-4930-7
DOI :
10.1109/APSEC.2012.60