Cooperative Software Testing and Analysis: Advances and Challenges

In recent years, to maximize the value of software testing and analysis, we have proposed the methodology of cooperative software testing and analysis （in short as cooperative testing and analysis） to enable testing and analysis tools to cooperate with their users （in the form of tool-human cooperation）, and enable one tool to cooperate with another tool （in the form of tool-tool cooperation）. Such cooperations are motivated by the observation that a tool is typically not powerful enough to address complications in testing or analysis of complex real-world software, and the tool user or another tool may be able to help out some problems faced by the tool. To enable tool-human or tool-tool cooperation, effective mechanisms need to be developed 1） for a tool to communicate problems faced by the tool to the tool user or another tool, and 2） for the tool user or another tool to assist the tool to address the problems. Such methodology of cooperative testing and analysis forms a new research frontier on synergistic cooperations between humans and tools along with cooperations between tools and tools. This article presents recent example advances and challenges on cooperative testing and analysis.

Architecting Fault Tolerance with Exception Handling: Verification and Validation

When building dependable systems by integrating untrusted software components that were not originally designed to interact with each other, it is likely the occurrence of architectural mismatches related to assumptions in their failure behaviour. These mismatches, if not prevented during system design, have to be tolerated during runtime. This paper presents an architectural abstraction based on exception handling for structuring fault-tolerant software systems. This abstraction comprises several components and connectors that promote an existing untrusted software element into an idealised fault-tolerant architectural element. Moreover, it is considered in the context of a rigorous software development approach based on formal methods for representing the structure and behaviour of the software architecture. The proposed approach relies on a formal specification and verification for analysing exception propagation, and verifying important dependability properties, such as deadlock freedom, and scenarios of architectural reconfiguration. The formal models are automatically generated using model transformation from UML diagrams： component diagram representing the system structure, and sequence diagrams representing the system behaviour. Finally, the formal models are also used for generating unit and integration test cases that are used for assessing the correctness of the source code. The feasibility of the proposed architectural approach was evaluated on an embedded critical case study.

Verification of Interdomain Routing System Based on Formal Methods

In networks, the stable path problem （SPP） usually results in oscillations in interdomain systems and may cause systems to become unstable. With the rapid development of internet technology, the occurrence of SPPs in interdomain systems has quite recently become a significant focus of research. A framework for checking SPPs is presented in this paper with verification of an interdomain routing system using formal methods and the NuSMV software. Sufficient conditions and necessary conditions for determining SPP occurrence are presented with proof of the method＇s effectiveness. Linear temporal logic was used to model an interdomain routing system and its properties were analyzed. An example is included to demon- strate the method＇s reliability.

Combination of Model Checking and Theorem Proving to Verify Embedded Software

In this paper, a scheme of combining model checking and theorem proving techniques to verify high trustworthy embedded software is proposed. The software model described in state machine of unified model language is transformed into the input modeling language of a model checker in which the model is analyzed with associated property specifications expressed in temporal logic. The software model which has been verified by model checker is then transformed into abstract specifications of a theorem prover , in which the model will be refined, verified and translated into source C code. The transformation rules from state machine to input language of model checker and abstract specifications of theorem prover are given. The experiment shows that the proposed scheme can effectively improve the development and verification of high trustworthy embedded software.

Improved Bounded Model Checking for the Universal Fragment of CTL

SAT-based bounded model checking （BMC） has been introduced as a complementary technique to BDD-based symbolic model checking in recent years, and a lot of successful work has been done in this direction. The approach was first introduced by A. Biere et al. in checking linear temporal logic （LTL） formulae and then also adapted to check formulae of the universal fragment of computation tree logic （ACTL） by W. Penczek et al. As the efficiency of model checking is still an important issue, we present an improved BMC approach for ACTL based on Penczek＇s method. We consider two aspects of the approach. One is reduction of the number of variables and transitions in the κ-model by distinguishing the temporal operator EX from the others. The other is simplification of the transformation of formulae by using uniform path encoding instead of a disjunction of all paths needed in the κ-model. With these improvements, for an ACTL formula, the length of the final encoding of the formula in the worst case is reduced. The improved approach is implemented in the tool BMV and is compared with the original one by applying both to two well known examples, mutual exclusion and dining philosophers. The comparison shoves the advantages of the improved approach with respect to the efficiency of model checking.

A QUANTIFIER-ELIMINATION BASED HEURISTIC FOR AUTOMATICALLY GENERATING INDUCTIVE ASSERTIONS FOR PROGRAMS

A method using quantifier-elimination is proposed for automatically generating program invariants/inductive assertions. Given a program, inductive assertions, hypothesized as parameterized formulas in a theory, are associated with program locations. Parameters in inductive assertions are discovered by generating constraints on parameters by ensuring that an inductive assertion is indeed preserved by all execution paths leading to the associated location of the program. The method can be used to discover loop invariants-properties of variables that remain invariant at the entry of a loop. The parameterized formula can be successively refined by considering execution paths one by one; heuristics can be developed for determining the order in which the paths are considered. Initialization of program variables as well as the precondition and postcondition, if available, can also be used to further refine the hypothesized invariant. The method does not depend on the availability of the precondition and postcondition of a program. Constraints on parameters generated in this way are solved for possible values of parameters. If no solution is possible, this means that an invariant of the hypothesized form is not likely to exist for the loop under the assumptions/approximations made to generate the associated verification condition. Otherwise, if the parametric constraints are solvable, then under certain conditions on methods for generating these constraints, the strongest possible invariant of the hypothesized form can be generated from most general solutions of the parametric constraints. The approach is illustrated using the logical languages of conjunction of polynomial equations as well as Presburger arithmetic for expressing assertions.