"Parametric Verification of Real-Time systems using LPMC"
This lecture addresses formal verification of Real-Time systems using
model-checking. The three core elements of the general approach are the
modeling language (a timed automaton language), the specification language a
branching time logic) and the verification process itself, which checks whether
a model expressed in the timed automaton language "models" a specification in
the logic language. The lecture will briefly address timed automata, timed
logics and general approaches for real-time model checking.
Next our approach will be presented in some detail, including the syntax and
semantics of the timed automaton language XTG, the logic TCTL and a sketch of
the model-checking algorithms. The second part of the lecture will address the
application of the verification toolbox through some case studies, including a
case study on parts of the IEEE 1394a standard.
In the lecture we address the verification of the root contention protocol.
Timing parameters play an essential role in this protocol. Only for certain
parameter values, the protocol will end correctly, in other cases it will
fail. We will show that parametrical model checking will deliver the parameter
relations and timing intervals under which the protocol will behave correctly.
