We present constraint matrix diagrams (CMDs), a novel data structure for the fully symbolic reach ability analysis of timed automata. CMDs combine matrix-based and diagram-based state space representations generalizing the concepts of difference bound matrices (DBMs), clock difference diagrams (CDDs), and clock restriction diagrams (CRDs). The key idea is to represent convex parts of the state space as (partial) DBMs which are, in turn, organized in a CDD/CRD-like ordered and reduced diagram. The location information is incorporated as a special Boolean constraint in the matrices. We describe all CMD operations needed for the construction of the transition relation and the reach ability fixed point computation. Based on a prototype implementation, we compare our technique with the timed model checkers RED and Uppaal, and furthermore investigate the impact of two different reduced forms on the time and space consumption.

The mission of the Verisoft project is (i) to develop techniques, which permit the pervasive formal verification of computer systems comprising hardware, system software, communication systems, and applications, (ii) to apply these techniques in an industrial context to verify prototypical systems. One such application is an emergency call, which is automatically placed on the mobile phone net after the sensors of a car have detected that it was involved in a crash. The application runs on a system of several electronic control units (ECUs). The local application programs of the ECUs run on top of a simple real time operating system kernel like described in the OSEKTime standard. ECUs are connected via a FlexRay bus. We outline the structure of an overall correctness proof for such a parallel system from the gate to the kernel level for the communication system hardware one has to combine existing correctness proofs for components of time triggered architectures (e.g. clock synchronization) and arguments about hardware correctness into a single theorem. Results on processor, driver, and kernel correctness can to a large extent be imported from existing research in the Verisoft project. worst case execution time bounds are derived with advanced industrial tools based on abstract interpretation.