Compositional Verification Based On Interface Automata

Formal verification is an effective approach to enhancing the reliability of softwares. In order to lower the complexity of formal verification, especially model checking and refinement checking, compositional methods have been presented. Its core idea is to divide a big and global verification task into a group of small and local subtasks, which are then solved separately. A key problem of compositional verification lies in the difficulties of task division, which are brought by the dependence relationships between components. Because the traditional formalisms can not express explicitly the assumptions of a component to the environment, it is often necessary to construct some environment models in the procedure of compositional verification, which increases the complexity to a great extent. The thesis investigates the compositional verification, especially the compositional refinement checking, of software designs based on a new formalism, interface automata, which can express explicitly the assumptions of a component to the environment and thus benefits compositional verification.The research is done from three aspects. Firstly, in order to reveal the essence of interface automata, the thesis investigates the relationship between the new formalism and the traditional I/O automata. Secondly, some correction and enhancement are made to the theory of interface automata, and then the revised theory is applied to the compositional analysis and verification of software architectures. Lastly, a new approach is presented to the compositional refinement checking of interface automata.The main contributions of this thesis are summarized as follows.1. An equivalence relation is established between the refinement of interface automata and the forward simulation of I/O automata. The refinement of interface automata is defined in an alternating approach, which is such different with the forward simulation of I/O automata that some researchers consider that they respectively belong to two different kinds of models for component-based development: interface models and component models. Thus the equivalence relation also means the setting up of a connection between the two categories of models, and the setting up of the basis to integrate the design of components based on interface automata with the verification of components based on I/O automata. At the meantime, the result makes it possible to reuse the theory and tool supports of I/O automata to solve the problem of interface automata.2. Some correction and enhancement are made to the interface automata formalism. Firstly, we find and fix an error in the original theory of interface automata. Secondly, we extend the idea of 2/3 simulation in CCS to interface automata and present the notion of 2/3 alternating simulation. Then the refinement of interface automata is redefined based on 2/3 alternating simulation. The new refinement can preserve deadlock-freedom property, which makes it more useful. Thirdly, to describe the refinement relations between the interfaces of components and the implementations of components, we bring forward the notion of generalized refinement. At the same time, the rules of compositional refinement checking are established for the new refinements.3. Based on the revised interface automata theory, we redefine the semantics of the architecture description language WRIGHT. The new semantics appears more concise and more natural. Wright is a famous architecture description language. Its existent testing rules are complicated, because the assumptions to environments must be calculated explicitly in the rules. We find that the interpretation to Wright can become much simpler if adopting interface automata as the new semantic model. Thus, the paper redefines the semantics and testing rules of Wright based on interface automata. Besides, a solution to the problem of web service composition is presented in the framework of Wright.4. The notion of relative unreachable transitions is defined, on the basis of which a new approach to compositional refinement checking is presented. Because no consideration is made to the influence of environments to subtasks, the application of the simple principle for compositional refinement checking is limited greatly. In the thesis, an improvement to the simple principle is made. According to the new principle, a reduction should be made first to simplify those behaviors that are not possible to take place, and then the simple principle is applied. Thus when it is not feasible to apply the simple principle directly, applying the new principle may do. Furthermore, the calculation of the relative unreachable transitions of interface automata can be transformed to the invariants checking of LSTS (Labelled State Transition System). In order to solve the latter problem efficiently, the thesis presents a new equivalence on LSTS, namely called reverse observation equivalence. The new equivalence can preserve invariants properties. Moreover, it is a congruence with respect to the parallel composition and hiding operators of LSTS. Therefore, compositional reachability analysis based on the new equivalence can be made to check invariants of LSTS. The experimentsshow that the method is effective.