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 1 EE249Fall07 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 2 EE249Fall07 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 3 EE249Fall07 FSM Example KEY ON START TIMER WAIT OFF KEY OFF or BELT ON END TIMER 10 or BELT ON or KEY OFF ALARM OFF END TIMER 5 ALARM ON ALARM If no condition is satisfied implicit self loop in the current state 4 EE249Fall07 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 2O e g KEY ON OFF START TIMER 5 EE249Fall07 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 6 EE249Fall07 NDFSM incomplete specification E g error checking first partially specified BIT or not BIT 0 BIT or not BIT ERR BIT or not BIT 1 7 8 BIT or not BIT SYNC Then completed as even parity not BIT BIT 0 p1 not BIT BIT d1 BIT not BIT p7 BIT ERR not BIT not BIT ERR d7 8 BIT SYNC 7 EE249Fall07 NDFSM unknown behavior Modeling the environment Useful to optimize don t care conditions verify exclude impossible cases E g driver model s0 KEY ON or KEY OFF or BELT ON Can be refined E g introduce timing constraints minimum reaction time 0 1 s EE249Fall07 NDFSM time range Special case of unspecified unknown behavior but so common to deserve special treatment for efficiency E g delay between 6 and 10 s START SEC 1 SEC 2 SEC 3 4 SEC START SEC END SEC END 9 0 5 SEC END SEC END 6 SEC SEC 8 9 SEC 7 SEC EE249Fall07 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 c c a s1 s3 s3 a a c b s2 c b s2 s3 s3 a a a b s2 EE249Fall07 Finite State Machines Advantages Easy to use graphical languages Powerful algorithms for synthesis SW and HW verification Disadvantages Sometimes over specify implementation sequencing is fully specified Number of states can be unmanageable Numerical computations cannot be specified compactly need Extended FSMs 11 EE249Fall07 Modeling Concurrency Need to compose parts described by FSMs Describe the system using a number of FSMs and interconnect them How do the interconnected FSMs talk to each other 12 EE249Fall07 FSM Composition Bridle complexity via hierarchy FSM product yields an FSM Fundamental hypothesis all the FSMs change state together synchronicity System state Cartesian product of component states state explosion may be a problem E g seat belt control timer START TIMER SEC 1 SEC 2 SEC 3 4 START TIMER 0 13 SEC END 10 SEC SEC 9 SEC 8 SEC 7 SEC END 5 SEC SEC 6 5 EE249Fall07 FSM Composition KEY ON and START TIMER must be coherent START TIMER OFF 0 WAIT 1 not SEC and KEY OFF or BELT ON OFF 1 SEC and not KEY OFF or BELT ON WAIT 2 SEC and KEY OFF or BELT ON OFF 2 Belt Timer Control 14 EE249Fall07 FSM Composition Given M1 I1 O1 S1 r1 1 1 and M2 I2 O2 S2 r2 2 2 Find the composition M I O S r given a set of constraints of the form C o i1 in o is connected to i1 in 15 EE249Fall07 FSM Composition Unconditional product M I O S r I I1 U I2 O O1 U O2 S S1 x S2 r r1 x r2 A1 A2 s1 s2 t1 t2 and A1 s1 t1 1 A2 s2 t2 2 A1 A2 s1 s2 B1 B2 A1 s1 B1 1 and A2 s2 B2 2 Note A1 I1 A2 I2 B1 O1 B2 O2 2X U Y 2X x 2Y 16 EE249Fall07 FSM Composition Constraint application A1 A2 s1 s2 B1 B2 for all o i1 in C and only if ij A1 U A2 for all j o B1 U B2 if The application of the constraint rules out the cases where the connected input and output have different values present absent 17 EE249Fall07 FSM Composition I I1 I2 i1 O O1 O2 i2 FSM1 S S1 S2 FSM2 o2 o1 i3 Assume that o1 O1 i3 I2 o1 i3 communication and are such that e g for each pair 1 i1 s1 t1 1 i1 s1 o1 2 i2 i3 s2 t2 2 i2 i3 s2 o2 we have i1 i2 i3 s1 s2 t1 t2 i1 i2 i3 s1 s2 o1 o2 i e i3 is in input pattern iff o2 is in output pattern 18 EE249Fall07 FSM Composition Problem what if there is a cycle Moore machine depends on input and state only on state composition is always well defined Mealy machine and depend on input and state composition may be undefined what if 1 i1 s1 o1 but o2 2 i3 s2 i1 FSM1 o1 i3 FSM2 o2 Causality analysis in Mealy FSMs Berry 98 19 EE249Fall07 Moore vs Mealy Theoretically same computational power almost In practice different characteristics Moore machines non reactive response delayed by 1 cycle easy to compose always well defined good for implementation software is always slow hardware is better when I O is latched 20 EE249Fall07 Moore vs Mealy Mealy machines reactive 0 response time hard to compose problem with combinational cycles problematic for implementation software must be fast enough synchronous hypothesis may be needed in hardware for speed 21 EE249Fall07 Hierarchical FSM models Problem how to reduce the size of the representation Harel s classical papers on StateCharts language and bounded concurrency model 3 orthogonal exponential reductions Hierarchy state a encloses an FSM being in a means FSM in a is active states of a are called OR states a odd a1 a2 even used to model pre emption and exceptions Concurrency two or more FSMs are simultaneously active done error recovery states are called AND states Non determinism 22 used to abstract behavior EE249Fall07 The vending machine A machine that sells coffee Accepts one dollar d1 bills Maximum two dollars Quarters change Sells two products Small coffee for 1 Large coffee for 1 25 23 EE249Fall07 Denotational description …
View Full Document
Unlocking...