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

Julien Bertrane - ENS Parigi
Date and time
Tuesday, September 16, 2008 at 4:15 PM - Inizio alle 16:30, Caffè e biscotti alle 16:15.
Ca' Vignal - Piramide, Floor 0, Hall Verde
Programme Director
Roberto Giacobazzi
External reference
Publication date
August 30, 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 ?)

© 2002 - 2021  Verona University
Via dell'Artigliere 8, 37129 Verona  |  P. I.V.A. 01541040232  |  C. FISCALE 93009870234