Please use this identifier to cite or link to this item:
Title: Using monterey phoenix to formalize and verify system architectures
Authors: Zhang, Jiexin
Liu, Yang
Auguston, Mikhail
Sun, Jun
Dong, Jin Song
Issue Date: 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.
DOI: 10.1109/APSEC.2012.60
Fulltext Permission: none
Fulltext Availability: No Fulltext
Appears in Collections:SCSE Conference Papers

Citations 20

Updated on Jul 13, 2020

Citations 20

Updated on Mar 10, 2021

Page view(s) 10

Updated on Jul 3, 2022

Google ScholarTM




Items in DR-NTU are protected by copyright, with all rights reserved, unless otherwise indicated.