Developing temporal abstract domains that prove the temporal specifications of reactive systems

May 10, 2010

Julien Bertrane


Developing temporal abstract domains that prove the temporal specifications of reactive systems

Time:   11:00am
Location:   IMDEA conference room

We consider the complex behaviors of embedded systems with several communicating imperfectly-clocked synchronous systems. In order to prove statically and automatically their properties, we introduced a “time-continuous” semantics and several ad hoc temporal abstract domains.

Then we show how to build new temporal domains from these simple basic domains, through the use of abstract transformers and of reduced products. The temporal aspects of this domains eases the automatisation of some of this optimizations and makes reductions more precise.