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)