CAVERN
ANR-07-SESUR-003
http://www-anr-ci.cea.fr
Sécurité et Sûreté Informatique
By increasing our confidence in software reliability and safety, software testing techniques play an important rôle in the software certification process. In particular, normative documents such as DO-178 for civil and military airborne systems, Common criteria for smart cards or CEI 61508 for the automotive field include strict requirements with regard to software testing. However, software testing remains very expensive in the software development process and one of the main challenges here concerns its automation. Though much progress has been made in the last few years in this area, several limitations make it difficult to scale-up the proposed techniques. On the one hand, it is well known that some features of imperative languages are difficult to treat in an automated way (loops, references and dynamic structures, floating-point computations, etc.) ; on the other hand, building automatic tools able to test programs containing non-linear or heterogeneous computations (disjunctions, non-linear arithmetic expressions, etc.) requires expertise in different domains.
The CAVERN project (Constraints and Abstractions for program VERificatioN) aims to enhance the potential of Constraint Programming for the automated verification of imperative programs. The classic approach consists in building a constraint system representating the objective to meet. This objective may be positive, when it is a test objective; in this case the constraint system solutions are scenarios illustrating the objective, this principle is used in automatic functional or structural coverage test generation tools. Conversely, the objective may be negative in order to detect particular defects or threats; in this case the constraint system is built from the combination of the program under test and the negation of the property to be verified. A solution to the resulting constraint system corresponds to a counter-example scenario of the property; while the absence of solution, when it can be demonstrated, may correspond to a verification of the property.
This process is currently based on the use of “generic” constraint propagation based solvers developed for other applications (combinatorial optimization, planning, etc.). The originality of the project lies in the design of abstraction-based constraint solver dedicated to the automated testing of imperative programs. In Static Analysis, the last few years have seen the development of powerful techniques over various abstract domains (polyhedra, congruence, octagons, etc.) and this project aims to explore results obtained in this area to develop constraint solvers with improved deductive capabilities. The main scientific outcome of the project will be a profound understanding of the benefit of using abstraction techniques in constraint solvers for the automated testing of imperative programs.
The CAVERN project includes four partners involved in the development of constraint-based testing tools:
- the LANDE team-project of IRISA in Rennes (LANDE) – coordinator
- the “Constraints and Proofs” team from CNRS I3S laboratory in Sophia-Antipolis(CeP)
- the CEA-LIST laboratory in Saclay (CEA)
- the ILOG Company in Gentilly (ILOG)
In addition, the project will include a foreign associate partner: Andy King from the University of Kent.
Concretely, the CAVERN project partners will study the integration of selected abstractions in their own constraint libraries, as currently used in their testing tools, in order to improve the treatment of loops, memory accesses (references and dynamic structures) and floating-point computations. Dealing efficiently with these constructs will allow us to scale-up constraint-based testing techniques for imperative programs. This should open the way to more automated testing processes which will facilitate software dependability assessment.
