Runtime Verification of Safety-Progress Properties (2009)
Falcone, Yliès, Fernandez, Jean-Claude, Mounier, Laurent
The underlying property, its definition and representation play a ma jor role when monitoring a system. Having a suitable and convenient framework to express properties is thus a concern for runtime...
Runtime Verification of Safety-Progress Properties (2009)
Falcone, Yliès, Fernandez, Jean-Claude, Mounier, Laurent
The underlying property, its definition and representation play a ma jor role when monitoring a system. Having a suitable and convenient framework to express properties is thus a concern for runtime...
J.L.: A test calculus framework applied to network security policies (2008)
Yliès Falcone, Jean-claude Fern, Laurent Mounier, Jean-luc Richier
Abstract. We propose a syntax-driven test generation technique to automaticaly derive abstract test cases from a set of requirements expressed in a linear temporal logic. Assuming that an elementary...
Ecole Normale, Supérieure Lyon, Laurent Mounier, Gil Utard, Adresses Électroniques, Laurent Mounier, ...
Unité de recherche associée au CNRS n°1398 Semantique axiomatique des langages a parallelisme de donnees � automatisation de la preuve de programmes
IF Validation Environment (2008)
Marius Bozga, Laurent Mounier, Iulian Ober
IF[5, 6, 10, 15] is an open validation platform for asynchronous timed systems such as telecommunication protocols or distributed applications developed at Verimag during the last 5 years. The...
IF: a validation environment for real-time UML and SDL models (2008)
Marius Bozga, Susanne Graf, Laurent Mounier, Iulian Ober
IF[5, 6, 8, 10, 14] is an open validation platform for asynchronous timed systems such as telecommunication protocols or distributed applications. The toolbox is built upon a specification language...
A Basu, Laurent Mounier, Marc Poulhiès, Jacques Pulou, Joseph Sifakis
networks, using the Behavior-Interaction-Priority
Synthesizing Enforcement Monitors wrt. the Safety-Progress Classification of Properties (2008)
Falcone, Yliès, Fernandez, Jean-Claude, Mounier, Laurent
Runtime enforcement is a powerful technique to ensure that a program will respect a given security policy. We extend previous works on this topic in several directions. Firstly, we propose a generic...
j-POST: a Java Toolchain for Property-Oriented Software Testing (2008)
Falcone, Yliès, Mounier, Laurent, Fernandez, Jean-Claude, Richier, Jean-Luc
j-POST is an integrated toolchain for property-oriented software testing. This toolchain includes a test designer, a test generator, and a test execution engine. The test generation is based on an...
Synthesizing Enforcement Monitors wrt. the Safety-Progress Classification of Properties (2008)
Falcone, Yliès, Fernandez, Jean-Claude, Mounier, Laurent
Runtime enforcement is a powerful technique to ensure that a program will respect a given security policy. We extend previous works on this topic in several directions. Firstly, we propose a generic...
j-POST: a Java Toolchain for Property-Oriented Software Testing (2008)
Falcone, Yliès, Mounier, Laurent, Fernandez, Jean-Claude, Richier, Jean-Luc
j-POST is an integrated toolchain for property-oriented software testing. This toolchain includes a test designer, a test generator, and a test execution engine. The test generation is based on an...
A Lotos Specification of a "Transit-Node" (2007)
This report describes the formal specification and verification of a "Transit-Node", an abstraction of a routing component of a communication network. First, an informal definition...
IF Validation Environment Tutorial (2007)
Marius Bozga, Susanne Graf, Laurent Mounier, Iulian Ober
IF[3, 7] is an open validation platform for asynchronous timed systems developed at Verimag during the last 5 years.
Marius Bozga, Jean-claude Fernandez, Lucian Ghirvu, Susanne Graf, Laurent Mounier, Joseph Sifakis
We present work of a project for the improvement of a specification/validation toolbox integrating a commercial toolset Objectgeode and different validation tools such as the verification tool cadp...
Marius Bozga, Jean-claude Fernandez, Lucian Ghirvu, Susanne Graf, Jean-pierre Krimm, Laurent Mounier
2
Marius Bozga, Susanne Graf, Laurent Mounier, Iulian Ober, Jean-luc Roux, Daniel Vincent
Abstract: In this paper we propose some extensions necessary to enable the specification and description language SDL to become an appropriate formalism for the design of real-time and embedded...
Marius Bozga, Jean-claude Fernandez, Lucian Ghirvu, Susanne Graf, Jean-pierre Krimm, Laurent Mounier
VERIMAG, Centre Equation, 2 avenue de Vignate, F-38610 Gi`eres 2 LSR/IMAG, BP 82, F-38402 Saint Martin d'H`eres Cedex
The ARESA Project: Facilitating Research, Development and Commercialization of WSNs (2007)
Dohler, Mischa, Barthel, Dominique, Maraninchi, Florence, Mounier, Laurent, Aubert, Stéphane, Dugas, Christophe, ...
Within academia, wireless sensor networks have witnessed a tremendous upsurge in the last decade, which is mainly attributed to their unprecedented operating conditions and hence unlimited research...
The ARESA Project: Facilitating Research, Development and Commercialization of WSNs (2007)
Dohler, Mischa, Barthel, Dominique, Maraninchi, Florence, Mounier, Laurent, Aubert, Stéphane, Dugas, Christophe, ...
Within academia, wireless sensor networks have witnessed a tremendous upsurge in the last decade, which is mainly attributed to their unprecedented operating conditions and hence unlimited research...
A Compositional Testing Framework Driven by Partial Specifications (2007)
Falcone, Yliès, Fernandez, Jean-Claude, Mounier, Laurent, Richier, Jean-Luc
We present a testing framework using a compositional approach to generate and execute test cases. Test cases are generated and combined with respect to a partial specification expressed as a set of...
A Compositional Testing Framework Driven by Partial Specifications (2007)
Falcone, Yliès, Fernandez, Jean-Claude, Mounier, Laurent, Richier, Jean-Luc
We present a testing framework using a compositional approach to generate and execute test cases. Test cases are generated and combined with respect to a partial specification expressed as a set of...
Avenue De Vignate, A Basu, Laurent Mounier, Marc Poulhiès, Pulou Joseph Sifakis, ...
Complex heterogeneous systems such as networked systems, composed of hardware and software, are validated by simulation of physical or virtual prototypes. The main obstacle for the application of...
A Test Calculus Framework Applied to Network Security Policies (2006)
Falcone, Yliès, Fernandez, Jean-Claude, Mounier, Laurent, Richier, Jean-Luc
We propose a syntax-driven test generation technique to automatically derive abstract test cases from a set of requirements expressed in a linear temporal logic. Assuming that an elementary test case...
A Test Calculus Framework Applied to Network Security Policies (2006)
Falcone, Yliès, Fernandez, Jean-Claude, Mounier, Laurent, Richier, Jean-Luc
We propose a syntax-driven test generation technique to automatically derive abstract test cases from a set of requirements expressed in a linear temporal logic. Assuming that an elementary test case...
Méthodes de vérification de spécifications comportementales : étude et mise en oeuvre (2004)
Nous rappelons tout d'abord le principe des procedures de decision classiques,qui reposent sur des algorithmes de raffinement de partitions. Cette approche necessite de construire au prealable les...
Change History Date Author Summary of changes (2004)
16/2/2004 Alan Hartman Approved after editorial changes from the internal reviewers 30/3/2004 Alan Hartman Revised according to the remarks from the external review panel
IF-2.0: A Validation Environment for Component-Based Real-Time Systems (2002)
Bozga, Marius, Graf, Susanne, Mounier, Laurent
This paper presents an overview on the IF toolset which is an environment for modelling and validation of heterogeneous real-time systems. The toolset is built upon a rich formalism, the IF notation,...
IF-2.0: A Validation Environment for Component-Based Real-Time Systems (2002)
Bozga, Marius, Graf, Susanne, Mounier, Laurent
This paper presents an overview on the IF toolset which is an environment for modelling and validation of heterogeneous real-time systems. The toolset is built upon a rich formalism, the IF notation,...
Using UML for automatic test generation (2002)
Ra Cavarra, Charles Crichton, Jim Davies, Alan Hartman, Laurent Mounier
Abstract. This paper presents an architecture for model-based verification and testing using a profile of the Unified Modeling Language (UML). Class, object, and state diagrams are used to define...
IF-2.0: A validation environment for component-based real-time systems (2002)
Marius Bozga, Susanne Graf, Laurent Mounier
It is widely recognised that the automated validation of complex systems can hardly be achieved without tool integration. The development of the IF-1.0 toolbox [3] was initiated several years ago, in...
Automated validation of distributed software using the IF environment (2001)
Marius Bozga, Susanne Graf, Laurent Mounier
This paper summarizes our experience with IF, an open validation environment for distributed software systems. Indeed, face to the increasing complexity of such systems, none of the existing tools...
Automated validation of distributed software using the IF environment (2001)
Bozga, Marius, Graf, Susanne, Mounier, Laurent
This paper summarizes our experience with IF, an open validation environment for distributed software systems. Indeed, face to the increasing complexity of such systems, none of the existing tools...
Automated validation of distributed software using the IF environment (2001)
Bozga, Marius, Graf, Susanne, Mounier, Laurent
This paper summarizes our experience with IF, an open validation environment for distributed software systems. Indeed, face to the increasing complexity of such systems, none of the existing tools...
Automated validation of distributed software using the IF environment (2001)
Bozga, Marius, Graf, Susanne, Mounier, Laurent
This paper summarizes our experience with IF, an open validation environment for distributed software systems. Indeed, face to the increasing complexity of such systems, none of the existing tools...
Model Checking Ariane-5 Flight Program (2001)
Bozga, Marius, Mounier, Laurent, Lesens, David
This paper reports a verification experiment carried out on a re-engineered description of a part of Ariane-5 Flight Program. This is the embedded software which solely controls the Ariane-5 launcher...
Timed Extensions for SDL (2001)
Bozga, Marius, Graf, Susanne, Mounier, Laurent, Ober, Iulian, Roux, Jean-Luc, Vincent, Daniel
In this paper we propose some extensions necessary to enable the specification and description language SDL to become an appropriate formalism for the design of real-time and embedded systems. The...
Automated validation of distributed software using the IF environment (2001)
Bozga, Marius, Graf, Susanne, Mounier, Laurent
This paper summarizes our experience with IF, an open validation environment for distributed software systems. Indeed, face to the increasing complexity of such systems, none of the existing tools...
Model Checking Ariane-5 Flight Program (2001)
Bozga, Marius, Mounier, Laurent, Lesens, David
This paper reports a verification experiment carried out on a re-engineered description of a part of Ariane-5 Flight Program. This is the embedded software which solely controls the Ariane-5 launcher...
Timed Extensions for SDL (2001)
Bozga, Marius, Graf, Susanne, Mounier, Laurent, Ober, Iulian, Roux, Jean-Luc, Vincent, Daniel
In this paper we propose some extensions necessary to enable the specification and description language SDL to become an appropriate formalism for the design of real-time and embedded systems. The...
SDL for Real-Time: What Is Missing? (2000)
Marius Bozga, Susanne Graf, Alain Kerbrat, Daniel Vincent, Laurent Mounier, Iulian Ober
. In this paper we give an overview on the main weaknesses of SDL for the development of real-time systems, both on the programming and on the specification side. In particular, the SDL semantics...
Jean-pierre Krimm, Laurent Mounier
. Compositional generation is an incremental technique for generating a reduced labelled transition system representing the behaviour of a set of communicating processes. In particular, since...
IF: A Validation Environment for Timed Asynchronous Systems (category B: tool presentation) (2000)
Marius Bozga, Jean-Claude Fernandez, Lucian Chirvu, Susanne Graf, Jean-Pierre Krimm, Laurent Mounier
Introduction Formal validation of distributed systems relies on several specification formalisms (such as the international standards lotos [16] or sdl [17]), and it requires different kinds of tools...
IF: A Validation Environment for Timed Asynchronous Systems (2000)
Bozga, Marius, Fernandez, Jean-Claude, Ghirvu, Constantin Lucian, Graf, Susanne, Jean Pierre, Krimm, Mounier, Laurent
Formal validation of distributed systems relies on several specification formalisms (such as the international standards LOTOS or SDL, and it requires different kinds of tools to cover the whole...
IF: A Validation Environment for Timed Asynchronous Systems (2000)
Bozga, Marius, Fernandez, Jean-Claude, Ghirvu, Constantin Lucian, Graf, Susanne, Jean Pierre, Krimm, Mounier, Laurent
Formal validation of distributed systems relies on several specification formalisms (such as the international standards LOTOS or SDL, and it requires different kinds of tools to cover the whole...
SDL for Real-Time: What Is Missing? (2000)
Bozga, Marius, Graf, Susanne, Mounier, Laurent, Kerbrat, Alain, Ober, Iulian, Vincent, Daniel
In this paper we review the needs of a real-time systems developer that are not covered, for various reasons, by SDL. The issues that we examine are heterogeneous, ranging from pure programming...
SDL for Real-Time: What Is Missing? (2000)
Bozga, Marius, Graf, Susanne, Mounier, Laurent, Kerbrat, Alain, Ober, Iulian, Vincent, Daniel
In this paper we review the needs of a real-time systems developer that are not covered, for various reasons, by SDL. The issues that we examine are heterogeneous, ranging from pure programming...
IF: An Intermediate Representation for SDL and its Applications (1999)
Marius Bozga, Jean-Claude Fernandez, Lucian Ghirvu, Susanne Graf, Jean-pierre Krimm, Laurent Mounier, ...
We present work of a project for the improvement of a specification/validation toolbox integrating a commercial toolset Objectgeode and different validation tools such as the verification tool cadp...
IF: An Intermediate Representation and Validation Environment for Timed Asynchronous Systems (1999)
Marius Bozga, Jean-Claude Fernandez, Lucian Ghirvu, Susanne Graf, Jean-pierre Krimm, Laurent Mounier
. Formal Description Techniques (fdt), such as lotos or sdl are at the base of a technology for the specification and the validation of telecommunication systems. Due to the availability of...
IF: An Intermediate Representation and Validation Environment for Timed Asynchronous Systems (1999)
Marius Bozga, Jean-Claude Fernandez, Lucian Ghirvu, Susanne Graf, Jean-pierre Krimm, Laurent Mounier
. Formal Description Techniques (fdt), such as lotos or sdl are at the base of a technology for the specification and the validation of telecommunication systems. Due to the availability of...
IF: An intermediate Representation and Validation Environment for Timed Asynchronous Systems (1999)
Bozga, Marius, Fernandez, Jean-Claude, Ghirvu, Constantin Lucian, Graf, Susanne, Krimm, Jean Pierre, Mounier, Laurent
Formal Description Techniques (FDT), such as LOTOS or SDL are at the base of a technology for the specification and the validation of telecommunication systems. Due to the availability of commercial...
IF: An intermediate Representation and Validation Environment for Timed Asynchronous Systems (1999)
Bozga, Marius, Fernandez, Jean-Claude, Ghirvu, Constantin Lucian, Graf, Susanne, Krimm, Jean Pierre, Mounier, Laurent
Formal Description Techniques (FDT), such as LOTOS or SDL are at the base of a technology for the specification and the validation of telecommunication systems. Due to the availability of commercial...
IF: An Intermediate Representation for SDL and its Applications (1999)
Bozga, Marius, Fernandez, Jean-Claude, Ghirvu, Constantin Lucian, Graf, Susanne, Jean Pierre, Krimm, Mounier, Laurent, ...
We present work of a project for the improvement of a specification/validation toolbox integrating a commercial toolset ObjectGeode and different validation tools such as the verification tool CADP...
IF: An Intermediate Representation for SDL and its Applications (1999)
Bozga, Marius, Fernandez, Jean-Claude, Ghirvu, Constantin Lucian, Graf, Susanne, Jean Pierre, Krimm, Mounier, Laurent, ...
We present work of a project for the improvement of a specification/validation toolbox integrating a commercial toolset ObjectGeode and different validation tools such as the verification tool CADP...
Compositional State Space Generation from Lotos Programs (1997)
Jean-pierre Krimm, Laurent Mounier
. This paper describes a compositional approach to generate the labeled transition system representing the behavior of a Lotos program by repeatedly alternating composition and reduction operations...
Garavel, Hubert, Mounier, Laurent
This report deals with the formal specification and verification of distributed leader election algorithms for a set of machines connected by a unidirectional ring network. Starting from an algorithm...
Chehaibar, Ghassan, Garavel, Hubert, Mounier, Laurent, Tawbi, Nadia, Zulian, Ferruccio
This paper presents the results of an industrial case-study concerning the use of formal methods for the validation of hardware design. The case-study focuses on PowerScale, a multiprocessor...
Garavel, Hubert, Mounier, Laurent
This report deals with the formal specification and verification of distributed leader election algorithms for a set of machines connected by a unidirectional ring network. Starting from an algorithm...
Chehaibar, Ghassan, Garavel, Hubert, Mounier, Laurent, Tawbi, Nadia, Zulian, Ferruccio
This paper presents the results of an industrial case-study concerning the use of formal methods for the validation of hardware design. The case-study focuses on PowerScale, a multiprocessor...
Garavel, Hubert, Mounier, Laurent
This report deals with the formal specification and verification of distributed leader election algorithms for a set of machines connected by a unidirectional ring network. Starting from an algorithm...
Chehaibar, Ghassan, Garavel, Hubert, Mounier, Laurent, Tawbi, Nadia, Zulian, Ferruccio
This paper presents the results of an industrial case-study concerning the use of formal methods for the validation of hardware design. The case-study focuses on PowerScale, a multiprocessor...
Ghassan Chehaibar, Ghassan Chehaibar, Hubert Garavel, Hubert Garavel, Laurent Mounier, Laurent Mounier, ...
: This paper presents the results of an industrial case-study concerning the use of formal methods for the validation of hardware design. The case-study focuses on PowerScale TM , a multiprocessor...
Hubert Garavel, Hubert Garavel, Laurent Mounier, Laurent Mounier, Projet Spectre
: This report deals with the formal specification and verification of distributed leader election algorithms for a set of machines connected by a unidirectional ring network. Starting from an...
CADP - A Protocol Validation and Verification Toolbox (1996)
Jean-Claude Fernandez, Hubert Garavel, Alain Kerbrat, Laurent Mounier, Radu Mateescu, Mihaela Sighireanu
Introduction Cadp (Caesar/Ald' ebaran Development Package) is a toolbox for protocol engineering. It offers a wide range of functionalities, ranging from interactive simulation to the most...
A local checking algorithm for Boolean Equation Systems (1995)
J.Cl. Fernandez, Laurent Mounier
Given a boolean equation system E and one of its bound variables X init , we propose a local algorithm for computing the solution ffi (X init ) of E . This algorithm relies on depth-first traversals...
On-the-fly verification of finite transition systems (1993)
Jard, Claude, Jéron, Thierry, Fernandez, Jean-Claude, Mounier, Laurent
Disponible dans les fichiers attachés à ce document
On-the-fly verification of finite transition systems (1993)
Jard, Claude, Jéron, Thierry, Fernandez, Jean-Claude, Mounier, Laurent
Disponible dans les fichiers attachés à ce document
On-The-Fly Verification Of Finite Transition Systems (1993)
Thierry J, Thierry Jéron, Jean-Claude Fernandez, Laurent Mounier, Claude Jard, Claude Jard
: The analysis of programs by the exhaustive inspection of reachable states in a finite state graph is a well-understood procedure It is actually implemented in several industrial tools but one of...
Méthodes de vérification de spécifications comportementales : étude et mise en oeuvre (1992)
Nous rappelons tout d'abord le principe des procedures de decision classiques,qui reposent sur des algorithmes de raffinement de partitions. Cette approche necessite de construire au prealable les...
Méthodes de vérification de spécifications comportementales : étude et mise en oeuvre (1992)
Nous rappelons tout d'abord le principe des procedures de decision classiques,qui reposent sur des algorithmes de raffinement de partitions. Cette approche necessite de construire au prealable les...
Méthodes de vérification de spécifications comportementales : étude et mise en oeuvre (1992)
Nous rappelons tout d'abord le principe des procedures de decision classiques,qui reposent sur des algorithmes de raffinement de partitions. Cette approche necessite de construire au prealable les...
Méthodes de vérification de spécifications comportementales : étude et mise en œuvre (1992)
Nous rappelons tout d'abord le principe des procedures de decision classiques,qui reposent sur des algorithmes de raffinement de partitions. Cette approche necessite de construire au prealable les...
Méthodes de vérification de spécifications comportementales : étude et mise en œuvre (1992)
Nous rappelons tout d'abord le principe des procedures de decision classiques,qui reposent sur des algorithmes de raffinement de partitions. Cette approche necessite de construire au prealable les...
Méthodes de vérification de spécifications comportementales : étude et mise en uvre (1992)
Nous rappelons tout d'abord le principe des procedures de decision classiques,qui reposent sur des algorithmes de raffinement de partitions. Cette approche necessite de construire au prealable les...
Méthodes de vérification de spécifications comportementales : étude et mise en oeuvre / (1992)
Résumé également en anglais.
A Toolbox for the Verification of LOTOS Programs (1992)
Jean-Claude Fernandez, Hubert Garavel, Laurent Mounier, Anne Rasse, Carlos Rodriguez, Joseph Sifakis
This paper presents the tools Ald' ebaran, Caesar, Caesar.adt and Cl' eop atre which constitute a toolbox for compiling and verifying Lotos programs. The principles of these tools are...
"On the Fly" Verification of Behavioural Equivalences and Preorders (1991)
Jean-Claude Fernandez, Laurent Mounier, Grenoble Cedex
This paper describes decision procedures for bisimulation and simulation relations between two transition systems. The algorithms proposed here do not need to previously construct them: the...
A Tool Set for deciding Behavioral Equivalences (1991)
Jean-Claude Fernandez, Laurent Mounier
This paper deals with verification methods based on equivalence relations between labeled transition systems. More precisely, we are concerned by two practical needs: how to efficiently minimize and...
Verifying Bisimulations "On the Fly" (1990)
Jean-Claude Fernandez, Laurent Mounier
This paper describes a decision procedure for bisimulation-based equivalence relations between labeled transition systems. The algorithm usually performed in order to verify bisimulation consists in...
Aldébaran: Users's manual (1990)
Jean-Claude Fernandez, Laurent Mounier
Introduction Ald'ebaran [2] is a system for verifying communicating systems, represented by transition systems whose arcs are labelled by action names. It allows the reduction and the comparison...
Validation of Asynchronous Circuit Specifications Using IF/CADP (1970)
Dominique Borrione, Menouer Boubekeur, Laurent Mounier, Marc Renaudin, Antoine Siriani
This work addresses the analysis and validation of modular CHP specifications for asynchronous circuits, using formalisms and tools coming from the field of distributed software. CHP specifications...