Verification, Compositionality and Refinements for Real-Time Systems

Abstract

We present a complete framework for specifying and verifying real-time systems using Timed I/O Automata as the specification formalisms, with the semantics expressed in terms of Timed I/O Transition Systems. We demonstrate the use of the model checking engine of the tool UPPAAL for verifying safety and liveness properties. In addition we provide constructs for refinement, consistency checking, logical and structural composition, and quotient of specifications – all indispensable ingredients of a compositional design methodology. The theory is implemented in the new tool ECDAD on top of the UPPAAL engine for timed games. The new compositional approach allows for scalability of verification.

09:00-10:00 Wednesday, 23 June 2010