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

Speaker:  Julien Bertrane - ENS Parigi
  Tuesday, September 16, 2008 at 4:15 PM 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 - Piramide, Floor 0, Hall Verde

Programme Director
Roberto Giacobazzi

External reference
Publication date
August 30, 2008