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

Relatore
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.

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

Referente
Roberto Giacobazzi

Referente esterno

Data pubblicazione
30 agosto 2008

Dipartimento
 

Riassunto

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

ornamento
Inizio pagina