Corso di Sistemi in Tempo Reale
Laurea in Ingegneria dell‘Automazione
a.a. 2008-2009
Paolo Pagano ([email protected])
Today’s topic
• First day (23rd)
– Basics of FSM (slides by prof. Lipari)
– The Uppaal platform
– Formal verification
Paolo Pagano - Embedded Systems
2/13
Finite State Machines
Credits: John Favaro
([email protected])
Paolo Pagano - Embedded Systems
3/13
Finite State Machines
Paolo Pagano - Embedded Systems
4/13
Finite State Machines
Paolo Pagano - Embedded Systems
5/13
Finite State Machines
Paolo Pagano - Embedded Systems
6/13
Finite State Machines
Paolo Pagano - Embedded Systems
7/13
Uppaal model
• Uppaal
(www.uppaal.com) is a
tool box for validation (via
graphical simulation) and
verification (via automatic
model-checking) of FSM
driven systems. It
consists of two main
parts:
– a graphical user interface;
– a model-checker engine.
Paolo Pagano - Embedded Systems
8/13
FSM design and implementation
• We model a panel of
leds and buttons
making use of a set
of FSMs;
• Let’s verify this
simple system
making use of
Uppaal inner engine.
Transitions
States
Paolo Pagano - Embedded Systems
Conditions
9/13
Formal verification (1/2)
Paolo Pagano - Embedded Systems
10/13
Modeling OS-entities like Mutexes
Paolo Pagano - Embedded Systems
11/13
Formal verification (2/2)
Paolo Pagano - Embedded Systems
12/13