An Improvement of Software Architecture Verification

作     者：Ding, Zuohua Liu, Jing 

作者机构：Zhejiang Sci Tech Univ Ctr Math Comp & Software Engn Hangzhou 310018 Peoples R China East China Normal Univ Shanghai Key Lab Trustworthy Comp Shanghai 200062 Peoples R China 

出 版 物：《ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE》 (理论计算机科学电子札记)

年 卷 期：2009年第243卷

页      面：49-67页

核心收录：

学科分类：08[工学] 0812[工学-计算机科学与技术（可授工学、理学学位）] 

基　　金：National Key Research program of Dependable Software Theory National High Tech Research 863 Program of China [2006AA01Z165] National Natural Science Foundation of China [60673114, 60603037] International Cooperation Program of Shanghai 

主　　题：Static analysis architecture ordinary differential equation Wright 

摘      要：Static analysis may cause state space explosion problem. In this paper we explore differential equation model that makes the task of verifying software architecture properties much more efficient. We demonstrate how ordinary differential equations can be used to verify application-specific properties of an architecture description without hitting this problem. An architecture behavior can be modeled by a group of ordinary differential equations containing some control parameters, where the control parameters are used to represent deterministic/nondeterministic choices. Each equation describes the state change. By checking the conditions associated with the control parameters, we can check whether an equation model is feasible. After solving a feasible equation model, based on the solution behavior and the state variable representation, we can analyze properties of the architecture. A WRIGHT architecture description of the Gas Station problem has been used as the example to illustrate our method. All of the equations have been computed with Matlab tool.