In this article, we study several relevant algebraic frameworks to define synchronous language semantics. Synchronous languages are quite dedicated to design critical embedded applications. Thus, verification and compilation is challenging and should rely on mathematical semantics. We study multi-valued algebras as foundation for semantics definition and we show that a 4-valued algebra with a bilattice structure is well suited to our concern. With this approach we can define semantics offering both the generation of models where verification techniques apply, and separated compilation means.

In this demonstration session, we present a toolkit we have designed around a model-driven language fLEJ. This relies on formal methods to ease the development of applications in an efficient and reusable way. Formal methods have been advocated as a means of increasing the reliability of systems, especially those which are safety or business critical. It is still difficult to develop automatic specification and verification tools due to limitations like state explosion, undecidability, etc. To face these problems, we provide LE with a constructive semantic that allows the modular compilation of programs into software and hardware targets (C code, VHDL code, FPGA synthesis, Verification tools). Moreover, we also provide software to design, compile and verify LE programs. Our approach is pertinent according to the two main requirements of critical realistic applications: the modular compilation allows us to deal with large systems, the model-driven approach provides us with formal validation.

Concrete critical systems validation is a major challenge in any development process. Model checking verification offers exhaustive and automated validation. To apply this methodology, the specification of critical systems must be supported by a formal mathematical well-sounded model. To this end, we rely on synchronous language to model such systems and to ensure model existence we consider systems falling into a particular SAS architecture. SAS systems are composed by a synchronous main controller that manages autonomic asynchronous tasks. Abstraction methods provide us with the required synchronous model. We show how our approach suits wearable computer applications designing and how the modeling we propose meets the requirements of wearable computer validation.