Modeling and Checking the Behavior of Software Architecture

He Jian; Qin Zheng

Journal of Computer Research and Development > 2005 > 42(11): 2018-2024.

He Jian, Qin Zheng. Modeling and Checking the Behavior of Software Architecture[J]. Journal of Computer Research and Development, 2005, 42(11): 2018-2024.

Citation:

He Jian, Qin Zheng. Modeling and Checking the Behavior of Software Architecture[J]. Journal of Computer Research and Development, 2005, 42(11): 2018-2024.

Citation:

He Jian, Qin Zheng. Modeling and Checking the Behavior of Software Architecture[J]. Journal of Computer Research and Development, 2005, 42(11): 2018-2024.

PDF (420 KB)

Modeling and Checking the Behavior of Software Architecture

He Jian^1,2,
Qin Zheng²

1(School of Software Engineering, Beijing University of Technology, Beijing 100022) 2(E-Commerce Institute, School of Electronic and Information Engineering, Xi'an Jiaotong University, Xi'an 710049)

More Information

Published Date: November 14, 2005

Graphical Abstract

Abstract

Abstract

Since architecture description languages are not capable enough in analyzing and validating the dynamic behavior of software architecture, the hierarchical framework for software architecture is proposed in this paper, in which the abstract algebra is used to abstract the components, connectors and architectural configuration. Meanwhile, the predicate transition (Pr/T) net is introduced to model the dynamic behavior of software architecture, and an efficient model-checking algorithm based on the linear temporal logic (LTL) is discussed in details. Finally, the approach to model a current control mechanism in an E-commerce system and checking results based on LTL are shown in details. It can be demonstrated by practice that the modeling-and-checking method presented combines the advantages of linear temporal logic with those of Pr/T net, so that it provides novel approaches to analyze and validate the dynamic behavior of software architecture.
- software architecture,
- Pr/T net,
- linear temporal logic,
- model checking

FullText(HTML)

References (0)

[1]	Wang Yuquan, Wen Lijie, Yan Zhiqiang. Alignment Based Conformance Checking Algorithm for BPMN 2.0 Model[J]. Journal of Computer Research and Development, 2017, 54(9): 1920-1930. DOI: 10.7544/issn1000-1239.2017.20160756
[2]	Chen Donghuo, Liu Quan, Jin Haidong, Zhu Fei, Wang Hui. A Temporal Logic with a Semantics Defined on the Static Structure and Dynamic Behavior of Program[J]. Journal of Computer Research and Development, 2016, 53(9): 2067-2084. DOI: 10.7544/issn1000-1239.2016.20150370
[3]	Wei Ou, Shi Yufeng, Xu Bingfeng, Huang Zhiqiu, Chen Zhe. Abstract Modeling Formalisms in Software Model Checking[J]. Journal of Computer Research and Development, 2015, 52(7): 1580-1603. DOI: 10.7544/issn1000-1239.2015.20140413
[4]	Pang Tao, Duan Zhenhua. Symbolic Model Checking of WISHBONE on-Chip Bus[J]. Journal of Computer Research and Development, 2014, 51(12): 2759-2771. DOI: 10.7544/issn1000-1239.2014.20131164
[5]	Jiang Hua, Li Xiang. Model Checking for Mobile Ambients[J]. Journal of Computer Research and Development, 2009, 46(10): 1750-1757.
[6]	Men Peng and Duan Zhenhua. Extension of Model Checking Tool of Colored Petri Nets and Its Applications in Web Service Composition[J]. Journal of Computer Research and Development, 2009, 46(8): 1294-1303.
[7]	Zhang Junhua, Huang Zhiqiu, and Cao Zining. Counterexample Generation for Probabilistic Timed Automata Model Checking[J]. Journal of Computer Research and Development, 2008, 45(10): 1638-1645.
[8]	Huang Weiping. Program Restructuring to Improve Efficiency of Software Model Checking[J]. Journal of Computer Research and Development, 2008, 45(8): 1417-1422.
[9]	Jiang Yuncheng, Tang Yong, Wang Ju, Ji Gaofeng. Description-Logic-Based Temporal ER Model with Attribute Dependencies[J]. Journal of Computer Research and Development, 2007, 44(10): 1765-1773.
[10]	Wu Lijun, Su Kaile, Chen Qingliang, Yang Zhihua. Algorithm Research on “On the Fly” Model Checking Temporal Logics of Knowledge in Multi-Agent Systems[J]. Journal of Computer Research and Development, 2006, 43(8): 1417-1424.