Using monterey phoenix to formalize and verify system architectures
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 develop...
Saved in:
| Main Authors: | , , , , |
|---|---|
| 格式: | text |
| 語言: | English |
| 出版: |
Institutional Knowledge at Singapore Management University
2012
|
| 主題: | |
| 在線閱讀: | https://ink.library.smu.edu.sg/sis_research/5014 https://ink.library.smu.edu.sg/context/sis_research/article/6017/viewcontent/APSEC_2012.pdf |
| 標簽: |
添加標簽
沒有標簽, 成為第一個標記此記錄!
|
| 機構: | Singapore Management University |
| 語言: | English |
| id |
sg-smu-ink.sis_research-6017 |
|---|---|
| record_format |
dspace |
| spelling |
sg-smu-ink.sis_research-60172020-03-12T09:08:57Z Using monterey phoenix to formalize and verify system architectures ZHANG, Jiexin LIU, Yang AUGUSTON, Mikhail SUN, Jun DONG, Jin Song 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. 2012-07-12T07:00:00Z text application/pdf https://ink.library.smu.edu.sg/sis_research/5014 info:doi/10.1109/APSEC.2012.60 https://ink.library.smu.edu.sg/context/sis_research/article/6017/viewcontent/APSEC_2012.pdf http://creativecommons.org/licenses/by-nc-nd/4.0/ Research Collection School Of Computing and Information Systems eng Institutional Knowledge at Singapore Management University Programming Languages and Compilers Software Engineering |
| institution |
Singapore Management University |
| building |
SMU Libraries |
| continent |
Asia |
| country |
Singapore Singapore |
| content_provider |
SMU Libraries |
| collection |
InK@SMU |
| language |
English |
| topic |
Programming Languages and Compilers Software Engineering |
| spellingShingle |
Programming Languages and Compilers Software Engineering ZHANG, Jiexin LIU, Yang AUGUSTON, Mikhail SUN, Jun DONG, Jin Song Using monterey phoenix to formalize and verify system architectures |
| description |
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. |
| format |
text |
| author |
ZHANG, Jiexin LIU, Yang AUGUSTON, Mikhail SUN, Jun DONG, Jin Song |
| author_facet |
ZHANG, Jiexin LIU, Yang AUGUSTON, Mikhail SUN, Jun DONG, Jin Song |
| author_sort |
ZHANG, Jiexin |
| title |
Using monterey phoenix to formalize and verify system architectures |
| title_short |
Using monterey phoenix to formalize and verify system architectures |
| title_full |
Using monterey phoenix to formalize and verify system architectures |
| title_fullStr |
Using monterey phoenix to formalize and verify system architectures |
| title_full_unstemmed |
Using monterey phoenix to formalize and verify system architectures |
| title_sort |
using monterey phoenix to formalize and verify system architectures |
| publisher |
Institutional Knowledge at Singapore Management University |
| publishDate |
2012 |
| url |
https://ink.library.smu.edu.sg/sis_research/5014 https://ink.library.smu.edu.sg/context/sis_research/article/6017/viewcontent/APSEC_2012.pdf |
| _version_ |
1770575189918089216 |