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