Jia Xiaolin, Qin Zheng, He Jian, Yu Fan
(School of Electronics and Information Engineering, Xi'an Jiaotong University, Xi'an 710049, China)
Abstract: Due to the deficiency of architecture description languages in
analyzing and validating dynamic behavior of software systems, the predicate/transition
(Pr/T) net was introduced to model the dynamic features of software architecture, and an
efficient model-checking algorithm was proposed. Firstly, the dynamic feature model (DFM)
of the architecture was constructed in terms of extended Pr/T net of the hierarchical
model of it and the approachability graph was formed. Then the linear temporal logic
properties (LTL) of the system could be verified based on the model checking method of
automata theory. Finally, the validity of our approach was shown through modelling the
concurrent control system and checking model in a case study of an electronic commerce
system. It is demonstrated by the practice that the modelling-and-checking method
presented combines the advantages of linear temporal logic with those of Pr/T net, so that
it provides a basis for further developing approaches to analyze and validate dynamic
features of software architectures.
Keywords: software architecture; predicate／transition net; linear temporal logic; model
validating