New features
Project manager 		Editors
Debugger 		White paper
Brochure 		bracketRTDS
blank
bandeau3

imPROVE-SDL

For software designers and verification engineers who need to boost their verification productivity in designing protocols, imPROVE-SDL is a prover and a property checker that complements simulation in performing exhaustive debugging of SDL models without the need for test benches.

Unlike automatic rule checking or random test generation techniques, imPROVE-SDL can find the "hard" bugs hidden in complex protocol implementations and help identify and fix ambiguities in specifications.

imPROVE-SDL is a formal verification tool for SDL models.

Formal proof has the value of an exhaustive simulation, and cannot miss any case of potential violation of a defined property, independently of its occurrence probability. If a suspect case is identified, the prover generates a counter-example that can then be replayed step by step, forward and backward, to analyse the behaviour of the system and take the necessary measures for correction, very early in the process. If, however, no violation case exists, imPROVE-SDL will give a proof of its absence.

Unlike traditional formal verification techniques, often quite complicated and requiring a lot of mathematical knowledge for successful applications, imPROVE-SDL is an intuitive, easy-to-use solution providing formal verification to the validation process without requiring any knowledge of formal verification languages, and mathematical background.


Formal Verification Vs. Simulation

Simulation

The most traditional verification method used for testing a model is simulation. Simulation is essential to functionally verify a system, but:
  • simulation is not exhaustive: some unwanted situations can be very difficult to reach by simulation; missing a possible combination of states may alter the product quality, and is too dangerous for a safety-critical system. That means that simulation can highlight the presence of errors, but NOT their absence.
  • manually setting-up and running test-scenarios on simulated models is time consuming and increases simulation costs.

Formal Verification

imPROVE-SDL is an innovative solution to verify the correct behavior of SDL designs. Unlike simulation - where confidence in a design comes from running an arbitrary number of test cases - formal verification uses exhaustive mathematical techniques to examine the entire solution space of a specified requirement of the design - explicit or not - called a property and extracted from the specifications, thus providing better functional test coverage.

Besides, it is much more direct and natural to verify that, at any instant, "if ECU1 is in Reset mode, ECU2 is always in Init or Ready mode", rather than trying to find situations where it is not the case, using simulation. In this situation imPROVE-SDL will give a proof of the invalidity of the property: "There exists a state where ECU1 is in Reset Mode and ECU2 is in a mode different than Init or Ready" or it will extract an execution sequence illustrating the violation of this property.