GAFFÉ , Daniel

Model verification, more commonly known as Model Checking, is a concept basedon an automatic formal verification approach of temporal properties on reactive systems.INRIA in collaboration with LEAT developed CLEM, a modeling and propertyverification tool, based on a state representation in finite automata generated automaticallyusing binary...

Dépôt conjoint entre l'UNS (Daniel Gaffé) et l'INRIA RocquencourtCertificat délivré par l'Agence pour la Protection des Programmes (AAP)Inter Deposit Digital Number IDDN.FR.001.170011.000.S.P.2014.000.1

From modeling to validation, the synchronous approch is well-suited to design reactive real-time computer-based systems. On the other hand, in the field of production system, the graphical and synchronous model GRAFCET is widely used. However, compared to GRAFCET, synchronous languages are endowed with a more formal semantics. In order to make...

In this report, we study different multi-valued algebras allowing to formally specify synchronous language semantics

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...

In this paper, we study the modular compilation of imperative synchronous programs. We rely on a formal framework well suited to perform compilation and formal validation of systems. In practice, we design and implement a special purpose language (LE) and its \execution equational semantics that allows the modular compilation of programs into...

International audience

The Automated Production Systems (APS) are composed of concurrent interacting entities. Then any model should exhibit parallel and sequential behaviours. The Grafcet is now well established in manufacturing to specify the awaited behaviour of the APS. Moreover, programmable components increase modularity and allow a higher integration rate of...

One of the biggest challenges in hardware and software design is to ensure that a system is error-free. Small errors in reactive embedded systems can have disastrous and costly consequences for a project. Preventing such errors by identifying the most probable cases of erratic system behavior is quite challenging. In this paper, we introduce an...

Synchronous languages rely 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...