GAFFÉ , Daniel

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

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

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

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 defects 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. Indeed, tests performed in...

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

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

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

AUTSEG is an automatic test set generator for embedded reactive systems. It automatically generates exhaustive testsets and allows to check safety properties of the tested system. A first version of AUTSEG has been initially designed for programs dealing with Boolean inputs and outputs. We present in this paper an extension of this tool called...

In this paper, we present the synchronous approach as a new method for modeling neural architectures. The synchronous approach is initially used to design controllers for reactive real-time systems, and we explain how it fits well to our objective to design bio-inspired neuromorphic circuits for biohybrid experiments. We describe synchronous...

This article is threefold: (i) we define the first formal framework able to model dendritic integration within biological neurons, (ii) we show how we can turn continuous time into discrete time consistently and (iii) we show how a Lustre model checker can automatically perform proofs about neuron input/output behavioursowing to our...

We firstly define an improved version of the spiking neuron model with dendrites introduced in [8] and we focus here on the fundamental mathematical properties of the framework. Our main result is that, under few simplifications with respect to biology, dendrites can be simply abstracted by delays. Technically, we define a method allowing to...

In this paper we formalize Boolean Probabilistic Leaky Integrate and Fire Neural Networks as Discrete-Time Markov Chains using the language PRISM. In our models, the probability for neurons to emit spikes is driven by the difference between their membrane potential and their firing threshold. The potential value of each neuron is computed...

Activity Recognition aims at recognizing and understanding sequences of actions and movements of mobile objects (human beings, animals or artefacts), that follow the predefined model of an activity. We propose to describe activities as a series of actions, triggered and driven by environmental events. Due to the large range of application...

Activity recognition aims at recognizing and understanding the movements, actions, and objectives of mobile objects. These objects can be humans, animals, or simple artefacts. Many important and critical applications such as surveillance or health care require some form of (human) activity recognition. Existing languages can be used to describe...

Many important and critical applications such as surveillance or healthcare require some form of (human) activity recognition. Activities are usually represented by a series of actions driven and triggered by events. Recognition systems have to be real time, reactive, correct, complete, and dependable. These stringent requirements justify the...

This article presents the development of a new simulation framework for wireless sensor networks based on QEMU and SystemC that is capable of validating the binary code of wireless protocols, by validating and verifying protocol properties during simulation. We describe the development ofthe model of a node's hardware platform capable of...

This article presents a new simulation framework for wireless sensor networks based on QEMU and SystemC that aims at validating the binary code of wireless protocols by checking that the protocol's implementation complies with its property specifications during simulation. We describe the development of the model of a node's precise hardware...

There exists many ways to connect two, three or more neurons together to form different graphs. We call archetypes only the graphs whose properties can be associated with specific classes of biologically relevant structures and behaviors. These archetypes are supposed to be the basis of typical instances of neuronal information ...