EECE 276 – Embedded Systems1EECE 276Embedded SystemsRequirements:Problems, types, real-timeEECE 276 – Embedded Systems2Requirement EngineeringO Capturing and documenting what the user wants. O Stages:» Preliminary study -> Feasibility report» Elicitation -> Domain model (interviews)» Definition -> Definition documents (writing it up)» Validation -> Specification documents (checking it)O Iterations:Elicitation <-> Definition <-> ValidationO Correctness is essential (hard to fix later)EECE 276 – Embedded Systems3Requirement Types1. Functional (what it does)2. External interfaces (how it connects)3. Performance (what is expected)4. Logical database (types of info used)5. Design constraints (standards, etc.)6. Attributes (reliability, availability, security, maintainability, portability)2-6: Non-functional RequirementsEECE 276 – Embedded Systems4Requirements for real-time systemsO Typical examples»Timing: – WCRT for every stimulus/response pair– Sustained data rates– Maximum latency » “Graceful degradation”» Availability, reliability, safety» Power consumption»…O To capture:» Formal “requirement” languagesEECE 276 – Embedded Systems5Formal Requirement LanguagesO “Formal methods” – mathematical, abstractO Why?» Consistency checking (Is it consistent?)» Model checking (Is a state reachable?)» Theorem proving (It is always true that …)O Example:1. If interrupt A arrives, the task B stops executing.2. Task A begins executing upon arrival of interrupt A.3. Either task A is executing and task B is not, or task B is executing and task A is not, or both are not executing.“interrupt A arrives” : p“task B is executing”: q“task A is executing”: r1. p implies q2. p implies r3. (r and not q) or (q and not r) or (not r and not q)EECE 276 – Embedded Systems6Consistency checkingO Are these consistent?O Check: build a truth-table with all the possible values for p,q,r, and see if 1.,2.,and 3. are true simultaneously. O Example: TACAS consistency checking• Terminal Area Collision Avoidance System by FAA1. p implies q2. p implies r3. (r and not q) or (q and not r) or (not r and not q)EECE 276 – Embedded Systems7Limitations of formal methodsO Can support verification but not validation» Verification: “the system is built right” (e.g. consistent) – w.r.t. ‘requirements’ » Validation: “the right system is built” (e.g. what the customer expects) – w.r.t. expectationsO We are verifying formulas but NOT the actual system!» We still need testing (which can never be complete…)O Difficulty in use…formal