SYDIC-Training Course on
System-Level Design of Embedded Systems
Part II: Lab exercise (8 hours)
The lab exercises will illustrate the use of modeling techniques and the associated formal verification tools. The focus is on model checking, one of the well-established automatic approaches in formal methods. Model checking is used to determine whether the model of a system satisfies a set of required properties. The software tools to be used include the model checkers SMV and Uppaal.
Exercise 1: Model Checking of Finite State Systems
The first exercise shows how to describe finite state systems using the input language of the tool SMV and also how to formalize required properties in the temporal logic CTL (Computation Tree Logic). Having as input the system description and the desired properties in a formal notation, the model checker answers whether the model of the system satisfies the given properties. If not, counter-examples are generated that can be further used as diagnosis information.
Exercise 2: Model Checking of Continuous-Time Systems
The second exercise illustrates how to represent, validate, and verify real-time systems based on timed automata. A timed automaton is a finite automaton enhanced with a set of real-valued clocks that may model systems where time advances continuously. Uppaal is a model checker that allows to graphically specify continuous-time systems and to perform their validation/verification. The logic for specifying properties is TCTL (Timed CTL), a real-time extension of CTL that allows to inscribe subscripts on the temporal operators to limit their scope in time.
Back to the course homepage
