CLEM Introduction

CLEM toolkit has been designed around the LE Synchronous language. It is a model-driven language to allow both efficiency and reusability of system design, and formal verification of system behavior. It relies on the synchronous hypothesis which assumes a discrete logic time scale, made of instants corresponding to reactions of the system. All the events concerned by a reaction are simultaneous: input events as well as the triggered output events. As a consequence, a reaction is instantaneous (we consider that a reaction takes no time, in compliance with synchronous language class), there are no concurrent partial reactions and so determinism can be ensured.

Although synchronous languages have begun to face the state explosion problem, there is still a need for further research on efficient and modular compilation of synchronous languages. Indeed, only few approaches consider a modular compilation because there is a deep dissension between causality and modularity . Causality means that for each event generated in a reaction, there is a causal chain of events leading to this generation. No causal loop may occur. Synchronous languages are well known to must check programs causality. Thus, rely on semantics to compile a language ensures a modular approach but requires to complete the compilation process with a global causality checking. The originality of our approach is the way we check causality from already checked sub programs and the modular approach we infer.

CLEM Modular Approach

The core of CLEM toolkit is the LE language and its modular compilation. The compiler relies on a constructive equational semantic which helps us to face the inherent causality cycle problem. Indeed, the constructive semantics is the application of constructive boolean logic theory to synchronous language semantics definition. A program is constructive}if and only if fact propagation is sufficient to establish the presence or absence of all signals.

An elegant means to define a constructive semantics for a language is to translate each program into a constructive equation system. Such a translation ensures that programs containing no cyclic instantaneous signal dependencies are translated into sorted equation systems. Equations propagate informations about signals status. The distinctive characteristic of our approach is that we don't consider boolean equation systems but &xi equation systems. &xi is a boolean algebra that provides us with a smarter information about signal status. Thus the information propagated by equations about signals status does not lead to determine signals as absent or present but also &perp (undefined) or T (error). As a consequence, this approach allows to not choose a static total order (that can lead to fake causality cycle) but to keep all eligible partial orders.