Heterogeneous Reactive Models and Correct-by-Construction DeploymentAlberto L. Sangiovanni-VincentelliWith A. Benveniste, L. Carloni and P. CaspiSynchronous Model•A synchronous process evolves according to an infinite sequence of successive reactions•The parallel composition of two processes is the conjunction of their reactions– product of automata, FSM connection Pi ≡ RiP1||P2 ≡ (R1∧R2)ωω• Pi: synchronous process• Ri: set of all possible reactions of process Pi• ω: indicates non-terminating reactionsSynchronous Model• Foundation of Synchronous Languages– Esterel, Lustre, Signal• Pervasive in Mathematics and Engineering– Discrete-Dynamic Control Systems– Digital Integrated Circuit Design• When composition is possible, we can reason formally on the properties of the composite system based on the properties of its components– Notice: generally, functional systems are not closed under concurrent compositionSynchronous Assumption• Communication Delay is negligible w.r.t. Computation Delay• The system transitionsbetween a reaction and the other instantaneouslyand the communication of the values from the outputs of a component to the inputs of another takeszero timeloop each tickread inputscompute next statewrite outputsend loopDistributed Nature of Implementations• in hardware– with DSM technologies, the chip becomes a distributed system– wire delays not negligible w.r.t. transistor delays– on-chip communication latency is hard to estimate• in (embedded) software– applications with distributed nature badly matching the synchronous assumption• real-time safety critical embedded systems in avionics and automotive industries• industrial plants, transportation/power networks– large variations in computation/communication times– hard to maintain a global notion of timeDSM: Percentage of Reachable Die020406080100250 180 130 100 80 6016 clock cyles8 clock cycles4 clock cycles2 clock cycles1 clock cycle•“For a 60 nanometer process a signal can reach only 5% of the die’s length in a clock cycle”[D. Matzke,1997]• Cause: Combination of high frequencies and slower wiresElectronics for the Car: A Distributed SystemInformationSystemsTelematicsFault TolerantBody ElectronicsBodyFunctionsFail SafeFaultFunctionalBody ElectronicsDriving and VehicleDynamic FunctionsMobile Communications NavigationFireWallAccess to WWWDABGateWayGateWayTheft warningDoor ModuleLight ModuleAirConditioningShift by WireEngineManagementABSSteer by WireBrake by WireMOSTMOSTFirewireFirewireCANCANLinLinCANCANTTCANTTCANFlexRayFlexRayToday, morethan 80Microprocessors and millions of lines of codeOutline• A common formal framework for the study of– Models of Computation (MOCs)– synchronous, asynchronous, GALS– event absence in modeling distributed systems–the de-synchronization problem• De-synchronization of embedded software programs• properties of endochrony and isochrony• Concluding Remarks• Event : a member of V x T, •V: set of values, T: set of tags• Signal : a set of events • s = { (v1, t1), (v2, t2), … , (vk, tk) } The Tagged-Signal Model [Lee & Sangiovanni ‘96]• Process : a subset P of the set of N-tuples of signals• Behavior : a tuple of signals b = (s1, s2, …, sN) which satisfies a process P• System : a composition of processes P1,… ,PM• (i.e. the intersection of their behaviors)More on Tags• Tags can be a mechanism to express time– across various levels of abstraction• Logical Time in initial specification• Physical (“Real”) Time in final implementation• But tags are essentially a tool to express constraints– Coordination constraints • among events of the same signal• among signals of the same behaviorsThe “Absent-Value” Event ( ⊥ )uvtagt2t1 t4t3 t6t5 t8t7 t10t9 t12t11 t14t134 -2 5 3-1 20 46 21 1 1 0 1 1 1 1• a signal s is present at tag t when∃e=(t,d) ∈ s | d≠⊥• otherwise, s is absent at tag tAssumption on the Tags of a Signal• For any tag t ∈ T, each signal s in the system has at most one event, i.e.∀b∈B, ∀s∈b, ¬[ ∃e1∈s ∃e2∈s | tag(e1) = tag(e2) ]• This implies –a total order < among the tags of a signal–a total order < among the events of a signalOrdering Tags in a Process• Generally, process tags are not ordered• When used to express causality relations among signals, it is common to assume a partial order ≤t < t’ when t ≤ t’ and t ≠ t’• Timed System: the set Tof tags (timestamps) is a totally ordered set. – the ordering among the timestamps of a signal s induces a natural order on the set of events of s∀ t,t’ ( t ≠ t’ ⇒ (t < t’ or t > t’) )Tags• Assumption: the tag set T is partially orderedt < t’ ⇔ ( t ≤ t’ ∧ t≠t’ )• A clock h is a non-decreasing map N → T• Modeling Heterogeneity: the set T of tags can be adjusted to account for different class of systems (synchronous, asynchronous, timed,…)TAGS generalize and heterogeneizeXYUXZ1,t11,s12,s23,t3 4,t44,s4a TAG consisting of the triple (reaction, phys.time, causality)TAGS generalize and heterogeneizeXYUt1 t2 t3 t423• TAGS can belong to any partially ordered set – tags can index reactions, can be real time R, can encode causality, can do both, etc.• TAGS can be tuples – desynchronization can be generalized to erasing some components of the tag; yields morphisms of tag sets, we denote them by r, a• different TAG sets can be used for different systems – we can mix synchronous systems (with tag set N) and asynchronous ones (with trivial tag set), and moreSynchronous Systems• Time change ρ any bijective and strictly-increasing function ρ: T → T•Rt: set of all time changes over T•Pis stuttering-invariantifffor every behavior b∈P and every time change ρ∈Rtbρ ∈ P ⇔ { (t,d) ∈ b ⇔ (ρ(t),d) ∈ bρ }Stuttering-invariance → invariance under time changeSynchronous Events, Behaviors, Processes• Synchronous Events have the same tag• Synchronous Signals s1≈s2 when• Synchronous Behaviors• Synchronous Processes∀ei∈s1, ∃ej∈s2 (ei≈ej) and∀ek∈s2, ∃el∈s1 (ek≈el)b1≈b2 when ∀si∈b1, ∀sj∈b2, (si≈sj)P1≈P2 when ∀bi∈B(P1), ∀bj∈B(P2), (bi≈bj)s1≈s2 when tag(s1) = tag(s2)Synchronous Systems• Stand-alone synchronous behavior b when b≈b• Synchronous process (system) P when P≈P• In a synchronous system P, every signal is synchronous with every other signal•
View Full Document
Unlocking...