Aspect-oriented Modeling And Analysis Techniques For Software Fault Tolerance

With the pervasive application of computational systems, the information infrastructure based on software has penetrated all walks of life, playing an extremely significant role. The rapid development of software techniques and increasing enhancement of function requirements make the software systems get increasingly complicated. Failing of these systems can cause mild inconveniences or even catastrophic damages with lives lost. Therefore, the requirements of correctness, dependability hold great significance to the software. The core of ensuring system dependability is accepting the ever-present errors in the system and its environment and providing expected service, which is called fault tolerance. Unfortunately, so far, most of the fault tolerance solutions exclusively focus on the implementation instead of earlier development phase, especially design phase. This could bring a serious gap between the requirement and the fault tolerant measures carried out during implementation phase.Generally, the software system requirements consist of functional requirements and non-functional ones. Functional requirements specify functionality that a system is supposed to accomplish while non-functional requirements specify overall characteristics and performance. Many non-functional requirements are orthogonal not only to each other but also to the functional requirements. Traditional methods always make non-functional code tangling and scattering in functional code, which reduces the efficiency and maintainability. The aspect-orientation method can clearly separate these non-functional requirements from functional ones and modular them by aspects then weave all the separate loose coupled concerns into a whole system. Most of the fault tolerant properties of software are non-functional requirements that across several functional modules. As a result, aspects can contribute to the modeling and analysis of fault tolerant properties, which improves the software extendibility, maintainability and reusability.There is an increasing number of works on aspect-oriented modeling which can be divided into informal and formal way. Informal methods lack of rigorous analysis leading to error-proneness. Most existing formal methods always introduce more complexity and need extra verification tool. Consequently, it is necessary to develop a succinct and strict way. Petri nets boost rigorous mathematical foundation and fruitful verification tools. It can describe and analyze systems that are characterized as concurrent, asynchronous, distributed, parallel and nondeterministic in an intuitive and easy way. It contributes not only to qualitatively understanding the dynamic behavior of system, but also to quantitatively evaluate various performance indexes. It is well suited for system modeling and analysis. In this thesis, we first observe system structure by Petri nets. On the basis of that, we exploit data features by hierarchical Colored Petri nets that consist of a series of subsets which related to each other in a formal way. These characteristics of hierarchical colored Petri nets naturally contribute to the separation and independent modularization of fault tolerant aspects as well as the composition with the base model. Furthermore, the design, simulation and analysis of the model can use the CPN tools at hand.The main contributions of this thesis are as follows.An approach to modeling aspect oriented Petri net based use case is proposed. The approach extends the traditional UML use case model to support aspect oriented annotation. Aspect oriented use case modeling approach is introduced at first. Use case view is formally transformed into Petri net model so as to make up for the non-formalism and semi-formalism properties of UML. Thus, requirements and modeling errors in use case view can be detected in time.Temporal logic is introduced into the verification and analysis of aspect oriented Petri nets. The correctness of transformed aspect oriented Petri nets can be verified by temporal logical formulations. The validity of weaving time can be checked via the execution sequence of Petri nets.A technique of aspect oriented modeling based colored Petri nets is established. Separation and composition of aspects from and with the base module are resorted to the hierarchy concept and sub module management of colored Petri nets. In addition, a formal weaving mechanism of AOHCPNM is proposed.A technique for aspect-oriented fault tolerance modeling and analysis is developed. Based on the aspect-oriented colored Petri nets, basic module and fault tolerant module are modeled as separate sub modules, connecting by general and specific substitution transitions. Besides, exception set and exception closure are constructed to contribute to error detection, exception handling and retry modeling. State space and simulator of CPN Tools are used to verify the correctness, validity and effectiveness of the fault tolerance model.