Publications

Mes publications sont triées par revues internationales, conférences internationales avec comité de relecture, chapitres de livres, workshops, mémoires et autres publications. La liste des publications est également disponible sur DBLP.

Revues internationales

Statistical Model Checking with Change Detection.
Axel Legay, Louis-Marie Traonouez. Transactions on Foundations for Mastering Change I, volume 1, pages 157-179, 2016.
Résumé

Statistical Model Checking (SMC) is a powerful and widely used approach that consists in estimating the probability for a system to satisfy a temporal property. This is done by monitoring a finite number of executions of the system, and then extrapolating the result by using statistics. The answer is correct up to some confidence that can be parameterized by the user. It is known that SMC mitigates the state-space explosion problem and allows to approximate undecidable queries. The approach has been implemented in several toolsets such as Plasma Lab, and successfully applied in a wide range of diverse areas such as systems biology, robotic, or automotive. In this paper, we add two new modest contributions to the cathedral of results on SMC. The first contribution is an algorithm that can be used to monitor changes in the probability distribution to satisfy a bounded-time property at runtime. Concretely, the algorithm constantly monitors the execution of the deployed system, and raises a flag when it observes that the probability has changed significantly. This is done by extending the applicability of the CUSUM algorithm used in signal processing into the formal validation setting. Our second contribution is to show how the programming interface of Plasma Lab can be exploited in order to make SMC technology directly available in toolsets used by designers. This integration is done by exploiting simulation facilities of design tools. Our approach thus differs from the one adopted by other SMC/formal verification toolsets which assume the existence of formal semantics for the design language, as well as a compiling chain to the rather academic one used by validation tool. The concept results in the integration of Plasma Lab as a library of the Simulink toolset. The contributions are illustrated by using Plasma Lab to verify a Simulink case study modelling a pig shed temperature controller.

Optimizing the resource requirements of hierarchical scheduling systems.
Jin Hyun Kim, Axel Legay, Louis-Marie Traonouez, Abdeldjalil Boudjadar, Ulrik Nyman, Kim G. Larsen, Insup Lee, Jin-Young Choi. SIGBED Review, volume 13, issue 3, pages 41-48, 2016.
Résumé

Compositional reasoning on hierarchical scheduling systems is a well-founded formal method that can construct schedulable and optimal system configurations in a compositional way. However, a compositional framework formulates the resource requirement of a component, called an interface, by assuming that a resource is always supplied by the parent components in the most pessimistic way. For this reason, the component interface demands more resources than the amount of resources that are really sufficient to satisfy sub-components. We provide two new supply bound functions which provides tighter bounds on the resource requirements of individual components. The tighter bounds are calculated by using more information about the scheduling system. We evaluate our new tighter bounds by using a model-based schedulability framework for hierarchical scheduling systems realized as Uppaal models. The timed models are checked using model checking tools Uppaal and Uppaal SMC, and we compare our results with the state of the art tool CARTS.

Smart sampling for lightweight verification of Markov decision processes.
Pedro D'Argenio, Axel Legay, Sean Sedwards, Louis-Marie Traonouez. Software Tools for Technology Transfer, volume 17, issue 4, pages 469-484, 2015.
Résumé

Markov decision processes (MDP) are useful to model optimisation problems in concurrent systems. To verify MDPs with efficient Monte Carlo techniques requires that their nondeterminism be resolved by a scheduler. Recent work has introduced the elements of lightweight techniques to sample directly from scheduler space, but finding optimal schedulers by simple sampling may be inefficient. Here we describe 'smart' sampling algorithms that can make substantial improvements in performance.

Real-time specifications.
Alexandre David, Kim G. Larsen, Axel Legay, Ulrik Nyman, Louis-Marie Traonouez, Andrzej Wąsowski. Software Tools for Technology Transfer, volume 17, issue 1, pages 17-45, 2015.
Résumé

A specification theory combines notions of specifications and implementations with a satisfaction relation, a refinement relation, and a set of operators supporting stepwise design. We develop a specification framework for real-time systems using Timed I/O Automata as the specification formalism, with the semantics expressed in terms of Timed I/O Transition Systems. We provide constructs for refinement, consistency checking, logical and structural composition, and quotient of specifications—all indispensable ingredients of a compositional design methodology. The theory is implemented in the new tool Ecdar. We present symbolic versions of the algorithms used in Ecdar, and demonstrate the use of the tool using a small case study in compositional verification.

Robust synthesis for real-time systems.
Kim G. Larsen, Axel Legay, Louis-Marie Traonouez, Andrzej Wąsowski. Theoretical Computer Science, volume 515, pages 96-122, January 2014.
Résumé

Specification theories for real-time systems allow reasoning about interfaces and their implementation models, using a set of operators that includes satisfaction, refinement, logical and parallel composition. To make such theories applicable throughout the entire design process from an abstract specification to an implementation, we need to reason about the possibility to effectively implement the theoretical specifications on physical systems, despite their limited precision. In the literature, this implementation problem has been linked to the robustness problem that analyzes the consequences of introducing small perturbations into formal models. We address this problem of robust implementations in timed specification theories. We first consider a fixed perturbation and study the robustness of timed specifications with respect to the operators of the theory. To this end we synthesize robust strategies in timed games. Finally, we consider the parametric robustness problem and propose a counter-example refinement heuristic for computing safe perturbation values.

Symbolic unfolding of parametric stopwatch Petri nets.
Claude Jard, Didier Lime, Olivier (H.) Roux, Louis-Marie Traonouez. Formal Methods in System Design, volume 43, issue 3, pages 493-519, December 2013.
Résumé

We address the problem of unfolding safe parametric stopwatch time Petri nets (PSwPNs), i.e., safe time Petri nets (TPNs) possibly extended with time parameters and stopwatches. We extend the notion of branching process to account for the dates of the occurrences of events and thus define a symbolic unfolding for PSwPNs. In the case of TPNs we also propose a method based on our so-called time branching processes to compute a finite complete prefix of the symbolic unfolding. The originality of our work relies on a precise handling of direct conflicts between events, and the analysis of their effects on the constraints between the firing dates of those events.

Parametric Model-Checking of Stopwatch Petri Nets.
Louis-Marie Traonouez, Didier Lime, Olivier (H.) Roux. Journal of Universal Computer Science, 15(17):3273-3304, December 2009.
Résumé

At the border between control and verification, parametric verification can be used to synthesize constraints on the parameters to ensure that a system verifies given specifications. In this paper we propose a new framework for the parametric verification of time Petri nets with stopwatches. We first introduce a parametric extension of time Petri nets with inhibitor arcs (ITPNs) with temporal parameters and we define a symbolic representation of the parametric state-space based on the classical state-class graph method. Then, we propose semi-algorithms for the parametric model-checking of a subset of parametric TCTL formulae on ITPNs. These results have been implemented in the tool Romeo and we illustrate them in a case-study based on a scheduling problem.

.

Conférences internationales

Statistical Model Checking of Dynamic Software Architectures.
Everton Cavalcante, Jean Quilbeuf, Louis-Marie Traonouez, Flavio Oquendo, Thais Batista, Axel Legay. 10th European Conference on Software Architecture (ECSA) Copenhagen, Denmark, November 28 -December 2, 2016.
Résumé

The critical nature of many complex software-intensive systems calls for formal, rigorous architecture descriptions as means of supporting automated verification and enforcement of architectural properties and constraints. Model checking has been one of the most used techniques to automatically verify software architectures with respect to the satisfaction of architectural properties. However, such a technique leads to an exhaustive exploration of all possible states of the system, a problem that becomes more severe when verifying dynamic software systems due to their typical non-deterministic runtime behavior and unpredictable operation conditions. To tackle these issues, we propose using statistical model checking (SMC) to support the verification of dynamic software architectures while aiming at reducing computational resources and time required for this task. In this paper, we introduce a novel notation to formally express architectural properties as well as an SMC-based toolchain for verifying dynamic software architectures described in Pi-ADL, a formal architecture description language. We use a flood monitoring system to show how to express relevant properties to be verified. We also report the results of some computational experiments performed to assess the efficiency of our approach.

Plasma Lab: A Modular Statistical Model Checking Platform.
Axel Legay, Sean Sedwards, Louis-Marie Traonouez. Leveraging Applications of Formal Methods, Verification and Validation. Foundational Techniques. 7th International Symposium ISoLA, Corfu, Greece, October 10-14, 2016.
Résumé

We present an overview of Plasma Lab, a modular statistical model checking (SMC) platform that facilitates multiple SMC algorithms, multiple modelling and query languages and has multiple modes of use. Plasma Lab may be used as a stand-alone tool with a graphical development environment or invoked from the command line for high performance scripting applications. Plasma Lab is written in Java for maximum cross-platform compatibility, but it may interface with tools and libraries written in arbitrary programming languages. Plasma Lab’s API also allows it to be incorporated as a library within other tools. We first describe the motivation and architecture of Plasma Lab, then proceed to describe some of its important algorithms, including those for rare events and nondeterminism. We conclude with a number of industrially-relevant case studies and applications.

A Logic for the Statistical Model Checking of Dynamic Software Architectures.
Jean Quilbeuf, Everton Cavalcante, Louis-Marie Traonouez, Flavio Oquendo, Thais Batista, Axel Legay Leveraging Applications of Formal Methods, Verification and Validation. Foundational Techniques. 7th International Symposium ISoLA, Corfu, Greece, October 10-14, 2016.
Résumé

Dynamic software architectures emerge when addressing important features of contemporary systems, which often operate in dynamic environments subjected to change. Such systems are designed to be reconfigured over time while maintaining important properties, e.g., availability, correctness, etc. Verifying that reconfiguration operations make the system to meet the desired properties remains a major challenge. First, the verification process itself becomes often difficult when using exhaustive formal methods (such as model checking) due to the potentially infinite state space. Second, it is necessary to express the properties to be verified using some notation able to cope with the dynamic nature of these systems. Aiming at tackling these issues, we introduce DynBLTL, a new logic tailored to express both structural and behavioral properties in dynamic software architectures. Furthermore, we propose using statistical model checking (SMC) to support an efficient analysis of these properties by evaluating the probability of meeting them through a number of simulations. In this paper, we describe the main features of DynBLTL and how it was implemented as a plug-in for PLASMA, a statistical model checker.

A formal modeling and analysis framework for software product line of preemptive real-time systems.
Jin Hyun Kim, Axel Legay, Louis-Marie Traonouez, Mathieu Acher, Sungwon Kang. 31st Annual ACM Symposium on Applied Computing (SAC), Pisa, Italy, April 4-8, 2016.
Résumé

This paper presents a formal analysis framework to analyze a family of platform products w.r.t. real-time properties. First, we propose an extension of the widely-used feature model, called Property Feature Model (PFM), that distinguishes features and properties explicitly Second, we present formal behavioral models of components of a real-time scheduling unit such that all real-time scheduling units implied by a PFM are automatically composed to be analyzed against the properties given by the PFM. We apply our approach to the verification of the schedulability of a family of scheduling units using the symbolic and statistical model checkers of Uppaal.

Domain-Specific Code Generator Modeling: A Case Study for Multi-faceted Concurrent Systems.
Stefan Naujokat, Louis-Marie Traonouez, Malte Isberner, Bernhard Steffen, Axel Legay. Leveraging Applications of Formal Methods, Verification and Validation. Technologies for Mastering Change. 6th International Symposium ISoLA, Corfu, Greece, October 8-11, 2014.
Résumé

In this paper we discuss an elaborate case study utilizing the domain-specific development of code generators within the Cinco meta tooling suite. Cinco is a framework that allows for the automatic generation of a wide range of graphical modeling tools from an abstract high-level specification. The presented case study makes use of Cinco to rapidly construct custom graphical interfaces for multi-faceted, concurrent systems, comprising non-functional properties like time, probability, data, and costs. The point of this approach is to provide user communities and their favorite tools with graphical interfaces tailored to their specific needs. This will be illustrated by generating graphical interfaces for timed automata (TA), probabilistic timed automata (PTA), Markov decision processes (MDP) and simple labeled transition systems (LTS). The main contribution of the presented work, however, is the metamodel-based domain-specific construction of the corresponding code generators for the verification tools Uppaal, Spin, Plasma-lab, and Prism.

A Formalism for Stochastic Adaptive Systems.
Benoît Boyer, Axel Legay, Louis-Marie Traonouez. Leveraging Applications of Formal Methods, Verification and Validation. Specialized Techniques and Applications. 6th International Symposium ISoLA, Corfu, Greece, October 8-11, 2014.
Résumé

Complex systems such as systems of systems result from the combination of several components that are organized in a hierarchical manner. One of the main characteristics of those systems is their ability to adapt to new situations by modifying their architecture. Those systems have recently been the subject of a series of works in the software engineering community. Most of those works do not consider quantitative features. The objective of this paper is to propose a modeling language for adaptive systems whose behaviors depend on stochastic features. Our language relies on an extension of stochastic transition systems equipped with (1) an adaptive operator that allows to reason about the probability that a system has to adapt its architecture over time, and (2) dynamic interactions between processes. As a second contribution, we propose a contract-based extension of probabilistic linear temporal logic suited to reason about assumptions and guarantees of such systems. Our work has been implemented in the Plasma-Lab tool developed at Inria. This tool allows us to define stochastic adaptive systems with an extension of the Prism language, and properties with patterns. In addition, Plasma-Lab offers a simulation-based model checking procedure to reason about finite executions of the system. First experiments on a large case study coming from an industrial driven European project give encouraging results.

Structural Refinement for the Modal nu-Calculus.
Uli Fahrenberg, Axel Legay, Louis-Marie Traonouez. 11th International Colloquium on Theoretical Aspects of Computing (ICTAC), Bucharest, Romania, September 17-19, 2014.
Résumé

We introduce a new notion of structural refinement, a sound abstraction of logical implication, for the modal nu-calculus. Using new translations between the modal nu-calculus and disjunctive modal transition systems, we show that these two specification formalisms are structurally equivalent.

Using our translations, we also transfer the structural operations of composition and quotient from disjunctive modal transition systems to the modal nu-calculus. This shows that the modal nu-calculus supports composition and decomposition of specifications.

Compositionality for Quantitative Specifications.
Uli Fahrenberg, Jan Křetínský, Axel Legay, Louis-Marie Traonouez. 11th International Symposium on Formal Aspects of Component Software (FACS), Bertinoro, Italy, September 10-12, 2014.
Résumé

We provide a framework for compositional and iterative design and verification of systems with quantitative information, such as rewards, time or energy. It is based on disjunctive modal transition systems where we allow actions to bear various types of quantitative information. Throughout the design process the actions can be further refined and the information made more precise. We show how to compute the results of standard operations on the systems, including the quotient (residual), which has not been previously considered for quantitative non-deterministic systems. Our quantitative framework has close connections to the modal nu-calculus and is compositional with respect to general notions of distances between systems and the standard operations.

PyEcdar: Towards Open Source Implementation for Timed Systems.
Axel Legay, Louis-Marie Traonouez. 11th International Symposium on Automated Technology for Verification and Analysis (ATVA), Hanoi, Vietnam, October 15-18 2013.
Résumé

PyEcdar is an open source implementation for reasoning on timed systems. PyEcdar's main objective is not efficiency, but rather flexibility to test and implement new results on timed systems.

QUAIL: A Quantitative Security Analyzer for Imperative Code.
Fabrizio Biondi, Axel Legay, Louis-Marie Traonouez, Andrzej Wąsowski. 25th International Conference on Computer Aided Verification (CAV), Saint Petersburg, Russia, July 13-19, 2013.
Résumé

Quantitative security analysis evaluates and compares how effectively a system protects its secret data. We introduce QUAIL, the first tool able to perform an arbitrary-precision quantitative analysis of the security of a system depending on private information. QUAIL builds a Markov Chain model of the system's behavior as observed by an attacker, and computes the correlation between the system's observable output and the behavior depending on the private information, obtaining the expected amount of bits of the secret that the attacker will infer by observing the system. QUAIL is able to evaluate the safety of randomized protocols depending on secret data, allowing to verify a security protocol's effectiveness. We experiment with a few examples and show that QUAIL's security analysis is more accurate and revealing than results of other tools.

Robust Specification of Real Time Components.
Kim G. Larsen, Axel Legay, Louis-Marie Traonouez, Andrzej Wąsowski. 9th International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS), Aalborg, Denmark, September 2011.
Résumé

Specification theories for real-time systems allow to reason about interfaces and their implementation models, using a set of operators that includes satisfaction, refinement, logical and parallel composition. To make such theories applicable throughout the entire design process from an abstract specification to an implementation, we need to be able to reason about possibility to effectively implement the theoretical specifications on physical systems. In the literature, this implementation problem has already been linked to the robustness problem for Timed Automata, where small perturbations in the timings of the models are introduced. We address the problem of robust implementations in timed specification theories. Our contributions include the analysis of robust timed games and the study of robustness with respect to the operators of the theory.

Symbolic Unfolding of Parametric Stopwatch Petri Nets.
Louis-Marie Traonouez, Bartosz Grabiec, Claude Jard, Didier Lime, Olivier (H.) Roux. 8th International Symposium on Automated Technology for Verification and Analysis (ATVA), Singapore, September 2010.
Résumé

This paper proposes a new method to compute symbolic unfoldings for safe Stopwatch Petri Nets (SwPNs), extended with time parameters, that symbolically handle both the time and the parameters. We propose a concurrent semantics for (parametric) SwPNs in terms of timed processes à la Aura and Lilius. We then show how to compute a symbolic unfolding for such nets, as well as, for the subclass of safe time Petri nets, how to compute a finite complete prefix of this unfolding. Our contribution is threefold: unfolding in the presence of stopwatches or parameters has never been addressed before. Also in the case of time Petri nets, the proposed unfolding has no duplication of transitions and does not require read arcs and as such its computation is more local. Finally the unfolding method is implemented (for time Petri nets) in the tool Romeo.

Diagnosis using unfoldings of parametric time petri nets.
Bartosz Grabiec, Louis-Marie Traonouez, Claude Jard, Didier Lime, Olivier (H.) Roux. 8th International Conference on Formal Modelling and Analysis of Timed Systems (FORMATS), Vienna, Austria, September 2010.
Résumé

This paper considers the model of Time Petri Nets (TPNs) extended with time parameters and its use to perform on-line diagnosis of distributed systems. We propose to base the method on unfoldings. Given a partial observation, as a possibly structured set of actions, our method determines the causal relation between events in the model that explain the observation. It can also synthesize parametric constraints associated with these explanations. The method is implemented in the tool Romeo. We present its application to the diagnosis of the example of a cowshed with pigs.

Romeo: A Parametric Model-Checker for Petri Nets with Stopwatches.
Didier Lime, Olivier (H.) Roux, Charlotte Seidner, Louis-Marie Traonouez. 15th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), York, United Kingdom, March 2009.
Résumé

Last time we reported on Romeo, analyses with this tool were mostly based on translations to other tools. This new version provides an integrated TCTL model-checker and has gained in expressivity with the addition of parameters. Although there exists other tools to compute the state-space of stopwatch models, Romeo is the first one that performs TCTL model-checking on stopwatch models. Moreover, it is the first tool that performs TCTL model-checking on timed parametric models. Indeed, Romeo now features an efficient model-checking of time Petri nets using the Uppaal DBM Library, the model-checking of stopwatch Petri nets and parametric stopwatch Petri nets using the Parma Polyhedra Library and a graphical editor and simulator of these models. Furthermore, its audience has increased leading to several industrial contracts. This paper reports on these recent developments of Romeo.

Parametric Model-Checking of Time Petri Nets with Stopwatches Using the State-Class Graph.
Louis-Marie Traonouez, Didier Lime, Olivier (H.) Roux. 6th International Conference on Formal Modelling and Analysis of Timed Systems (FORMATS), Saint-Malo, France, September 2008.

Papiers invités

Rare Events for Statistical Model Checking an Overview
Axel Legay, Sean Sedwards, Louis-Marie Traonouez. Reachability Problems - 10th International Workshop, Aalborg, Denmark, September 2016. Résumé

This invited paper surveys several simulation-based approaches to compute the probability of rare bugs in complex systems. The paper also describes how those techniques can be implemented in the professional toolset Plasma.

A Parametric Counterexample Refinement Approach for Robust Timed Specifications .
Louis-Marie Traonouez. Invited paper at the fourth International Workshop on Foundations of Interface Technologies (FIT), in conjunction with the ETAPS conference, Tallinn, Estonia, 25th of March 2012.
Résumé

Robustness analyzes the impact of small perturbations in the semantics of a model. This allows to model hardware imprecision and therefore it has been applied to determine implementability of timed automata. In a recent paper, we extend this problem to a specification theory for real-timed systems based on timed input/output automata, that are interpreted as two-player games. We propose a construction that allows to synthesize an implementation of a specification that is robust under a given timed perturbation, and we study the impact of these perturbations when composing different specifications.
To complete this work we present a technique that evaluates the greatest admissible perturbation. It consists in an iterative process that extracts a spoiling strategy when a game is lost, and through a parametric analysis refines the admissible values for the perturbation. We demonstrate this approach with a prototype implementation.

Chapitres de livre

Specification Theories for Probabilistic and Real-Time Systems.
Uli Fahrenberg, Axel Legay and Louis-Marie Traonouez. In From Programs to Systems -- The Systems Perspective in Computing, ETAPS Workshop in Honor of Joseph Sifakis, Grenoble, France, April 6, 2014.
Parametric and Quantitative Extensions of Modal Transition Systems.
Uli Fahrenberg, Kim G. Larsen, Axel Legay and Louis-Marie Traonouez. In From Programs to Systems -- The Systems Perspective in Computing, ETAPS Workshop in Honor of Joseph Sifakis, Grenoble, France, April 6, 2014.
Tools for Model-Checking Timed Systems.
A. David, G. Behrmann, P. Bulychev, T. Chatain, K.G. Larsen, P. Pettersson, J. Rasmussen, J. Srba, W. Yi, K.Y. Joergensen, D. Lime, M. Magnin, O.H. Roux and L.M. Traonouez. In Communicating Embedded Systems -- Software and Design, pages 165-225. ISTE Publishing / John Wiley, 2009.

Workshops

A Model-Based Framework for the Specification and Analysis of Hierarchical Scheduling Systems.
Mounir Chadli, Jin Hyun Kim, Axel Legay, Louis-Marie Traonouez, Stefan Naujokat, Bernhard Steffen, Kim Guldstrand Larsen. 21st International Workshop on Formal Methods for Industrial Critical Systems and 16th International Workshop on Automated Verification of Critical Systems (FMICS-AVoCS), Pisa, Italy, September 26-28, 2016.
Résumé

Over the years, schedulability of Cyber-Physical Systems (CPS) has mainly been performed by analytical methods. Those techniques are known to be effective but limited to a few classes of scheduling policies. In a series of recent work, we have shown that schedulability analysis of CPS could be performed with a model-based approach and extensions of verification tools such as UPPAAL. One of our main contribution has been to show that such models are flexible enough to embed various types of scheduling policies that go beyond those in the scope of analytical tools. In this paper, we go one step further and show how our formalism can be extended to account for stochastic information, such as sporadic tasks whose attributes depend on the hardware domain.

Distributed Verification of Rare Properties using Importance Splitting Observers.
Cyrille Jégourel, Axel Legay, Sean Sedwards, Louis-Marie Traonouez. 15th International Workshop on Automated Verification of Critical Systems (AVoCS), Edinburgh, United Kingdom, September 1-4, 2015.
Résumé

Rare properties remain a challenge for statistical model checking (SMC) due to the quadratic scaling of variance with rarity. We address this with a variance reduction framework based on lightweight importance splitting observers. These expose the model-property automaton to allow the construction of score functions for high performance algorithms. The confidence intervals defined for importance splitting make it appealing for SMC, but optimising its performance in the standard way makes distribution inefficient. We show how it is possible to achieve equivalently good results in less time by distributing simpler algorithms. We first explore the challenges posed by importance splitting and present an algorithm optimised for distribution. We then define a specific bounded time logic that is compiled into memory-efficient observers to monitor executions. Finally, we demonstrate our framework on a number of challenging case studies.

Estimating Rewards & Rare Events in Nondeterministic Systems.
Axel Legay, Sean Sedwards, Louis-Marie Traonouez. 15th International Workshop on Automated Verification of Critical Systems (AVoCS), Edinburgh, United Kingdom, September 1-4, 2015.
Résumé

Exhaustive verification can quantify critical behaviour arising from concurrency in nondeterministic models. Rare events typically entail no additional challenge, but complex systems are generally intractable. Recent work on Markov decision processes allows the extremal probabilities of a property to be estimated using Monte Carlo techniques, offering the potential to handle much larger models. Here we present algorithms to estimate extremal rewards and consider the challenges posed by rarity. We find that rewards require a different interpretation of confidence and that reachability rewards require the introduction of an auxiliary hypothesis test. We show how importance sampling can significantly improve estimation when probabilities are low, but find it is not a panacea for rare schedulers.

Statistical Model Checking of Simulink Models with Plasma Lab.
Axel Legay, Louis-Marie Traonouez. Fourth International Workshop on Formal Techniques for Safety-Critical Systems (FTSCS), Paris, France, November 6-7, 2015.
Résumé

We present an extension of the statistical model-checker Plasma Lab capable of analyzing Simulink models.

Scalable Verification of Markov Decision Processes.
Axel Legay, Sean Sedwards, Louis-Marie Traonouez. 4th Workshop on Formal Methods in the Development of Software (FMDS), in conjunction with the SEFM conference, Grenoble, France, September 2, 2014.
Résumé

Markov decision processes (MDP) are useful to model concurrent process optimisation problems, but verifying them with numerical methods is often intractable. Existing approximative approaches do not scale well and are limited to memoryless schedulers. Here we present the basis of scalable verification for MDPSs, using an O(1) memory representation of history-dependent schedulers. We thus facilitate scalable learning techniques and the use of massively parallel verification.

A Framework for the Rigorous Design of Highly Adaptive Timed Systems.
Maxime Cordy, Axel Legay, Pierre-Yves Schobbens, Louis-Marie Traonouez. First International Workshop on Formal Methods in Software Engineering (FormaliSE), in conjunction with the ICSE conference, San Francisco, USA, 25th of May 2013.
Résumé

Adaptive systems can be regarded as a set of static programs and transitions between these programs. These transitions allow the system to adapt its behaviour in responseto unexpected changes in its environment. Modelling highly dynamic systems is cumbersome, as these may go through a large number of adaptations. Moreover, often they must also satisfy real-time requirements whereas adaptations may not complete instantaneously. In this paper, we propose to model highly adaptive systems as dynamic real-time software product lines, where software products are able to change their features at runtime. Adaptive features allow one to design systems equipped with runtime reconfiguration capabilities and to model changes in their environment, such has failure modes. We define Featured Timed Game Automata, a formalism that combines adaptive features with discrete and real-time behaviour. We also propose a novel logic to express real-time requirements on adaptive systems, as well as algorithms to check a system against them. We implemented our method as part of PyECDAR, a model checker for timed systems.

Mémoires

Vérification et dépliages de réseaux de Petri temporels paramétrés.
Louis-Marie Traonouez. Ph.D thesis, University of Nantes, November 2009.
Stratégies d'analyse d'une fraction d'un réseau de Petri T-temporel
Louis-Marie Traonouez. Master's thesis, École Centrale de Nantes, September 2006.
Raisonnement temporel en sémantique forte à partir de Louis-Marie Traonouez. réseaux de Petri temporels exprimés en Logique Linéaire.
Master's bibliography report. École Centrale de Nantes, May 2006.

Divers

Synthèse de contraintes de conception à partir de réseaux de Petri temporels paramétrés.
Louis-Marie Traonouez, David Delfieu and Olivier (H.) Roux. 6ème Colloque Francophone sur la Modélisation des Systèmes Réactifs (MSR), Lyon, France, October 2007.
Parametrized Study of a Time Petri Net.
David Delfieu, Médésu Sogbohossou, Louis-Marie Traonouez and Sébastien Revol 4th International Conference on Cybernetics and Information Technologies, Systems and Applications (CITSA), Orlando, Florida, USA, July 2008.