Introduction to Embedded SystemsWhen is a Design “Correct”?The Challenge of Dependable Software in Cyber-Physical SystemsSpecification, Verification, and ControlModel-Based Design: Verification & SynthesisTemporal LogicExample: Specification of the SpaceWire Protocol (European Space Agency standard)A Robot delivery service, with moving obstacles Propositional LogicPropositional LogicIn-Line QuizExecution Trace of a State MachinePropositional Logic on TracesLinear Temporal Logic (LTL)Linear Temporal Logic (LTL)First LTL Operator: G (Globally)Second LTL Operator: F (Eventually, Finally)Propositional Linear Temporal LogicEvery input x is eventually followed by an output yWhen is a Temporal Logic formula satisfied by a State Machine?Example 1Example 2Third LTL Operator: X (Next)Fourth LTL Operator: U (Until)Examples: What do they mean?Examples: Write in Temporal LogicTemporal Operators & RelationshipsSome Points to PonderA “Specification Mining” ApproachExercisesIntroduction to Embedded Systems Edward A. Lee & Alberto Sangiovanni Vincentelli EECS 149/249A Fall 2014 UC Berkeley Chapter 13: Specification & Temporal LogicUC Berkeley: 2 When is a Design “Correct”? A design is correct when it meets its specification (requirements) in its operating environment “A design without specification cannot be right or wrong, it can only be surprising!” Simply running a few tests is not enough! Many embedded systems are deployed in safety-critical applications (avionics, automotive, medical, …)UC Berkeley: 4 The Challenge of Dependable Software in Cyber-Physical Systems “In 1 of every 12,000 settings, the software can cause an error in the programming resulting in the possibility of producing paced rates up to 185 beats/min.” Today’s medical devices run on software… software defects can have life-threatening consequences. “the patient collapsed while walking towards the cashier after refueling his car […] A week later the patient complained to his physician about an increasing feeling of unwell-being since the fall.” [different device] [Journal of Pacing and Clinical Electrophysiology, 2004]UC Berkeley: 5 Specification, Verification, and Control Specification A mathematical statement of the design objective (desired properties of the system) Verification Does the designed system achieve its objective in the operating environment? Controller Synthesis Given an incomplete design, synthesize a strategy to complete the system so that it achieves its objective in the operating environmentUC Berkeley: 6 Model-Based Design: Verification & Synthesis Verifier Does model satisfy spec.? Model Requirements No Use error trace information to revise model/spec. Yes Synthesize system Need a formal way to write models and requirements (specification) so that an algorithm can process itUC Berkeley: 7 Temporal Logic  A formal way to express properties of a system over time  E.g., Behavior of an FSM or Hybrid System  Many flavors of temporal logic  Propositional temporal logic (we will study this)  Real-time temporal logic  Signal temporal logic  Amir Pnueli won ACM Turing Award, in part, for the idea of using temporal logic for specificationUC Berkeley: 8 Example: Specification of the SpaceWire Protocol (European Space Agency standard)UC Berkeley: 11 A Robot delivery service, with moving 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 obstaclesUC Berkeley: 12 Propositional Logic Atomic formulas: Statements about an input, output, or state of a state machine (at the current time). Examples: These are propositions (true or false statements) about a state machine with input or output x and state s. formula meaning x x is present x = 1 x is present and has value 1 s machine is in state sUC Berkeley: 13 Propositional Logic Propositional logic formulas: More elaborate statements about an input, output, or state of a state machine (at the current time). Examples: Here, p1 and p2 are either atomic formulas or propositional logic formulas. formula meaningUC Berkeley: 14 In-Line Quiz If p1 is false, what is the truth value of ?UC Berkeley: 15 Execution Trace of a State MachineUC Berkeley: 16 Propositional Logic on TracesUC Berkeley: 17 Linear Temporal Logic (LTL) LTL formulas: Statements about an execution trace Here, p is propositional logic formula and is either a propositional logic or an LTL formula. formula meaningUC Berkeley: 18 Linear Temporal Logic (LTL) LTL formulas: Statements about an execution trace Here, p is propositional logic formula and is either a propositional logic or an LTL formula. formula mnemonic proposition globally finally, future, eventually next state untilUC Berkeley: 19 First LTL Operator: G (Globally) G p for propositional formula p, is also termed an invariantUC Berkeley: 20 Second LTL Operator: F (Eventually, Finally)UC Berkeley: 21 Propositional Linear Temporal Logic LTL operators can apply to LTL formulas as well as to propositional logic formulas. E.g. Every input x is eventually followed by an output y Globally (at any point in time) If x occurs It is eventually followed by yUC Berkeley: 22 Every input x is eventually followed by an output y x holds y holdsUC Berkeley: 23 When is a Temporal Logic formula satisfied by a State Machine? A linear temporal logic (LTL) formula is satisfied by a state machine iff every trace of that state machine satisfies the LTL formula.UC Berkeley: 24 Example 1 Does the following temporal logic property hold for the state machine below? YesUC Berkeley: 25 Example 2 Does the following hold? No. What’s the error trace?UC Berkeley: 26 Third LTL Operator: X (Next)UC Berkeley: 27 Fourth LTL Operator: U (Until) Note: A variant, called “weak until,” written W, does not require p2 to eventually hold. This variant does.UC Berkeley: 30 Examples: What do they mean?  G F p p holds infinitely often  F G p Eventually, p holds henceforth  G( p => F q ) Every p is eventually followed by a q  F( p => (X X q) ) If p occurs, then on some occurrence it is followed by a q two reactions later Remember: Gp p holds in all states Fp p holds eventually Xp p holds in the next stateUC Berkeley: 31 Examples: