EE249Fall071Models 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 networksEE249Fall072Finite 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)EE249Fall073FSM 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 keyEE249Fall074FSM ExampleKEY_ON => START_TIMEREND_TIMER_5 => ALARM_ONKEY_OFF orBELT _ON =>END_TIMER_10 orBELT_ON orKEY_OFF => ALARM_OFFIf no condition is satisfied, implicit self-loop in the current stateWAITALARMOFFEE249Fall075FSM 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δ : 2I× S → S e.g. δ( { KEY_OFF }, WAIT ) = OFFλ : 2I× S → 2Oe.g. λ ( { KEY_ON }, OFF ) = { START_TIMER }Set of all subsets of I (implicit “and”)All other inputs are implicitly absentEE249Fall076Non-deterministic FSMs δ and λ may be relations instead of functions:δ ⊆ 2I× S × S 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)implicit “and” implicit “or”EE249Fall077• E.g. error checking first partially specified:• Then completed as even parity:NDFSM: incomplete specificationBIT or not BIT => BIT or not BIT =>BIT or not BIT => ERRBIT or not BIT =>...SYNC =>BIT =>not BIT =>not BIT => ERR...SYNC =>not BIT =>...not BIT =>BIT =>not BIT =>BIT =>BIT => BIT => ERR 0 1 7 8p1 p7d7d10 8EE249Fall07NDFSM: unknown behavior• Modeling the environment• Useful to:– optimize (don’t care conditions)– verify (exclude impossible cases)• E.g. driver model:• Can be refined– E.g. introduce timing constraints– (minimum reaction time 0.1 s)s0=> KEY_ON or KEY_OFF orBELT_ONEE249Fall079NDFSM: time range• Special case of unspecified/unknown behavior, but so common to deserve special treatment for efficiency• E.g. delay between 6 and 10 s01 2 3 456789START => SEC =>SEC => ENDSEC => SEC =>SEC =>SEC =>SEC =>SEC =>SEC =>START =>SEC => ENDSEC => ENDSEC => ENDEE249Fall07NDFSMs and FSMs• Formally FSMs and NDFSMs are equivalent – (Rabin-Scott construction, Rabin ‘59)• In practice, NDFSMs are often more compact– (exponential blowup for determinization)s1s2s3s1s2,s3aabac as3bas2cbas1,s3cacEE249Fall0711Finite 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)EE249Fall0712Modeling 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?EE249Fall0713FSM 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 + timer01 2 3 456789START_TIMER =>START_TIMER =>SEC =>SEC => END_10_SECSEC => SEC =>SEC =>END_5_SECSEC =>SEC =>SEC =>SEC =>EE249Fall0714FSM CompositionOFF, 0 WAIT, 1KEY_ON and START_TIMER => START_TIMERmust be coherentWAIT, 2SEC and not (KEY_OFF or BELT_ON) =>OFF, 1not SEC and (KEY_OFF or BELT_ON) =>OFF, 2SEC and (KEY_OFF or BELT_ON) =>BeltControlTimerEE249Fall0715FSM CompositionGiven M1 = ( I1, O1, S1, r1, δ1, λ1) and M2= ( I2, O2, S2, r2, δ2, λ2)Find the compositionM = ( I, O, S, r, δ, λ )given a set of constraints of the form:C = { ( o, i1, … , in) : o is connected to i1, … , in}EE249Fall0716FSM Composition• Unconditional product M’ = ( I’, O’, S’, r’, δ’, λ’ )– I’ = I1 U I2– O’ = O1U O2– S’ = S1x S2– r’ = r1x r2δ’ = { ( A1, A2, s1, s2, t1, t2) : ( A1, s1, t1) ε δ1and ( A2, s2, t2) ε δ2}λ’ = { ( A1, A2, s1, s2, B1, B2) : ( A1, s1, B1) ε λ1and ( A2, s2, B2) ε λ2}• Note:– A1 ⊆ I1, A2⊆ I2, B1⊆ O1, B2⊆ O2– 2X U Y= 2Xx 2YEE249Fall0717FSM Composition• Constraint applicationλ = { ( A1, A2, s1, s2, B1, B2) ε λ’ : for all ( o, i1, … , in) ε C o ε B1U B2if and only if ijε A1U A2for all j }• The application of the constraint rules out the cases where the connected input and output have different values (present/absent).EE249Fall0718I = I1 ∪ I2 O = O1 ∪ O2S = S1 × S2Assume 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. i3is in input pattern iff o2is in output patternFSM CompositionFSM1FSM2i1i2i3o1o2EE249Fall0719• Problem: what if there is a cycle?– Moore machine: δ depends on input and state, λ only on statecomposition is always well-defined– Mealy machine: δ and λ depend on input and state composition may be undefinedwhat if λ1( { i1}, s1) = { o1} but o2∉ λ2( { i3}, s2 ) ?• Causality analysis in Mealy FSMs (Berry ‘98)FSM CompositionFSM1FSM2i1i3o1o2EE249Fall0720Moore 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 latchedEE249Fall0721Moore vs. Mealy• Mealy
View Full Document
Unlocking...