Petri Nets 2010, ACSD 2010 - Braga, Portugal


ACSD 2010

Braga, Portugal, June 21-25, 2010
Petri Nets 2010, ACSD 2010 - Braga, Portugal

Invited Speaker: Kim Guldstrand Larsen

Verification, Compositionality and Refinements for Real-Time Systems


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