An Improvement of Software Architecture Verification

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.