Skip to Main content Skip to Navigation
Theses

Simulation abstraite : une analyse statique de modèles Simulink

Abstract : In regard to the growth of complexity of embedded systems, software tools are needed at design-time. Simulink and Lustre/Scade are the main industrial tools used in this context. Despite of the numerous features added in both tools, such as simulation, test or code generation, Simulink is more often used due to its important system design expressiveness. It allows us to model and simulate continuous-time and discrete-time systems, as well as a mix of both. For embedded systems, Simulink offers a convenient way to model and specify both the embedded software and the physical environment. The application of formal methods on such specifications is an important challenge for the validation of embedded software. Moreover, applying formal methods sooner in the cycle of development is also an essential industrial challenge in order to reduce the cost of bug fixing.

In this thesis, we define a static analysis by abstract interpretation of Simulink models. This static analysis is called Abstract Simulation. The aim of Abstract Simulation is to provide a correctness criterion for the executions of Simulink models because they are often used for the validation of systems. However, such simulations are closer to test-based verifications than to formal proofs and, consequently, they do not permit to validate, in regards to the specification, a system. Abstract Simulation provides a correctness criterion for numerical behaviors of the Simulink models in the sense that they mimic what happens in the real world.

We assume that the mathematical model encoded as a Simulink model is correct (the physical system is correctly modeled). We aim at automatically and conjointly compute an over-approximation of the mathematical behaviors and the simulation behaviors for all the possible inputs of the model. We can thus estimate the whole imprecision introduced by the simulation, i.e. numerical errors as truncation errors and round-off errors as well as sensor errors like quantization and sampling. The correctness criterion of continuous-time models is given by the distance between numerical integration algorithm (Simulink solver) and guaranteed numerical integration algorithm based on Taylor method. The correctness criterion of discrete-time models is given by using the abstract numerical domain of floating-point numbers with errors. Furthermore, Abstract Simulation uses two abstract numerical domains, such that the domain of Taylor forms and the domain of floating-point numbers with differentiated errors. The former is a composition of the domain of floating-point numbers with errors and the automatic differentiation techniques. This combination permits to compute a better over-approximation of the rounding errors. Abstract Simulation is also based on an abstraction of sequences using set partitioning. These domains allow us to estimate errors introduced by numerical algorithms and by computations during simulations. As a result, our method makes it possible to validate numerical behaviors of embedded systems modeled in Simulink.
Complete list of metadatas

https://pastel.archives-ouvertes.fr/tel-00366685
Contributor : Alexandre Chapoutot <>
Submitted on : Monday, March 9, 2009 - 2:19:33 PM
Last modification on : Monday, October 19, 2020 - 11:12:58 AM
Long-term archiving on: : Friday, October 12, 2012 - 1:11:21 PM

Identifiers

  • HAL Id : tel-00366685, version 1

Citation

Alexandre Chapoutot. Simulation abstraite : une analyse statique de modèles Simulink. Génie logiciel [cs.SE]. Ecole Polytechnique X, 2008. Français. ⟨tel-00366685⟩

Share

Metrics

Record views

819

Files downloads

3017