Post on 13-Dec-2015
transcript
Corso di Sistemi in Tempo RealeLaurea in Ingegneria dell‘Automazione
a.a. 2008-2009
Paolo Pagano (p.pagano@sssup.it)
Paolo Pagano - Embedded Systems 2/13
Today’s topic
• First day (23rd)– Basics of FSM (slides by prof. Lipari)– The Uppaal platform– Formal verification
Paolo Pagano - Embedded Systems 3/13
Finite State Machines
Credits: John Favaro (john@favaro.net)
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
Finite State Machines
Paolo Pagano - Embedded Systems 8/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 9/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.
States
Transitions
Conditions
Paolo Pagano - Embedded Systems 10/13
Formal verification (1/2)
Paolo Pagano - Embedded Systems 11/13
Modeling OS-entities like Mutexes
Paolo Pagano - Embedded Systems 12/13
Formal verification (2/2)