文档介绍：The Journal of Systems and Software 83 (2010) 723–744
Contents lists available at ScienceDirect
The Journal of Systems and Software
journal homepage: ate/jss
A classification parison of model checking software architecture techniques
Pengcheng Zhang a,c, Henry ini b,*, Bixin Li a
a School puter Science and Engineering, Southeast University, China
b Dipartimento di Informatica, University of L’Aquila, L’Aquila, Italy
c College puter and Information Engineering, Hohai University, China
article info abstract
Article history: Software architecture specifications are used for many different purposes, such as documenting architec-
Received 28 August 2008 tural decisions, predicting architectural qualities before the system is implemented, and guiding the
Received in revised form 10 September design and coding process. In these contexts, assessing the architectural model as early as possible
2009
es a relevant challenge. Various analysis techniques have been proposed for testing, model check-
Accepted 11 November 2009
ing, and evaluating performance based on architectural models. Among them, model checking is an
Available online 16 December 2009
exhaustive and automatic verification technique, used to verify whether an architectural specification
conforms to expected properties. While model checking is being extensively applied to software architec-
Keywords:
tures, little work has been done prehensively enumerate and classify these different techniques.
Software architecture
Model checking The goal of this paper is to investigate the state-of-the-art in model checking software architectures.
For this purpose, we first define the main activities in a model checking software architecture process.
Then, we define a classification parison framework pare model checking software archi-
tecture techniques according to it.
Ó 2009 Elsevier Inc. All rights reserved.
1. Introduction Analysis techniques and tools have been introduced to under-
stand