Necessary and sufficient conditions for deterministic desynchronization

Synchronous reactive formalisms associate concurrent behaviors to precise schedules on global clock(s). This allows a non-ambiguous notion of "absent" signal, which can be reacted upon. But in desynchronized (possibly distributed) implementations, absent values must be explicitely exchanged, unless behaviors were already provably independent and asynchronous (a property formerly introduced as endochrony). We provide further criteria restricting "reaction to absence" to allow correct desynchronized implementation. We also show that these criteria not only depend on the desired correctness properties, but also on the desired structure of the implementation. Categories and Subject Descriptors C.3 [Special-Purpose and Application-Based Systems]: RealTime and Embedded Systems; D.3.1 [Formal Definitions and Theory]: Semantics Keywords Desynchronization, GALS, Endochrony, Execution machine, Correctness, Determinism, Reaction to signal absence, Kahn process networks

• Type: Conference
• Year: 2007
• Where: EMSOFT
• Authors: Dumitru Potop-Butucaru, Robert de Simone, Yves Sorel
• Keywords: Concurrent Behaviors, Correct Desynchronized Implementation, EMSOFT 2007, Software Engineering, Synchronous Reactive Formalisms