RESSOUCHE , Annie

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

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

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

BLOCKS is an answer to the software engineering needs of the design of knowledge-based system engines. It is a framework composed of reusable and adaptable software components. However , its safe and correct use is complex and we supply formal models and associated tools to assist using it. These models and tools are based on behavioral...

Nowadays, adaptive middleware plays an important role in the design of applications in ubiquitous and ambient computing. Currently most of these systems manage the adaptation at the middleware intermediary layer. Dynamic adaptive middleware are then decomposed into two levels : a first one to simplify the development of distributed systems...

Nowadays, adaptive middleware plays an important role in the design of applications in ubiquitous and ambient computing. In this paper we consider component-based middleware and a corresponding compositional adaptation. Indeed, the composition often involves conflicts between concurrent adaptations. Thus we study how to maintain consistency of...

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

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

The Internet of Things (IoT) connects sensors, actuators and autonomous objects interacting with each other. These devices are represented by web services. Web services composition often involves conflicts between systems having access to shared devices. In our component-based middleware, our solution allows managing access to shared devices,...

Activity recognition is important for security and safety in many domains, such as surveillanceand health care. We propose to describe activities as a series of actions, triggered and driven by environmental events. We rely on synchronous automata to describe such activities. We chose the synchronousparadigm because it has a well-founded...

There exists many ways to connect two, three or more neu-rons 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 processing. To...

In the literature, neuronal networks are often represented as graphs where each node symbolizes a neuron and each arc stands for a synaptic connection. Some specific neuronal graphs have biologically relevant structures and behaviors and we call them archetypes. Six of them have already been characterized and validated using formal methods. In...

Having a formal model of neural networks can greatly help in understanding and verifying their properties, behavior, and response to external factors such as disease and medicine. In this paper, we adopt a formal model to represent neurons, some neuronal graphs, and their composition. Some specific neuronal graphs are known for having...