Publication Type
Conference Proceeding Article
Version
publishedVersion
Publication Date
10-2012
Abstract
Software Architecture plays an essential role in the high level description of a system design. 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 paper, we present an automated approach to the modeling and verification of software architecture designs using the Process Analysis Toolkit (PAT). We present the formal syntax of the Wright# architecture description language together with its operational semantics in Labeled Transition System (LTS). A dedicated model checking module for Wright# is implemented in the PAT verification framework based on the proposed formalism. The module - ADL supports verification and simulation of software architecture models in PAT. We advance our work via defining an architecture style library that embodies commonly used architecture patterns to facilitate the modeling process. Finally, a case study of the Teleservices and Remote Medical Care System (TRMCS) modeling and verification is presented to evaluate the effectiveness and scalability of our approach.
Keywords
Software Architecture, Formal Verification, Model Checking, Wright, PAT
Discipline
Software Engineering | Systems Architecture
Research Areas
Software and Cyber-Physical Systems
Publication
Proceedings of the 14th International Symposium on High-Assurance Systems Engineering, Omaha, NE, USA, 2012 October 25-27
First Page
193
Last Page
200
ISBN
9780769549125
Identifier
10.1109/HASE.2012.12
Publisher
IEEE
City or Country
Omaha, NE, USA
Citation
ZHANG, Jiexin; LIU, Yang; SUN, Jing; DONG, Jin Song; and SUN, Jun.
Model checking software architecture design. (2012). Proceedings of the 14th International Symposium on High-Assurance Systems Engineering, Omaha, NE, USA, 2012 October 25-27. 193-200.
Available at: https://ink.library.smu.edu.sg/sis_research/5018
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.1109/HASE.2012.12