Heterogeneous Reactive Models and Correct by Construction Deployment Alberto L Sangiovanni Vincentelli With A Benveniste L Carloni and P Caspi Synchronous Model Pi synchronous process Pi Ri Ri set of all possible P1 P2 R1 R2 reactions of process Pi indicates non terminating reactions 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 Synchronous 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 composition Synchronous Assumption Communication Delay is negligible w r t Computation Delay The system transitions between a reaction and the other instantaneously and the communication of the values from the outputs of a component to the inputs of another takes zero time loop each tick read inputs compute next state write outputs end loop Distributed 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 time DSM Percentage of Reachable Die 100 80 16 clock 60 cyles 8 clock cycles 40 4 clock cycles 2 clock cycles 20 1 clock cycle 0 250 180 130 100 80 60 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 wires Fault Tolerant Mobile Communications MOST Firewire Fail Safe CAN Lin Navigation Access to WWW DAB Fire Wall Theft warning Air Conditioning Door Module Gate Way Light Module ABS CAN TTCAN Gate Way Fault Functional Body Electronics Body Functions Body Electronics Driving and Vehicle Dynamic Functions Information Systems Telematics Electronics for the Car A Distributed System Steer by Wire FlexRay Shift by Wire Engine Management Brake by Wire Today more than 80 Microprocessors and millions of lines of code Outline 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 The Tagged Signal Model Lee Sangiovanni 96 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 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 behaviors The Absent Value Event a signal s is present at tag t when e t d s d otherwise s is absent at tag t t1 t2 t3 t4 t5 t6 t7 t8 t9 t10 t11 t12 t13 t14 u 4 2 5 1 3 0 2 6 4 2 v 1 1 1 0 1 1 1 1 tag Assumption 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 signal Ordering 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 T of tags timestamps is a totally ordered set t t t t t t or t t the ordering among the timestamps of a signal s induces a natural order on the set of events of s Tags Assumption the tag set T is partially ordered t 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 heterogeneize X X Y U 1 t1 3 t3 4 t4 Z 1 s1 2 s2 4 s4 a TAG consisting of the triple reaction phys time causality TAGS generalize and heterogeneize X Y U t1 t2 2 3 t3 t4 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 more Synchronous Systems Time change any bijective and strictlyincreasing function T T Rt set of all time changes over T P is stuttering invariant iff for every behavior b P and every time change Rt b P t d b t d b Stuttering invariance invariance under time change Synchronous Events Behaviors Processes Synchronous Events have the same tag s1 s2 when tag s1 tag s2 s1 s2 when ei s1 ej s2 ei ej and Synchronous Signals ek s2 el s1 ek el Synchronous Behaviors b1 b2 when si b1 sj b2 si sj Synchronous Processes P1 P2 when bi B P1 bj B P2 bi bj 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 Equivalently for each tag t a signal has exactly one corresponding event b B P s b t T P e s tag e t Synchronous Systems Example tag w x y z t1 1 1 0 0 t2 0 3 2 0 t3 1 5 2 4 t4 0 7 6 0 t5 1 9 6 8 t6 t7 t8 0 1 0 11 13 15 10 10 14 4 12 8 3 processes 4 signals y P Q w x z R Synchronous Languages Signal Simplicity of synchronous assumption plus the power of concurrency in system specification Notion of clock of a variable a Boolean meta variable tracking the absence presence of a value for the corresponding variable clocks equivalence classes of simultaneously present variables The Signal compiler uses clock calculus to 1
View Full Document
Unlocking...