Static analysis by abstract interpretation of properties of imperfectly-clocked synchronous systems

Julien Bertrane - ENS Parigi

Data e ora
martedì 16 settembre 2008 alle ore 16.15 - Inizio alle 16:30, Caffè e biscotti alle 16:15.

Ca' Vignal 3 - Piramide, Piano 0, Sala Verde

Roberto Giacobazzi

Referente esterno

Data pubblicazione
30 agosto 2008



The control units of embedded systems are often implemented as  
synchronous systems, some being redundant so that they resist
hardware failures.
In order to be realistic, we introduce a framework where these units  
may be imperfectly-clocked and their communications non-instantaneous.

The semantics for such systems is defined as continuous-time boolean
signals, the control parts involving only few computations. The hardware
imperfections induce a huge number of possible behaviors so that the
specifications of such a system can only be proved by abstracting it.

We introduce several abstract domains and their interactions through
reductions that enable an automatic and abstract reasoning about the  
high-level properties :
- stability and instability
- quantitative properties, i.e. integral or close notions
- qualitative comparison of behaviors at similar points of the system  
(do they change their values at the same time ? Is this signal always  
ahead of this other one ?)

Inizio pagina