Modeling And Verification Of Self-adaptive Software Systems

A self-adaptive software system can modify its own behavior in response to the changes ofits requirements and operational environment at runtime. During runtime, the changes ofoperational environment will produce new requirements, but traditional models can only dealwith fixed requirements and cannot adapt themselves to the new requirements. Thus new modelswhich have the ability to describe the new requirements automatically must to be built to modelthe self-adaptive software systems. Besides, because of the continuity and uncertainty of theenvironment, the new models have infinite and uncertain states, so we must verify thecorrectness and properties of the new models.This thesis focuses on the modeling and verification of two kinds of self-adaptive systems.The first kind is the control theory based self-adaptive software systems. For this one, the thesismainly investigates the formal modeling methods and verification techniques for the switchedfuzzy systems and switched stochastic systems. A switched fuzzy system consists of globalswitching rules, local fuzzy rules and ordinary differential equations. The system is firstlydeblurred, and then transformed to a hybrid automaton. The reachable space of the gottenautomaton is then computed by the model checker PHAVer. Finally the stability is obtained byanalyzing the reachable space. A switched stochastic system is usually described by a Markovchain and stochastic differential equations. A new Petri net called stochastic-differential Petri netis proposed to model the discrete behavior, continuous and stochastic behavior of the switchedstochastic systems. The proposed model has infinite reachable states, so an equivalence relationbetween reachable states is constructed and a Markov chain is obtained from the state spacebased on the corresponding equivalence partitioning. Thus the probabilistic model checkerPRISM can be used to do model checking. The second kind is the environment-awarenessself-adaptive software systems, and a new modeling language called adaptive Petri net isproposed to model this kind of systems. An adaptive Petri net is an extension of the hybrid Petrinet by embedding a neural network in some special transitions, which is used to make decisionsaccording the changes of environment. The proposed net has the following advantages: It canmodel a runtime environment, the components in the model can collaborate to make adaptiondecisions; and the computing is done at the local while the adaption is for the whole system. Atlast a manufacturing system is used to illustrate the proposed adaptive Petri net. This thesis has done the following work:1) It is the first work that gives a formal method for modeling the switched fuzzy systemsand is able to use a model checking technique to analyze the systems’ stability, which can avoidfinding the Lyapunov functions in the traditional methods.2) A new Petri net is proposed to model discrete behavior, continuous behavior andstochastic behavior. It can be used to describe the switched stochastic systems and do modelchecking.3) A new formal language is built to describe the environment-awareness self-adaptivesoftware systems. It can not only model the software systems, but also can model the runtimeenvironment. It has a good scalability.4) A new technology is proposed to solve the problem of state explosion during the modelchecking of self-adaptive software systems.