Outline Part 3 Models of Computation FSMs Discrete Event Systems CFSMs Data Flow Models Petri Nets The Tagged Signal Model 1 Design From an idea build something that performs a certain function Never done directly some aspects are not considered at the beginning of the development the designer wants to explore different possible implementations in order to maximize or minimize a cost function Models can be used to reason about the properties of an object 2 Formalization Model of a design with precise unambiguous semantics Implicit or explicit relations inputs outputs and possibly state variables Properties Cost functions Constraints Formalization of Design Environment closed system of equations and inequalities over some algebra 3 Models of Computation And There are More Continuous time ODEs Spatial temporal PDEs Discrete time Rendezvous Synchronous Reactive Dataflow Each of these provides a formal framework for reasoning about certain aspects of embedded systems Tower of Babel Bruegel 1563 4 Model Of Computation A MoC is a framework in which to express what sequence of actions must be taken to complete a computation Examples Finite State Machine Turing Machine differential equation Why different models Different models different properties Turing complete models are too powerful Some problems may be undecidable MOC needs to be powerful enough for application domain have appropriate synthesis and validation algorithms 5 Usefulness of a Model of Computation Expressiveness Generality Simplicity Compilability Synthesizability Verifiability The Conclusion One way to get all of these is to mix diverse simple models of computation while keeping compilation synthesis and verification separate for each MoC To do that we need to understand these MoCs relative to one another and understand their interaction when combined in a single system design 6 Common Models of Computation Finite State Machines finite state no concurrency nor time Data Flow Partial Order Concurrent and Determinate Stream of computation Discrete Event Global Order embedded in time Continuous Time The behavior of a design in general is described by a composition 7 Notion of Time 8 Control versus Data Flow Fuzzy distinction yet useful for specification language model synthesis scheduling optimization validation simulation formal verification Rough classification control don t know when data arrive quick reaction time of arrival often matters more than value data data arrive in regular streams samples value matters most 9 Control versus Data Flow Specification synthesis and validation methods emphasize for control event reaction relation response time Real Time scheduling for deadline satisfaction priority among events and processes for data functional dependency between input and output memory time efficiency Dataflow scheduling for efficient pipelining all events and processes are equal 10 Telecom MM applications Heterogeneous specifications including data processing control functions Data processing e g encryption error correction computations done at regular often short intervals efficiently specified and synthesized using DataFlow models Control functions data dependent and real time say when and how data computation is done efficiently specified and synthesized using FSM models Need a common model to perform global system analysis and optimization 11 Reactive Real time Systems Reactive Real Time Systems React to external environment Maintain permanent interaction Ideally never terminate timing constraints real time As opposed to transformational systems interactive systems 12 09 1999 12 Models Of Computation for reactive systems We need to consider essential aspects of reactive systems time synchronization concurrency heterogeneity Classify models based on how specify behavior how specify communication implementability composability availability of tools for validation and synthesis 13 Models Of Computation for reactive systems Main MOCs Communicating Finite State Machines Dataflow Process Networks Petri Nets Discrete Event Abstract Codesign Finite State Machines Main languages StateCharts Esterel Dataflow networks 14 Finite State Machines Functional decomposition into states of operation Typical domains of application control functions protocols telecom computers Different communication mechanisms synchronous classical FSMs Moore 64 Kurshan 90 asynchronous CCS Milner 80 CSP Hoare 85 15 FSM Example Informal specification If the driver turns on the key and does not fasten the seat belt within 5 seconds then an alarm beeps for 5 seconds or until the driver fastens the seat belt or until the driver turns off the key 16 FSM Example KEY ON START TIMER OFF WAIT KEY OFF or END TIMER 5 BELT ON ALARM ON END TIMER 10 or BELT ON or ALARM KEY OFF ALARM OFF If no condition is satisfied implicit self loop in the current state 17 FSM Definition FSM I O S r I KEY ON KEY OFF BELT ON END TIMER 5 END TIMER 10 O START TIMER ALARM ON ALARM OFF S OFF WAIT ALARM r OFF Set of all subsets of I implicit and All other inputs are implicitly absent 2I S S e g KEY OFF WAIT OFF 2I S O e g KEY ON OFF START TIMER 18 Non deterministic FSMs and may be relations instead of functions 2I S S implicit and implicit or e g KEY OFF END TIMER 5 WAIT OFF ALARM 2I S 2O Non determinism can be used to describe an unspecified behavior incomplete specification an unknown behavior environment modeling 19 NDFSM incomplete specification E g error checking first partially specified BIT or not BIT BIT or not BIT ERR BIT or not BIT 0 1 7 BIT or not BIT Then completed as even parity not BIT 0 BIT p1 not BIT BIT d1 BIT SYNC Could be implemented as CRC later not BIT not BIT 8 p7 BIT ERR not BIT not BIT ERR d7 8 BIT SYNC 20 NDFSM unknown behavior Modeling the environment Useful to optimize don t care conditions verify exclude impossible cases E g driver model KEY ON or KEY OFF or BELT ON Can be refined E g introduce timing constraints s0 minimum reaction time 0 1 s 12 09 1999 21 NDFSM time range Special case of unspecified unknown behavior but so common to deserve special treatment for efficiency E g undetermined delay between 6 and 10 s START SEC SEC SEC 1 3 4 SEC START SEC END 9 SEC 0 SEC END SEC SEC END END 8 SEC 6 7 5 SEC SEC 22 NDFSMs and FSMs Formally FSMs and NDFSMs are equivalent Rabin Scott construction Rabin 59 In practice NDFSMs are often more compact exponential blowup for determinization s1 s1 a a b s a c s3 c s1 s3 c a c a s s3 a b s3 b a s 12 09 1999 23
View Full Document
Unlocking...