Research On Dynamic Software Architecture Modeling And Model Checking Methods

The environment which located by the software system is changing according to the technique development, so the traditional static software architecture does not satisfy the present user's demands.In the contrast, the dynamic software architecture can not only strengthen the user's definition and extensibility but also lower the development fee and decrease the system's risk, meanwhile it can provide the service to update the system's property to users.In this way the development and study of dynamic software architecture is becoming hotspot of software engineering.In the recent years,the primary coverage of dynamic software architecture studying concentrates on Modeling and Model Checking. The modeling of dynamic software architecture is the basis of successful software design, and the Model Checking of dynamic software architecture is the key factor to guarantee the quality of dynamic software architecture.Both of them are indispensable.At present days the studying of Modeling and Model Checking of dynamic software architecture is not consummate because of its particularity, and it lacks the uniform methods of Modeling and Checking.This Dissertation concentrates the author's research findings in software development, based on practice it proposed the methods of Modeling and Model Checking of dynamic software architecture to satisfy the demands of software architecture dynamics.The real application of "The production and project management system of power enterprises" has achieved perfect effects.The concrete contents are as following:1.Based on the theoretical basis of software architecture the dissertation elaborates how to choose the methods of Modeling and Model Checking of dynamic software architecture which will best suit the present system environment, meanwhile,importance of valid choosing Modeling and Model Checking has been proven through the practice.2.This dissertation proposes a demand driven modeling method of dynamic software architecture.Under Le Metayer's theory of system architecture modeling and principles,this method proposes a demand driven modeling method of dynamic software architecture based on the concept property demand and goal modeling, the SAAM method of graphic primitive symbolic describing system. 3.This dissertation proposes a property expressing logic method of dynamic software architecture based on predicateμcalcus arid space logics.It adds the expression logics to space algorithm operators, and unifying logic expresses the structure and behavior property to solve the problem of separately expressing the property and logics.In the expression of property logics, it proposes property goal partial satisfying model to solve the partial satisfy problem of property goal.4. In the Model Checking of dynamic software architecture, this dissertation separately proposes a demand goal driven decreasing state space method which is based on equivalent theory, and a Model Checking method of dynamic software architecture which is based on LMC.Using the equivalent theory to verify the equivalent relationship before and after the operation of system architecture, it proposes a new decreasing state space method upon dynamic system architecture, and it in some extent relieves the state space explosion problem. The state space of initial system architecture is the enter data of Model Checking algorithm, and the method of Model Checking is the core of Model Checking. Moreover, it still proposes an extended LMC Model Checking of dynamic software architecture, based on the LMC algorithm, it extendes the verifying of space operators and solved the problem of simultaneously verifying the structure and the behavior property.5.According to the Modeling and Model Checking methods in this dissertation, it carried out the application study in the real case of "The production and project management system of power enterprises"...