Créer une présentation
Télécharger la présentation

Télécharger la présentation
## CPE555A: Real-Time Embedded Systems

- - - - - - - - - - - - - - - - - - - - - - - - - - - E N D - - - - - - - - - - - - - - - - - - - - - - - - - - -

**CPE555A:Real-Time Embedded Systems**Lecture 12 Ali Zaringhalam Stevens Institute of Technology 1 1**Outline**• Termination transition • Synchronous composition • Asynchronous composition • Model checking & formal verification CS555A – Real-Time Embedded Systems Stevens Institute of Technology CS555A – Real-Time Embedded Systems Stevens Institute of Technology 2**Termination Transition**• A termination transition is a transition that is enabled only when the refinements of the current state reach a final state. • Note that a state can have more than one refinement CS555A – Real-Time Embedded Systems Stevens Institute of Technology**Example 6.12**• Transition is: • Preemptive transition • Reset transition • Termination transition is taken when: • Refinement A transitions to doneA • Refinement B transitions to doneB Two refinements for the same actor. CS555A – Real-Time Embedded Systems Stevens Institute of Technology**Type checking: the outputs of A must be in the set of**acceptable inputs to B. CS555A – Real-Time Embedded Systems Stevens Institute of Technology**If the composition is asynchronous, then the output of A**must be buffered before B can use it. • If the composition is synchronous, then both A and B react. But the reaction of A precedes the reaction of A. So the output of A is available as input into B. (Programming analogy is a program which calls A. A in turn calls B on the stack and passes its output parameters as input.) CS555A – Real-Time Embedded Systems Stevens Institute of Technology**When a is present**A outputs b & self-transitions B outputs c and self-transition FSM remains in state (s1, s3) When a is absent, b is also absent (s1, s3) transition to (s2, s4) Both A and B react together If they didn’t, one could go thru (s2, s3) on the way from (s1, s3) to (s2, s4) Example: Synchronous Cascade (s1, s4) and (s2, s3) are unreachable from the init state. CS555A – Real-Time Embedded Systems Stevens Institute of Technology**Synchronous Cascade Example**CS555A – Real-Time Embedded Systems Stevens Institute of Technology**Traffic Light Extended FSM**What happens 60 seconds go by and there is no pedestrian? • Model is time-triggered • Assumes one reaction per second. • Default transition • Guard: true • Action: none Initial state. Re-init count=0. CS555A – Real-Time Embedded Systems Stevens Institute of Technology**Composition of Traffic Light With Pedestrian Light**The pedR & pedG signals control the pedestrian light signal. sigR from the traffic ligh FSM CS555A – Real-Time Embedded Systems Stevens Institute of Technology**Composition of two FSMs**sigR from traffic light FSM feeds the pedestrian FSM CS555A – Real-Time Embedded Systems Stevens Institute of Technology**State Enumeration**• State = (Traffic light state, pedestrian light state) • (red, red) • (red, green) • (yellow, red) • (yellow, green) • (green, red) • (green , green) • (pending, red) • (pending, green) • 61 distinct values for count variable • 56 distinct values for pcount variable • 8x61x56 distinct states • How may are reachable? State combinations in red font are not safe and must be made unreachable by design What guarantees that this state is not reached? CS555A – Real-Time Embedded Systems Stevens Institute of Technology**FSM Flattening: Reachable States**CS555A – Real-Time Embedded Systems Stevens Institute of Technology**What guarantees that this state is not reached?**Pedestrian transitions to red (pcount >= 55) before traffic light goes green (count >= 60). CS555A – Real-Time Embedded Systems Stevens Institute of Technology**Asynchronous Compositions**CS555A – Real-Time Embedded Systems Stevens Institute of Technology • In asynchronous compositions, FSMs representing actors react independently • Communication between actors is through exchange of messages • Rate of message production and message consumption may not be the same • Buffers are required to absorb differences in production/consumption rates 15**Firing Function & Firing Rule**CS555A – Real-Time Embedded Systems Stevens Institute of Technology Firing function maps a finite set of the input to output Firing rule is the condition for triggering the firing function (e.g., the number of tokens) 16**Issues In Asynchronous Compositions**CS555A – Real-Time Embedded Systems Stevens Institute of Technology • Buffer overflow • Can the actors continue to execute indefinitely with limited number of buffers? • Deadlock • Are there enough input tokens to satisfy the firing rule? • For a general FSM, these questions are undecidable • The Synchronous Dataflow (SDF) model puts constraints on FSM to address this 17**The SDF Model**CS555A – Real-Time Embedded Systems Stevens Institute of Technology • On firing, each FSM consumes a fixed number of tokens and fires a fixed number of tokens • Balance equation • qA*M=qB*N • Allows a schedule for unbounded execution with bounded buffers 18**Example**CS555A – Real-Time Embedded Systems Stevens Institute of Technology 19**Example**CS555A – Real-Time Embedded Systems Stevens Institute of Technology 20**Example**C consumes 2 tokens per transition but receives three tokens. Buffer overflow results. • qA=qB • 2qA=qC • qB=qC • qA= qB = qC= 0 CS555A – Real-Time Embedded Systems Stevens Institute of Technology 21**Observations**• A model that has no non-zero solution is referred to as “inconsistent” • If a model is inconsistent, it does not have an unbounded execution with bounded buffers • If a models is consistent, it can operate with a bounded buffer • But there is no guarantee of unbounded execution • There could be deadlock CS555A – Real-Time Embedded Systems Stevens Institute of Technology 22**Example**CS555A – Real-Time Embedded Systems Stevens Institute of Technology 23**CS555A – Real-Time Embedded Systems**Stevens Institute of Technology 24**Specification & Verification**CS555A – Real-Time Embedded Systems Stevens Institute of Technology • Specification: a precise statement of the design objectives and system behavior • Mathematical in a model • Typically English in published specs • Verification: does the system behave according to specification in the operating environment? 25**CS555A – Real-Time Embedded Systems**Stevens Institute of Technology 26**CS555A – Real-Time Embedded Systems**Stevens Institute of Technology 27**Example & Issues**• Consider the traffic light problem discussed earlier • Show that the FSM model guarantees that pedestrians are allowed to cross only when the traffic light is red • Two issues: • How do you express this property? • How do you prove it? CS555A – Real-Time Embedded Systems Stevens Institute of Technology**CS555A – Real-Time Embedded Systems**Stevens Institute of Technology 29**Given two or more interacting open systems, it is always**possible to define an equivalent closed system. CS555A – Real-Time Embedded Systems Stevens Institute of Technology 30**Example – 6.1**p1 F1 Any interconnection of actors can be modeled as a single side-by-side composition with feedback p2 F2 p1 F1 Composition p2 p3 F2 p4 F3 p1, p2,…..,pn Composition Composition CS555A – Real-Time Embedded Systems Stevens Institute of Technology**The composition step derives a closed system from the FSM**models of S and E. The behavior of the System S and Environment E are represented by interacting FSMs. Counterexample provides a trace where the property F is violated. CS555A – Real-Time Embedded Systems Stevens Institute of Technology 32**CS555A – Real-Time Embedded Systems**Stevens Institute of Technology 33**Atomic Formula Examples**A pure input is either present or absent. There is no associated value. CS555A – Real-Time Embedded Systems Stevens Institute of Technology 34**CS555A – Real-Time Embedded Systems**Stevens Institute of Technology 35**Implication**• By definition his proposition is False when p1 is True and p2 is False. The proposition is True otherwise. • The rationale for this truth table becomes clear when you consider how it is used in formal reasoning. • The mathematical definition of implication has nothing to do with cause and effect between hypothesis and conclusion. • p1 = you get 100 on your final exam • p2 = I will give you A • p1 => p2 • Suppose you get 100 (p1=True) but I give you a B (p2=False) • So p1 => p2 is False • p1 = it is Friday • p2 = (2+2=4) • Proposition: p1 => p2 • Suppose it is Thursday (p1=False) but 2+2 is still 4 (p2=True) • So p1 => p2 is True independent of the premise p1 • p1 = it is Friday • p2 = (2+6=10) • Proposition: p1 => p2 • Suppose it is Thursday (p1=False). 2+6 is not 10 (p2=False) • So p1 => p2 is True on any day other than Friday CS555A – Real-Time Embedded Systems Stevens Institute of Technology 36**Example:p1 => p2 if and only if !p2 => !p1**If !p2 => !p1 then p1 => p2 (sufficient condition) Suppose p1=true but p2=false Then !p2 => !p1 means that p1=false A contradiction This is the sufficient condition Suppose p1 => p2 but !p2 => p1 p2 = false means p1 = true But p1 => p2 means that p2 is true A contradiction Therefore !p2 => p1 is false So we must have !p2 => !p1 This is the necessary condition Conclusion: p1 => p2 if and only if !p2 => ! p1 CS555A – Real-Time Embedded Systems Stevens Institute of Technology 37**CS555A – Real-Time Embedded Systems**Stevens Institute of Technology 38**CS555A – Real-Time Embedded Systems**Stevens Institute of Technology 39**This does not mean G(p) which means it holds globally in**the trace (meaning in all states). • This is a statement about a trace, not the FSM. q0 is the first reaction in the trace. It is NOT the first state in the FSM. CS555A – Real-Time Embedded Systems Stevens Institute of Technology 40**Suffix is a tail of a trace beginning with some reaction and**including all subsequent reactions. See earlier definition: p holds for a trace if & only if it holds in q0 which is the first state in the trace. Next state. q1 comes after q0. CS555A – Real-Time Embedded Systems Stevens Institute of Technology 41**Globally: at any point in time; on every transition.**CS555A – Real-Time Embedded Systems Stevens Institute of Technology 42**Invariants**An invariant is a property of the system that never changes during the operation of the system If it is true at the beginning it remains true forever If it is false at the beginning it remains false forever Example of an invariant: There should be no pedestrian crossing when the traffic light is green CS555A – Real-Time Embedded Systems Stevens Institute of Technology 43**G(p) = TRUE in a trace if p = TRUE in every suffix of the**trace • But every suffix starts with a state • So G(p) means that p = TRUE in every state of the trace CS555A – Real-Time Embedded Systems Stevens Institute of Technology 44**This is a closed system consisting of the FSMs for the**traffic controller and the pedestrian arrival model. CS555A – Real-Time Embedded Systems Stevens Institute of Technology 45**Equivalent Propositions**CS555A – Real-Time Embedded Systems Stevens Institute of Technology**Flattened single FSM combining both FSMs**• Reachable states: • (red, crossing): 61 • (green, none): 61 • (pending, waiting): 60 • (yellow, waiting): 6 • Total: 188 188 Note that on this transition we increment count, rather than initializing it to 0. So the number of states in (pending, waiting) is 60 not 61. Visual inspection shows that in all states the property holds. The Crossing state happens only when Red. CS555A – Real-Time Embedded Systems Stevens Institute of Technology 47**Typically, the state graph of the FSM is not available.**• Build a composite FSM for System and Environment • This composite is a closed system with the formal description of its FSM: • States • Outputs • Update function: states -> states x outputs • Initial state • Note: there is no input as the composite is a closed system CS555A – Real-Time Embedded Systems Stevens Institute of Technology 48**Given d(s) as the set of possible next-states in s. The**DFS algorithm discovers all states reachable from the root initial state s0. • The property F=p can be checked in each state CS555A – Real-Time Embedded Systems Stevens Institute of Technology 49**The algorithm provides a path in the DFS graph from the**error state to the root initial state. CS555A – Real-Time Embedded Systems Stevens Institute of Technology 50