Paper Info
Title
Formalizing and verifying stochastic system architectures using Monterey Phoenix.
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
Year
DOI
Venue
2016
10.1007/s10270-014-0411-7
Software and Systems Modeling (SoSyM)
Keywords
Field
DocType
Model checking, Stochastic system architecture, Monterey Phoenix
Operational semantics,Architecture,Programming language,Model checking,Computer science,Theoretical computer science,Software,Software architecture,User requirements document,Architecture description language,Formal verification
Journal
Volume
Issue
ISSN
15
2
1619-1374
Citations 
PageRank 
References 
2
0.57
21
Authors
7
Name
Order
Citations
PageRank
Songzheng Song1787.62
Jiexin Zhang2284.70
Yang Liu32194188.81
Mikhail Auguston427335.20
Jun Sun51407120.35
Jin Song Dong61369107.12
Tieming Chen7295.11