Publication Type
Journal Article
Version
publishedVersion
Publication Date
1-2016
Abstract
The analysis of software architecture plays an important role in understanding 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 in this domain hinders the development of quality architectural models. To tackle this problem, in this work, we develop an approach for modeling and verifying software architectures specified using Monterey Phoenix (MP) architecture description language. MP is capable of modeling system and environment behaviors based on event traces, as well as supporting different architecture composition operations and views. First, we formalize the syntax and operational semantics for MP; therefore, formal verification of MP models is feasible. Second, we extend MP to support shared variables and stochastic characteristics, which not only increases the expressiveness of MP, but also widens the properties MP can check, such as quantitative requirements. Third, a dedicated model checker for MP has been implemented, so that automatic verification of MP models is supported. Finally, several experiments are conducted to evaluate the applicability and efficiency of our approach.
Discipline
Software Engineering | Systems Architecture
Research Areas
Software and Cyber-Physical Systems
Publication
Software and Systems Modeling
Volume
15
Issue
2
First Page
453
Last Page
471
ISSN
1619-1366
Identifier
10.1007/s10270-014-0411-7
Publisher
Springer Verlag (Germany)
Citation
SONG, Songzheng; ZHANG, Jiexin; LIU, Yang; AUGUSTON, Mikhail; SUN, Jun; DONG, Jin Song; and CHEN, Tieming.
Formalizing and verifying stochastic system architectures using Monterey Phoenix. (2016). Software and Systems Modeling. 15, (2), 453-471.
Available at: https://ink.library.smu.edu.sg/sis_research/4970
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.1007/s10270-014-0411-7