Please use this identifier to cite or link to this item: https://doi.org/10.1109/HASE.2012.12
Title: Model checking software architecture design
Authors: Zhang, J.
Liu, Y.
Sun, J.
Dong, J.S. 
Sun, J.
Keywords: Formal Verification
Model Checking
PAT
Software Architecture
Wright
Issue Date: 2012
Source: Zhang, J.,Liu, Y.,Sun, J.,Dong, J.S.,Sun, J. (2012). Model checking software architecture design. Proceedings of IEEE International Symposium on High Assurance Systems Engineering : 193-200. ScholarBank@NUS Repository. https://doi.org/10.1109/HASE.2012.12
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. © 2012 IEEE.
Source Title: Proceedings of IEEE International Symposium on High Assurance Systems Engineering
URI: http://scholarbank.nus.edu.sg/handle/10635/40064
ISBN: 9780769549125
ISSN: 15302059
DOI: 10.1109/HASE.2012.12
Appears in Collections:Staff Publications

Show full item record
Files in This Item:
There are no files associated with this item.

SCOPUSTM   
Citations

2
checked on Dec 11, 2017

Page view(s)

65
checked on Dec 9, 2017

Google ScholarTM

Check

Altmetric


Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.