Author

Alexandre David

64 papers · 1998–2026

1998peak 7 in 20122026

Frequent co-authors

Papers

showing 1–25 of 64 RSS

Timed I/O automata

Alexandre David, Kim G. Larsen, Axel Legay +2 more

Computational Theory and Mathematics · IT University Of Copenhagen (IT University of Copenhagen) · 12 Apr 2010 · cited 173× · DOI ↗ · more like this ·

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 complete 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 on top of an engine for timed games, Uppaal-tiga, and illustrated with a small case study.

UPPAAL-SMC: Statistical Model Checking for Priced Timed Automata

Peter Bulychev, Alexandre David, Kim Gulstrand Larsen +4 more

cs.LO · 4 Jul 2012 · cited 162× · arXiv ↗ · more like this ·

This paper offers a survey of uppaalsmc, a major extension of the real-time verification tool uppaal. uppaalsmc allows for the efficient analysis of performance properties of networks of priced timed automata under a natural stochastic semantics. In particular, uppaalsmc relies on a series of extensions of the statistical model checking approach generalized to handle real-time systems and estimate undecidable problems. uppaalsmc comes together with a friendly user interface that allows a user to specify complex problems in an efficient manner as well as to get feedback in the form of probability distributions and compare probabilities to analyze performance aspects of systems. The focus of the survey is on the evolution of the tool - including modeling and specification formalisms as well as techniques applied - together with applications of the tool to case studies.

Developing U<scp>PPAAL</scp> over 15 years

Gerd Behrmann, Alexandre David, Kim G. Larsen +2 more

Computational Theory and Mathematics · Software Practice and Experience · 23 Jan 2011 · cited 95× · DOI ↗ · more like this ·

Abstract U PPAAL is a tool suitable for model checking real‐time systems described as networks of timed automata communicating by channel synchronizations and extended with integer variables. Its first version was released in 1995 and its development is still very active. It now features an advanced modeling language, a user‐friendly graphical interface, and a performant model checker engine. In addition, several flavors of the tool have matured in recent years. In this paper, we present how we managed to maintain the tool during 15 years, its current architecture with its challenges, and we give the future directions of the tool. Copyright © 2011 John Wiley & Sons, Ltd.

Statistical Model Checking for Stochastic Hybrid Systems

Alexandre David, Dehui Du, Kim G. Larsen +4 more

cs.CE · 19 Aug 2012 · cited 92× · arXiv ↗ · more like this ·

This paper presents novel extensions and applications of the UPPAAL-SMC model checker. The extensions allow for statistical model checking of stochastic hybrid systems. We show how our race-based stochastic semantics extends to networks of hybrid systems, and indicate the integration technique applied for implementing this semantics in the UPPAAL-SMC simulation engine. We report on two applications of the resulting tool-set coming from systems biology and energy aware buildings.

Model-Based Framework for Schedulability Analysis Using Uppaal 4.1

Alexandre David, Jacob Illum, Kim G. Larsen +1 more

Hardware and Architecture · VBN Forskningsportal (Aalborg Universitet) · 3 Sep 2018 · cited 70× · DOI ↗ · more like this ·

Embedded systems involve the monitoring and control of complex physical processes using applications running on dedicated execution platforms in aresource-constrained manner in terms of, for example, memory, processing power, bandwidth, energy consumption, and timing behavior.

From HUPPAAL to UPPAAL - A Translation from Hierarchical Timed Automata to Flat Timed Automata

Alexandre David, Marianne Møller

Computational Theory and Mathematics · BRICS Report Series · 11 Mar 2001 · cited 46× · DOI ↗ · more like this ·

We present a hierarchical version of timed automata, equipped with data types, hand-shake synchronization, and local variables. We describe the formal semantics of this hierarchical timed automata (HTA) formalism in terms of a transition system. We report on the implementation of a flattening algorithm, that translates our formalism to a network of Uppaal timed automata. We establish a correspondence between symbolic states of an HTA and its translations, and thus are able to make use of Uppaal’s simulator and model checking engine. This technique is exemplified with a cardiac pacemaker model. Here, the overhead introduced by the translation is tolerable. We give run-time data for deadlock checking, timed reachability, and timed response analysis.

Timed Testing under Partial Observability

Alexandre David, Kim G. Larsen, Shuhao Li +1 more

Computational Theory and Mathematics · VBN Forskningsportal (Aalborg Universitet) · April 2009 · cited 22× · DOI ↗ · more like this ·

This paper studies the problem of model-based testing of real-time systems that are only partially observable. We model the system under test (SUT) using timed game automata (TGA) which has internal actions, uncontrollable outputs and timing uncertainty of outputs. We define the partial observability of SUT using a set of predicates over the TGA state space, and specify the test purposes in computation tree logic (CTL) formulas. A developed partially observable timed game solver is used to generate winning strategies, which are used as test cases. We propose a conformance testing framework, define a partial observation-based conformance relation, present the test execution algorithms, and prove the soundness and completeness of this test method (i.e., a detected error really violates the conformance relation; and if the SUT violates the test purpose, then a test case can be generated to…

Modelling Social-Technical Attacks with Timed Automata

Nicolas David, Alexandre David, René Rydhof Hansen +4 more

Information Systems · VBN Forskningsportal (Aalborg Universitet) · 6 Oct 2015 · cited 21× · DOI ↗ · more like this ·

Attacks on a system often exploit vulnerabilities that arise from human behaviour or other human activity. Attacks of this type, so-called socio-technical attacks, cover everything from social engineering to insider attacks, and they can have a devastating impact on an unprepared organisation. In this paper we develop an approach towards modelling socio-technical systems in general and socio-technical attacks in particular, using timed automata and illustrate its application by a complex case study. Thanks to automated model checking and automata theory, we can automatically generate possible attacks in our model and perform analysis and simulation of both model and attack, revealing details about the specific interaction between attacker and victim. Using timed automata also allows for intuitive modelling of systems, in which quantities like time and cost can be easily added and…

Statistical Model Checking of Dynamic Networks of Stochastic Hybrid Automata

Alexandre David, Kim G. Larsen, Axel Legay +1 more

Computational Theory and Mathematics · VBN Forskningsportal (Aalborg Universitet) · 25 Mar 2024 · cited 20× · DOI ↗ · more like this ·

In this paper we present a modelling formalism for dynamic networks of stochastic hybrid automata. In particular, our formalism is based on primitives for the dynamic creation and termination of hybrid automata components during the execution of a system. In this way we allow for natural modelling of concepts such as multiple threads found in various programming paradigms, as well as the dynamic evolution of biological systems. We provide a natural stochastic semantics of the modelling formalism based on re- peated output races between the dynamic evolving components of a system. As specification language we present a quantified extension of the logic Metric Tempo- ral Logic (MTL). As a main contribution of this paper, the statistical model checking engine of U PPAAL has been extended to the setting of dynamic networks of hybrid systems and quantified MTL. We demonstrate the usefulness…

Verification of UML Statecharts with Real-Time Extensions

Alexandre David, Marianne Møller, Yi Wang

Computational Theory and Mathematics · KTH Publication Database DiVA (KTH Royal Institute of Technology) · 2003 · cited 20× · OpenAlex ↗ · more like this ·

Mobile work situations within home care of the elderly require immediate and ubiquitous access to patient-oriented data. We intend to develop a mobile information system that provides correct information in a proper way to the right person in the appropriate occasion of care. This requires a thorough user needs analysis that so far often has been neglected during systems development in health care. We conducted the user needs analysis in interdisciplinary working groups in order to achieve a holistic view of the entire work process. This allows for the development of not only patient-oriented but care process oriented systems. In this paper, we describe how the user needs analysis was conducted, the impact of this work on the user group and some of the requirements found to be specific for mobile IT-support for home care of the elderly.

A game-theoretic approach to real-time system testing

Alexandre David, Kim G. Larsen, Shuhao Li +1 more

Computational Theory and Mathematics · VBN Forskningsportal (Aalborg Universitet) · 10 Mar 2008 · cited 16× · DOI ↗ · more like this ·

This paper presents a game-theoretic approach to the testing of uncontrollable real-time systems. By modelling the systems with Timed I/O Game Automata and specifying the test purposes as Timed CTL formulas, we employ a recently developed timed game solver UPPAAL-TIGA to synthesize winning strategies, and then use these strategies to conduct black-box conformance testing of the systems. The testing process is proved to be sound and complete with respect to the given test purposes. Case study and preliminary experimental results indicate that this is a viable approach to uncontrollable timed system testing.

Degree of Schedulability of Mixed-Criticality Real-Time Systems with Probabilistic Sporadic Tasks

Abdeldjalil Boudjadar, Alexandre David, Jin Hyun Kim +4 more

Hardware and Architecture · VBN Forskningsportal (Aalborg Universitet) · September 2014 · cited 13× · DOI ↗ · more like this ·

We present the concept of degree of schedulability for mixed-criticality scheduling systems. This concept is given in terms of the two factors 1) Percentage of Missed Deadlines (PoMD), and 2) Degradation of the Quality of Service (DoQoS). The novel aspect is that we consider task arrival patterns that follow user-defined continuous probability distributions. We determine the degree of schedulability of a single scheduling component which can contain both periodic and sporadic tasks using statistical model checking in the form of UPPAAL SMC. We support uniform, exponential, Gaussian and any user-defined probability distribution.

W2574579385

Jalil Boudjadar, Alexandre David, Jin Hyun Kim +3 more

Hardware and Architecture · VBN Forskningsportal (Aalborg Universitet) · 2014 · cited 13× · OpenAlex ↗ · more like this ·

We propose a framework for modeling and analyzing the schedulability and energy efficiency of embedded hierarchical scheduling systems running on a multi-core platform.The framework is realized using Hybrid Timed Automata describing the concrete task behavior.The schedulability can be verified in a compositional way using UPPAAL, and the energy profile can be generated using the statistical model checking algorithms of UPPAAL SMC.To our knowledge, our paper is the first one considering hierarchical scheduling, multi-core platforms and energy consumption simultaneously.The framework is being applied to a case-study from the CRAFTERS project.

Computing Nash Equilibrium in Wireless Ad Hoc Networks: A Simulation-Based Approach

Peter Bulychev, Alexandre David, Kim G. Larsen +2 more

cs.GT · 21 Feb 2012 · cited 13× · arXiv ↗ · more like this ·

This paper studies the problem of computing Nash equilibrium in wireless networks modeled by Weighted Timed Automata. Such formalism comes together with a logic that can be used to describe complex features such as timed energy constraints. Our contribution is a method for solving this problem using Statistical Model Checking. The method has been implemented in UPPAAL model checker and has been applied to the analysis of Aloha CSMA/CD and IEEE 802.15.4 CSMA/CA protocols.

Cooperative Testing of Timed Systems

Alexandre David, Kim G. Larsen, Shuhao Li +1 more

Computational Theory and Mathematics · Electronic Notes in Theoretical Computer Science · December 2008 · cited 12× · DOI ↗ · more like this ·

This paper deals with targeted testing of timed systems whose models may have uncontrollable behavior. The testing activity is viewed as a game between the tester and the system under test (SUT) towards a given test purpose. The SUT is modeled as Timed Game Automaton and the test purpose is specified in Timed CTL formula. We employ a timed game solver UPPAAL-TIGA to check if the test purpose is ture w.r.t. the model, and if yes, to generate a winning strategy and use it for black-box conformance testing of the SUT implementation. Specifically, we show that in case the checking yields a negative result, we can still test the SUT implementation against the test purpose as long as the SUT implementation reacts to our moves in a cooperative style. We present an operational framework of cooperative winning strategy generation, test case derivation and execution. The test method is proved to…

Tools for Real-Time UML: Formal Verification and Code Synthesis

Tobias Amnell, Alexandre David, Elena Fersman +3 more

Computational Theory and Mathematics · 2001 · cited 12× · OpenAlex ↗ · more like this ·

We present a real-time extension of UML statecharts to enable modelling and verification of real-timed constraints. For clarity, we shall consider a reasonable subset of the rich UML statechart model and extend it with real-time constructs (clocks, timed guards, invariants and real-time tasks). We have developed a a rule-based formal semantics for the obtained formalism, called hierarchical timed automata (HTA). To use the existing tool UPPAAL for formal verification, HTA are translated to enriched timed automata model. We report on an XML based implementation of the translation from HTA to a network of timed automata and present an example to illustrate our technique and report run-time data for the formal verification part. We also report on a prototype implementation of the code synthesis for the legOS platform. 1

Hierarchical Modeling and Analysis of Timed Systems

Alexandre David

Computational Theory and Mathematics · KTH Publication Database DiVA (KTH Royal Institute of Technology) · 2003 · cited 11× · OpenAlex ↗ · more like this ·

Uppaal is a tool for model-checking real-time systems developed jointly by Uppsala University and Aalborg University. It has been applied successfully in case studies ranging from communication protocols to multimedia applications. The tool is designed to verify systems that can be modeled as networks of timed automata. But it lacks support for systems with hierarchical structures, which makes the construction of large models difficult. In this thesis we improve the efficiency of Uppaal with new data structures and extend its modeling language and its engine to support hierarchical constructs. To investigate the limits of Uppaal, we model and analyze an industrial fieldbus communication protocol. To our knowledge, this case study is the largest application…

State-of-the-art tools and techniques for quantitative modeling and analysis of embedded systems

Marius Bozga, Alexandre David, Arnd Hartmanns +4 more

Hardware and Architecture · VBN Forskningsportal (Aalborg Universitet) · 12 Mar 2012 · cited 10× · DOI ↗ · more like this ·

This paper surveys well-established/recent tools and techniques developed for the design of rigorous embedded systems. We will first survey Uppaal and Modest, two tools capable of dealing with both timed and stochastic aspects. Then, we will overview the BIP framework for modular design and code generation. Finally, model-based testing will be discussed.

Distributed Parametric and Statistical Model Checking

Peter Bulychev, Alexandre David, Kim Guldstrand Larsen +2 more

cs.SE · 2 Nov 2011 · cited 9× · arXiv ↗ · more like this ·

Statistical Model Checking (SMC) is a trade-off between testing and formal verification. The core idea of the approach is to conduct some simulations of the system and verify if they satisfy some given property. In this paper we show that SMC is easily parallelizable on a master/slaves architecture by introducing a series of algorithms that scale almost linearly with respect to the number of slave computers. Our approach has been implemented in the UPPAAL SMC toolset and applied on non-trivial case studies.

Stochastic Semantics and Statistical Model Checking for Networks of Priced Timed Automata

Alexandre David, Kim G. Larsen, Axel Legay +4 more

cs.SE · June 2011 · cited 9× · arXiv ↗ · more like this ·

This paper offers a natural stochastic semantics of Networks of Priced Timed Automata (NPTA) based on races between components. The semantics provides the basis for satisfaction of probabilistic Weighted CTL properties (PWCTL), conservatively extending the classical satisfaction of timed automata with respect to TCTL. In particular the extension allows for hard real-time properties of timed automata expressible in TCTL to be refined by performance properties, e.g. in terms of probabilistic guarantees of time- and cost-bounded properties. A second contribution of the paper is the application of Statistical Model Checking (SMC) to efficiently estimate the correctness of non-nested PWCTL model checking problems with a desired level of confidence, based on a number of independent runs of the NPTA. In addition to applying classical SMC algorithms, we also offer an extension that allows to…

Uppaal-Tiga: Timed Games for Everyone

Gerd Behrmann, Agnès Cougnard, Alexandre David +3 more

Computational Theory and Mathematics · HAL (Le Centre pour la Communication Scientifique Directe) · 3 Apr 2008 · cited 8× · OpenAlex ↗ · more like this ·

Abstract. In 2005 we proposed the first efficient on-the-fly algorithm for solving games based on timed game automata with respect to reachability and safety properties. Since then we have completely re-implemented the first prototype and made dramatic improvements both in terms of performance (several orders of magnitude) and the input language (complete support of all the language features of Uppaal). In addition, the tool supports the new feature of strategy generation with different compactness levels. In this paper we present this new version of Uppaal-Tiga. 1

A Forward Reachability Algorithm for Bounded Timed-Arc Petri Nets

Alexandre David, Lasse Jacobsen, Morten Jacobsen +1 more

cs.LO · 27 Nov 2012 · cited 7× · arXiv ↗ · more like this ·

Timed-arc Petri nets (TAPN) are a well-known time extension of the Petri net model and several translations to networks of timed automata have been proposed for this model. We present a direct, DBM-based algorithm for forward reachability analysis of bounded TAPNs extended with transport arcs, inhibitor arcs and age invariants. We also give a complete proof of its correctness, including reduction techniques based on symmetries and extrapolation. Finally, we augment the algorithm with a novel state-space reduction technique introducing a monotonic ordering on markings and prove its soundness even in the presence of monotonicity-breaking features like age invariants and inhibitor arcs. We implement the algorithm within the model-checker TAPAAL and the experimental results document an encouraging performance compared to verification approaches that translate TAPN models to UPPAAL timed…

A Formal Semantics for UML Statecharts

Alexandre David, Johann Deneux, Julien d’Orso

Artificial Intelligence · KTH Publication Database DiVA (KTH Royal Institute of Technology) · 2003 · cited 7× · OpenAlex ↗ · more like this ·

The UML language is a large set of notations and rules to describe different aspects of a system. It provides a set of diagrams to view the system from different angles: use case diagrams, class diagrams, statecharts diagrams, and deployment diagrams are some of them. In this report we are interested in the statecharts diagrams that describe dynamic behaviours. We give a formal semantics for a large subset of these statecharts, in particular we focus on the action language semantics. Our subset and semantics are very close to the one supported by the tool Rhapsody.

Flexible Framework for Statistical Schedulability Analysis of Probabilistic Sporadic Tasks

Abdeldjalil Boudjadar, Jin Hyun Kim, Alexandre David +5 more

Hardware and Architecture · VBN Forskningsportal (Aalborg Universitet) · April 2015 · cited 3× · DOI ↗ · more like this ·

The analysis of probabilistic schedulability explores all possible combinations of the probabilities of task attributes, which can easily lead to exponential computation time [24]. In this paper, we present a flexible schedulability analysis framework for periodic and sporadic tasks having probabilistic attributes where the computation time scales linearly in the size of analyzed systems. The framework is given in terms of a set of Parameterized Stopwatch Automata (PSA) models, which leads to a large degree of flexibility. Probability distributions for response time are generated using statistical model checking (UPPAAL SMC) while the overall schedulability can be checked using symbolic model checking (UPPAAL). We also define PoMD (percentage of missed deadlines) as a measure of the probabilistic schedulability of systems. To evaluate our approach, we compare the time used for computing…

Adaptive Task Automata with Earliest-Deadline-First Scheduling

Leo Hatvani, Alexandre David, Cristina Seceleanu +1 more

Hardware and Architecture · VBN Forskningsportal (Aalborg Universitet) · 18 Nov 2014 · cited 3× · DOI ↗ · more like this ·

Adjusting to resource changes, dynamic environmental conditions, or new usage modes are some of the reasons why real-time embedded systems need to be adaptive. This requires a rigorous framework for designing such systems, to ensure that the adaptivity does not result in invalidating the system’s real-time constraints. To address this need, we have recently introduced adaptive task automata, a framework for modeling, verification, and schedulability analysis in adaptive, hard real-time embedded systems, assuming a fixed-priority scheduler. In this work, we extend the adaptive task automata framework to incorporate the earliest-deadline-first scheduling policy, as well as enable implementation of any other dynamic scheduling policy. To prove the decidability of our model, and at the same time maintain a manageable degree of conciseness, we show an encoding of our model as a network of…