Sécurité et Sûreté Informatique








Modèle Rapport



Cpbpv (CeP) is a novel constraint-programming framework for bounded program verification.  The Cpbpv framework uses constraint stores to represent the specification and the program and explores execution paths non-deterministically. The input program is partially correct if each constraint store so produced implies the post-condition. Cpbpv does not explore spurious execution paths as it incrementally prunes execution paths early by detecting that the constraint store is not consistent. Cpbpv is parameterized with a list of solvers which are tried in sequence, starting with the least expensive and less general. Experimental results often produce orders of magnitude improvements over earlier approaches, running times being often independent of the variable domains. Moreover, Cpbpv was able to detect subtle errors in some programs while other frameworks based on model checking have failed.

Euclide (INRIA-Lande) is a Constraint-Based Testing tool for verifying safety-critical C programs. By using a mixture of symbolic and numerical analyses (namely static single assignment form, constraint propagation, integer linear relaxation and search-based test data generation), it addresses three distinct applications in a single framework: structural test data generation, counter-example generation and partial program proving. The core algorithm of the tool takes as input a C program and a point to reach somewhere in the code. As a result, it outcomes either a test datum that reaches the selected point, or an ``unreachable'' indication showing that the selected point is unreachable. Optionally, the tool takes as input additional safety properties that can be given under the form of pre/post conditions in ACSL or assertions directly written in the code. In this case, Euclide can either prove that these properties or assertions are verified or find a counter-example when there is one. As these problems are undecidable in the general case, Euclide only provides a semi-correct procedure (when it terminates, it provides the right answer) for them. Current Research works around the tool focus on modular integers and floating-point computations and better constraint solving procedures based on relational abstract domains computations.

Gatel (CEA) is a test environment for synchronous models of reactive systems described in Lustre/SCADE. The core of the tool is a CLP interpretation of the Lustre language, together with a resolution procedure dedicated to the underlying linear temporal logic. This framework allows to automate a wide range of usual testing activities. Initially designed for generating test sequences according to a test objective, Gatel also addresses symbolic simulation, model debug, conformance checking, coverage analysis/completion, test suite evaluation.  Current work is twofold: updating the CLP interpretation and procedure to the latest version of the SCADE Suite (enriched with built-in state machines), upgrading the procedure with powerful abstractions to scale up to real-life industrial models.

Jaut (Java Automatic Unit Testing) (INRIA -- Lande)  is a test case generator for programs in bytecode Java. Given a bytecode instruction of the method under test, it aims to find an input memory state (values of the parameters and of the instances in the heap) to cover this instruction. Repeating this process, the structural coverage criteria of  all-the-statements can be fulfilled. In Jaut, bytecode instructions are modelled with constraints, as well as the conditions that permit to reach the goal: an input memory state to cover the goal instruction can so be found by constraint solving. The tool currently deals with arithmetic operations on integers, heap manipulation and conditional instructions. The implementation of a strategy to avoid enumerating the paths that lead to the goal until finding an executable one is in progress. Current work also includes dealing with polymorphic function calls.

PathCrawler is a tool prototype developed by the LSL laboratory of CEA List. PathCrawler automatically generates test-case inputs guaranteeing full structural coverage of the C function under test: all feasible paths, all reachable branches, all k-paths,... PathCrawler runs an automatically-instrumented version of the function under test on each test-case as soon as it is generated in order to recover the path covered by this test-case and ensure that the next test-case covers a path which is not covered yet. Test-case generation is implemented using constraint logic programming. To ensure that PathCrawler can be used on real-life programs, current work focusses on the treatment of called functions, the treatment of the precondition on the effective input parameters under which the function is to be tested, the treatment of pointer casts, the treatment of integer overflows and floating-point numbers and the early detection of infeasible path prefixes.