Introduction to Embedded SystemsA Robot delivery service, with obstacles Slide Number 7Reachability Analysis and Model CheckingFormal Verification Open vs. Closed SystemsModel Checking G pTraffic Light Controller ExampleComposed FSM for Traffic Light ControllerReachability Analysis Through Graph Traversal Depth-First Search (DFS)Generating counterexamplesGenerating counterexamplesExplicit State Model Checking ExampleExplicit State Model Checking ExampleExplicit State Model Checking ExampleExplicit State Model Checking ExampleExplicit State Model Checking ExampleExplicit State Model Checking ExampleExplicit State Model Checking ExampleExplicit State Model Checking ExampleExplicit State Model Checking ExampleThe Symbolic ApproachSymbolic Approach (Breadth First Search)The Symbolic Reachability AlgorithmSymbolic Model Checking ExampleSymbolic Model Checking ExampleSymbolic Model Checking ExampleSymbolic Model Checking ExampleSymbolic Model Checking ExampleSymbolic Model Checking ExampleSymbolic Model Checking ExampleSymbolic Model Checking ExampleAbstraction in Model CheckingAbstract Model for Traffic Light ExampleModel Checking Liveness PropertiesSuppose we have a Robot that must pick up multiple things, in any order Suppose we have a Robot that must pick up multiple things, in any order Variant: Suppose we have a Robot that must pick up multiple things, in a specified order Controller SynthesisController SynthesisIntroduction to Embedded Systems Edward A. Lee & Alberto Sangiovanni Vincentelli EECS 149/249A Fall 2014 UC Berkeley Chapter 15: Reachability Analysis6 A Robot delivery service, with obstacles φ = destination for robot Specification: The robot eventually reaches φ Suppose there are n destinations φ1, φ2, …, φn The new specification could be that The robot visits φ1, φ2, …, φn in that order φ Starting position of robot obstacles7 Graph of FSM modeling 2 trains and a bridge traffic controller. Is it possible for the trains to be on a collision path? [Moritz Hammer, Uni. Muenchen]8 Reachability Analysis and Model Checking Reachability analysis is the process of computing the set of reachable states for a system.  preceding problems can be solved using reachability analysis Model checking is an algorithmic method for determining if a system satisfies a formal specification expressed in temporal logic. Model checking typically performs reachability analysis.9 Formal Verification S E Φ Compose Verify Property System Environment YES [proof] NO counterexample M10 Open vs. Closed Systems A closed system is one with no inputs For verification, we obtain a closed system by composing the system and environment models11 Model Checking G p • Consider an LTL formula of the form Gp where p is a proposition (p is a property on a single state) • To verify Gp on a system M, need to enumerate all the reachable states and check that they all satisfy p. • The state space explored is typically represented as a directed graph called a state graph. • When M is a finite-state machine, this reachability analysis will always terminate (in theory). • The number of states may be prohibitively large consuming too much run-time or memory (the state explosion problem).12 Traffic Light Controller Example Property:13 Composed FSM for Traffic Light Controller This FSM has 189 states (accounting for different values of count) Property:14 Reachability Analysis Through Graph Traversal • Construct the state graph on the fly. • Start with initial state, and explore next states using a suitable graph-traversal strategy.15 Depth-First Search (DFS) Maintain 2 data structures: 1. Set of visited states R 2. Stack with current path from the initial state Potential problems for a huge graph?16 Generating counterexamples If the DFS algorithm finds the target (‘error’) state s, how can we generate a trace from the initial state to that state?17 Generating counterexamples If the DFS algorithm finds the target (‘error’) state s, how can we generate a trace from the initial state to that state? s s0 s1 Stack: s0 s1 s Simply read the trace off the stack18 Explicit State Model Checking Example R = { (red, crossing, 0) } Property:19 Explicit State Model Checking Example R = { (red, crossing, 0), (red, crossing, 1) } Property:20 Explicit State Model Checking Example R = { (red, crossing, 0), (red, crossing, 1), … (red, crossing, 60) } Property:21 Explicit State Model Checking Example R = { (red, crossing, 0), (red, crossing, 1), … (red, crossing, 60), (green, none, 0) } Property:22 Explicit State Model Checking Example R = { (red, crossing, 0), (red, crossing, 1), … (red, crossing, 60), (green, none, 0), (green, none, 1) } Property:23 Explicit State Model Checking Example R = { (red, crossing, 0), (red, crossing, 1), … (red, crossing, 60), (green, none, 0), (green, none, 1), …, (green, none, 60) } Property:24 Explicit State Model Checking Example R = { (red, crossing, 0), (red, crossing, 1), … (red, crossing, 60), (green, none, 0), (green, none, 1), …, (green, none, 60), (yellow, waiting, 0) } Property:25 Explicit State Model Checking Example R = { (red, crossing, 0), (red, crossing, 1), … (red, crossing, 60), (green, none, 0), (green, none, 1), …, (green, none, 60), (yellow, waiting, 0), … (yellow, waiting, 5) } Property:26 Explicit State Model Checking Example R = { (red, crossing, 0), (red, crossing, 1), … (red, crossing, 60), (green, none, 0), (green, none, 1), …, (green, none, 60), (yellow, waiting, 0), … (yellow, waiting, 5), (pending, waiting, 1), …, (pending, waiting, 60) } Property:27 The Symbolic Approach • Rather than exploring new reachable states one at a time, we can explore new sets of reachable states  However, we only represent sets implicitly, as Boolean functions • Set operations can be performed using Boolean algebra • Represent a finite set of states S by its characteristic (Boolean) function fS  fS (x) = 1 iff x ∈ S • Similarly, the state transition function δ yields a set δ(s) of next states from current state s, and so can also be represented using a characteristic Boolean function for each s.28 . . . Qk Q2 Symbolic Approach (Breadth First Search)  Generate the state graph by repeated application of transition function (δ)  If the goal state reached, stop & report success. Else, continue until all states are seen. Q1 Q0 δ s29 The Symbolic Reachability