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

Relatore:  Julien Bertrane - ENS Parigi
  martedì 16 settembre 2008 alle ore 16.15 - Inizio alle 16:30, Caffè e biscotti alle 16:15.

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 ?)

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

Roberto Giacobazzi

Data pubblicazione
30 agosto 2008

Offerta formativa