Using Monterey Phoenix to Formalize and Verify System Architectures
Dong, Jin Song
MetadataShow full item record
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.
19th Asia-Pacific Software Engineering Conference APSEC 2012, December 4 – 7, 2012, Hong Kong
RightsThis publication is a work of the U.S. Government as defined in Title 17, United States Code, Section 101. Copyright protection is not available for this work in the United States.
Showing items related by title, author, creator and subject.
Kunde, Dietmar; Darken, Christian J. (2005);Nearly all armies of the Western Hemisphere use modeling and simulation tools as an essential part for analysis and training their leaders and war fighters. Tremendous resources have been applied to increase the level of ...
Phillips, Donovan D. (Monterey, California. Naval Postgraduate School, 1998);Mathematical modeling forms a bridge between the study of mathematics and the application of mathematics with the intent of explaining or predicting real world behavior. In their book A First Course in Mathematical Modeling, ...
Michael, Sarah F. (Monterey, California. Naval Postgraduate School, 2011);Carbon nanotube field ionization technology has the potential to make ion propulsion feasible for use in micro and nano-satellites. To better understand the phenomenon and optimize the ion thruster design, it is useful to ...