M2 Research Internship State space abstraction for timed systems

Timed systems have become ubiquitous in the past few years. Some of them (e.g., automated plane and unmanned systems control, driverless cars) are critical in the sense that no error must occur. Testing these systems can possibly detect the pres-ence of bugs, but not guarantee their absence. It is necessary to use formal methods such as model checking [BK08] so as to prove formally the correctness of a system. One of the main formalisms used to specify and verify critical timed systems is timed automata [AD94]. Unfortunately, verifying large systems is often challenging due to the state space explosion problem. One way to prevent this problem is to build abstractions of the state space. Such an abstraction is generally guided by the property one wants to check. Internship subject Recently, Symbolic Observation Graphs [HIK04, KP08, DLKPTM11] have been pro-posed for untimed systems. This powerful abstraction significantly reduces the state space while preserving some interesting temporal properties (LTL). The main objec-tive of this internship is to extend the SOG-based approach to timed systems. An implementation may also be performed by the intern, so as to validate the proposed approach