Publication Type
Conference Proceeding Article
Version
publishedVersion
Publication Date
7-2012
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.
Discipline
Programming Languages and Compilers | Software Engineering
Research Areas
Software and Cyber-Physical Systems
Publication
Proceedings of the 19th Asia-Pacific Software Engineering Conference, APSEC 2012, Hong Kong, China, December 4-7
First Page
644
Last Page
653
Identifier
10.1109/APSEC.2012.60
Publisher
IEEE
City or Country
China
Citation
ZHANG, Jiexin; LIU, Yang; AUGUSTON, Mikhail; SUN, Jun; and DONG, Jin Song.
Using monterey phoenix to formalize and verify system architectures. (2012). Proceedings of the 19th Asia-Pacific Software Engineering Conference, APSEC 2012, Hong Kong, China, December 4-7. 644-653.
Available at: https://ink.library.smu.edu.sg/sis_research/5014
Creative Commons License
This work is licensed under a Creative Commons Attribution-NonCommercial-No Derivative Works 4.0 International License.
Additional URL
https://doi.org/10.1109/APSEC.2012.60