Il est courant de programmer les systèmes de contrôles des systèmes embarqués dans des langages synchrones. Ceux-ci postulent que les événements se produisent simultanément dans tout le système lors d'instants particuliers : les tics d'une horloge. Mais de nombreux systèmes doivent être construits autour de plusieurs horloges qui de plus peuvent se désynchroniser. Nous proposons une sémantique temps-continu qui non seulement permet de rendre compte des imperfections de façon réaliste mais aussi permet la définition de domaines abstraits plus rapides, plus simples et plus précis permettant la preuve de certaines spécifications temporelles complexes.
Synchronous programming is a formalism well adapted to the development of computer systems controlling embedded systems. It is based on the idea of the repeated synchrony of some tasks (at clock ticks). However, it is often necessary to use multi-clock systems. Furthermore, physical clocks may desynchronize. We believe that giving such a system a continuous-time semantics does not only enable modeling in a more realistic way the actual execution but also enables defining faster more precise and less costly abstract domains that can prove some of the temporal specifications of such systems.
Les systèmes de contrôles des systèmes embarqués sont souvent conçus dans des environnements qui considèrent le temps comme continu et qui modélisent sous forme d'équations différentielles ces systèmes ainsi que l'environnement avec lequel ils interagissent.
Ces systèmes sont ensuite discrétisés (selon une horloge) et programmés dans des langages synchrones. Mais de nombreux systèmes doivent alors être construits de façon plus complexe autour de plusieurs horloges qui peuvent alors se désynchroniser.
Nous proposons une sémantique non-standard à temps-continu qui permet de rendre compte des imperfections matérielles de façon réaliste et des difficultés du cas multi-horloge. Mais elle permet surtout la définition de domaines abstraits plus rapides, plus simples et plus précis, capables de prouver certaines spécifications temporelles complexes des systèmes.
Nous proposons une description d'un prototype d'analyseur statique implémenté en Ocaml, qui abstrait cette sémantique temps-continu en un produit-réduit de plusieurs domaines abstraits. Ces domaines formalisent la manipulation automatique des notions suivantes, en tenant compte de leur forte dimensions temporelle : - les relations entre la valeur d'une variable et le temps, - la stabilité et l'instabilité des valeurs, - les propriétés quantitatives des variables, comme leur intégrale au cours du temps.
The common way to design the computerized control of embedded systems is to describe their behavior as well as the environment they evolve in as differential equations in a framework (e.g. Simulink) that is able to study and combine such equations.
These equations are then discretized (according to a clock) so that they can programmed in a synchronous language. However, more complex system are often necessary, in particular multi-clock systems, but their physical clocks may desynchronize, which makes them difficult to study.
We believe that giving such a system a continuous-time semantics does not only enable modeling in a more realistic way the actual execution (including hardware imperfections and the multiple clock case) but enables moreover defining faster, more precise and less costly abstract domains that can prove some of the temporal specifications of such systems.
We introduced a framework that enables an automatic static analysis, based on several abstractions of this continuous-time semantics and their interactions through reductions. It reasons abstractly about the following high-level properties, which are closely related to temporal aspects: - relation between constant values and the time, - stability and instability of values, - quantitative properties, i.e. integral or close notions. This framework led to the implementation of a prototype of analyzer.
