Invited Talk

Modular Performance Analysis of Distributed Embedded Systems

Abstract

Embedded computer systems are getting increasingly distributed. This can not only be seen on a small scale, e.g. in terms of multiprocessors on a chip, but also in terms of embedded systems that are connected via various communication networks. Whereas classical methods from the worst case timing analysis and real-time community focus on single resources, new models and methods need to be developed that enable the design and analysis of systems that guarantee end-to-end properties.

The talk covers a new class of methods based on real-time calculus. They can be considered as a deterministic variant of queuing theory and allow for (a) bursty input events and event streams, (b) heterogeneous composition of scheduling methods (EDF, FP, TDMA, WFQ, ...), (c) distributed computation and communication resources (d) detailed modeling of event stream correlations and resource behavior and (d) hard worst case bounds. In addition, the methods have been combined with formal assume/guarantee interfaces. Besides introducing the basic models and methods, some application studies are covered also.

It appears that this class of new methods provide a major step towards the analysis and design of predictable distributed systems.

Lothar Thiele

Logic and Specification

Real Time Temporal Logic: Past, Present, Future

Abstract

This paper attempts to improve our understanding of timed languages and their relation to timed automata. We start by giving a constructive proof of the folk theorem stating that timed languages specified by the past fragment of mitl, can be accepted by deterministic timed automata. On the other hand we provide a proof that certain languages expressed in the future fragment of mitl are not deterministic, and analyze the reason for this asymmetry.

Oded Maler, Dejan Nickovic, Amir Pnueli

Translating Timed I/O Automata Specifications for Theorem Proving in PVS

Abstract

Timed Input/Output Automaton (TIOA) is a mathematical framework for specification and analysis of systems that involve discrete and continuous evolution. In order to employ an interactive theorem prover in deducing properties of a TIOA, its state-transition based description has to be translated to the language of the theorem prover. In this paper, we describe a tool for translating TIOA to the language of the Prototype Verification System (PVS)—a specification system with an integrated interactive theorem prover. We describe the translation scheme, discuss the design decisions, and briefly present three case studies to illustrate the application of the translator in the verification process.

Hongping Lim, Dilsun Kaynar, Nancy Lynch, Sayan Mitra

Specification and Refinement of Soft Real-Time Requirements Using Sequence Diagrams

Abstract

Soft real-time requirements are often related to communication in distributed systems. Therefore it is interesting to understand how UML sequence diagrams can be used to specify such requirements. We propose a way of integrating soft real-time requirements in sequence diagram specifications by adding probabilities to timed sequence diagrams. Our approach builds on timed STAIRS, which is an approach to the compositional and incremental development of sequence diagrams supporting specification of mandatory as well as potential behavior.

Atle Refsdal, Knut Eilif Husa, Ketil Stølen

Times Games and Synthesis

On Optimal Timed Strategies

Abstract

In this paper, we study timed games played on weighted timed automata. In this context, the reachability problem asks if, given a set T of locations and a cost C, Player 1 has a strategy to force the game into T with a cost less than C no matter how Player 2 behaves. Recently, this problem has been studied independently by Alur et al and by Bouyer et al. In those two works, a semi-algorithm is proposed to solve the reachability problem, which is proved to terminate under a condition imposing the non-zenoness of cost. In this paper, we show that in the general case the existence of a strategy for Player 1 to win the game with a bounded cost is undecidable. Our undecidability result holds for weighted timed game automata with five clocks. On the positive side, we show that if we restrict the number of clocks to one and we limit the form of the cost on locations, then the semi-algorithm proposed by Bouyer et al always terminates.

Thomas Brihaye, Véronique Bruyère, Jean-François Raskin

Average Reward Timed Games

Abstract

We consider real-time games where the goal consists, for each player, in maximizing the average reward he or she receives per time unit. We consider zero-sum rewards, so that a reward of +r to one player corresponds to a reward of –r to the other player. The games are played on discrete-time game structures which can be specified using a two-player version of timed automata whose locations are labeled by reward rates. Even though the rewards themselves are zero-sum, the games are not, due to the requirement that time must progress along a play of the game.

Since we focus on control applications, we define the value of the game to a player to be the maximal average reward per time unit that the player can ensure. We show that, in general, the values to players 1 and 2 do not sum to zero. We provide algorithms for computing the value of the game for either player; the algorithms are based on the relationship between the original, infinite-round game, and a derived game that is played for only finitely many rounds. As memoryless optimal strategies exist for both players in both games, we show that the problem of computing the value of the game is in NP∩coNP.

Bo Thomas Adler, Luca de Alfaro, Marco Faella

Beyond Liveness: Efficient Parameter Synthesis for Time Bounded Liveness

Abstract

In this paper, we deal with the problem of parameter synthesis for a subset of parameterised TCTL over timed automata. The problem was proved decidable by V. Bruyere et al. in [10] for general parameterised TCTL using a translation to Presburger arithmetic and also considered by F. Wang in [13] using a parametric region construction. In contrast, we provide two efficient zone based algorithms for a useful subset of parameterised TCTL. The subset has obvious applications to worst case execution time (WCET) analysis. In [11] WCET is performed via model checking, but their approach uses a binary search strategy over several invocations of the model checker. In contrast, both our algorithms synthesise the bound directly. We provide experimental results based on a prototype implementation in Uppaal for two case studies: The first concerns response time analysis of a well known train gate scenario. The second is an execution time analysis of task graph problems where tasks have uncertain execution times.

Gerd Behrmann, Kim G. Larsen, Jacob Illum Rasmussen

Invited Talk

Verification of Parameterized Timed Systems

Abstract

One of the prominent methods for program verification is that of model checking [CES86,QS82]. In the last decade there has been an extensive research effort in order to extend the applicability of model checking to systems with infinite state spaces. There are at least two reasons why a system may be infinite-state:

– A system may operate on data structures with unbounded domains. Examples include real-valued clocks in timed automata [AD94], stacks in push-down automata [BEM97], queues in communicating processes [AJ96], counters in counter machines, etc.

– A system can also be infinite-state because it is parameterized. This means that the description of the system is parameterized by the number of components inside the system. In such a case, we would like to verify correctness of the system regardless of the number of processes.

We consider systems which contain both sources of infiniteness; namely parameterized systems of processes each of which behaves as a timed automaton.

Parosh Aziz Abdulla

Model Checking

Model Checking the Time to Reach Agreement

Abstract

The timed automaton framework of Alur and Dill is a natural choice for the specification of partially synchronous distributed systems (systems which have only partial information about timing, e.g., only an upper bound on the message delay). The past has shown that verification of these systems by model checking usually is very difficult. The present paper demonstrates that an agreement algorithm of Attiya et al, which falls into a – for model checkers – particularly problematic subclass of partially synchronous distributed systems, can easily be modeled with the Uppaal model checker, and that it is possible to analyze some interesting and non-trivial instances with reasonable computational resources. Although existing techniques are used, this is an interesting case study in its own right that adds to the existing body of experience. Furthermore, the agreement algorithm has not been formally verified before to the author’s knowledge.

Martijn Hendriks

Diagonal Constraints in Timed Automata: Forward Analysis of Timed Systems

Abstract

Timed automata (TA) are a widely used model for real-time systems. Several tools are dedicated to this model, and they mostly implement a forward analysis for checking reachability properties. Though diagonal constraints do not add expressive power to classical TA, the standard forward analysis algorithm is not correct for this model. In this paper we survey several approaches to handle diagonal constraints and propose a refinement-based method for patching the usual algorithm: erroneous traces found by the classical algorithm are analyzed, and used for refining the model.

Patricia Bouyer, François Laroussinie, Pierre-Alain Reynier

A New Verification Procedure for Partially Clairvoyant Scheduling

Abstract

In this paper, we describe a new algorithm for the problem of checking whether a real-time system has a Partially Clairvoyant schedule (PCS). Existing algorithms for the PCS problem are predicated on sequential quantifier elimination, i.e., the innermost quantifier is eliminated first, followed by the next one and so on. Our technique is radically different in that the quantifiers in the schedulability specification are eliminated in arbitrary fashion. We demonstrate the usefulness of this technique by achieving significant performance improvement over a wide range of inputs. Additionally, the analysis developed for the new procedure may find applications in domains such as finite model theory and classical logic.

K. Subramani, D. Desovski

Invited Talk

Timing Analysis and Simulation Tools for Real-Time Control

Abstract

The temporal non-determinism introduced by computing and communication in the form of delay and jitter can lead to significant performance degradation. To achieve good performance in systems with limited computer resources, e.g. embedded systems, the resource constraints of the implementation platform must be taken into account at design time. To facilitate this, software tools are needed to analyze and simulate how the timing affects the control performance. Recently two new such tools, JITTERBUG and TRUETIME have been developed at the Department of Automatic Control, Lund University.

Karl-Erik Årzén

Hybrid Systems

Automatic Rectangular Refinement of Affine Hybrid Systems

Abstract

We show how to automatically construct and refine rectangular abstractions of systems of linear differential equations. From a hybrid automaton whose dynamics are given by a system of linear differential equations, our method computes automatically a sequence of rectangular hybrid automata that are increasingly precise overapproximations of the original hybrid automaton. We prove an optimality criterion for successive refinements. We also show that this method can take into account a safety property to be verified, refining only relevant parts of the state space. The practicability of the method is illustrated on a benchmark case study.

Laurent Doyen, Thomas A. Henzinger, Jean-François Raskin

Reachability Problems on Extended O-Minimal Hybrid Automata

Abstract

Within hybrid systems theory, o-minimal automata are often considered on the border between decidability and undecidability. In such classes of hybrid automata, the constraint of having only constant reset upon discrete jumps is a strong limitation for their applicability: hence, an important issue for both theoreticians and practitioners, is that of relaxing the above constraint, while not fall into undecidability.

In this paper we start considering the problem of timed-bounded reachability on o-minimal automata. This can be seen either as a reachability problem paired with time-constraints or as a classical reachability problem for a class of hybrid automata which properly extends the o-minimal one, with an extra variable representing time. Then, we directly face the problem of extending o-minimal automata by allowing some variables to retain their values upon a discrete jump, without crossing the undecidability border.

Raffaella Gentilini

Counterexamples for Timed Probabilistic Reachability

Abstract

The inability to provide counterexamples for the violation of timed probabilistic reachability properties constrains the practical use of CSL model checking for continuous time Markov chains (CTMCs). Counterexamples are essential tools in determining the causes of property violations and are required during debugging. We propose the use of explicit state model checking to determine runs leading into property offending states. Since we are interested in finding paths that carry large amounts of probability mass we employ directed explicit state model checking technology to find such runs using a variety of heuristics guided search algorithms, such as Best First search and Z*. The estimates used in computing the heuristics rely on a uniformisation of the CTMC. We apply our approach to a probabilistic model of the SCSI-2 protocol.

Husain Aljazzar, Holger Hermanns, Stefan Leue

Petri Nets

Time Supervision of Concurrent Systems Using Symbolic Unfoldings of Time Petri Nets

Abstract

Monitoring real-time concurrent systems is a challenging task. In this paper we formulate (model-based) supervision by means of hidden state history reconstruction, from event (e.g. alarm) observations. We follow a so-called true concurrency approach using time Petri nets: the model defines explicitly the causal and concurrency relations between the observable events, produced by the system under supervision on different points of observation, and constrained by time aspects. The problem is to compute on-the-fly the different partial order histories, which are the possible explanations of the observable events. We do not impose that time is observable: the aim of supervision is to infer the partial ordering of the events and their possible firing dates. This is achieved by considering a model of the system under supervision, given as a time Petri net, and the on-the-fly construction of an unfolding, guided by the observations. Using a symbolic representation, this paper presents a new definition of the unfolding of time Petri nets with dense time.

Thomas Chatain, Claude Jard

Comparison of the Expressiveness of Timed Automata and Time Petri Nets

Abstract

In this paper we consider the model of Time Petri Nets (TPN) where time is associated with transitions. We also consider Timed Automata (TA) as defined by Alur & Dill, and compare the expressiveness of the two models w.r.t. timed language acceptance and (weak) timed bisimilarity. We first prove that there exists a TA \(\mathcal{A}\) s.t. there is no TPN (even unbounded) that is (weakly) timed bisimilar to \(\mathcal{A}\). We then propose a structural translation from TA to (1-safe) TPNs preserving timed language acceptance. Further on, we prove that the previous (slightly extended) translation also preserves weak timed bisimilarity for a syntactical subclass \(\mathcal{T}_{syn}(\leq,\geq)\) of TA. For the theory of TPNs, the consequences are: 1) TA, bounded TPNs and 1-safe TPNs are equally expressive w.r.t. timed language acceptance; 2) TA are strictly more expressive than bounded TPNs w.r.t. timed bisimilarity; 3) The subclass \(\mathcal{T}_{syn}(\leq,\geq)\), bounded and 1-safe TPNs “à la Merlin” are equally expressive w.r.t. timed bisimilarity.

Beatrice Bérard, Franck Cassez, Serge Haddad, Didier Lime, Olivier H. Roux

Semantics

Quantifying Similarities Between Timed Systems

Abstract

We define quantitative similarity functions between timed transition systems that measure the degree of closeness of two systems as a real, in contrast to the traditional boolean yes/no approach to timed simulation and language inclusion. Two systems are close if for each timed trace of one system, there exists a corresponding timed trace in the other system with the same sequence of events and closely corresponding event timings. We show that timed CTL is robust with respect to our quantitative version of bisimilarity, in particular, if a system satisfies a formula, then every close system satisfies a close formula. We also define a discounted version of CTL over timed systems, which assigns to every CTL formula a real value that is obtained by discounting real time. We prove the robustness of discounted CTL by establishing that close states in the bisimilarity metric have close values for all discounted CTL formulas.

Thomas A. Henzinger, Rupak Majumdar, Vinayak S. Prabhu

Performance of Pipelined Asynchronous Systems

Abstract

A testing-based faster-than relation has previously been developed that compares the worst-case efficiency of asynchronous systems. This approach reveals that pipelining does not improve efficiency in general; that it does so in practice depends on assumptions about the user behaviour. Accordingly, the approach was adapted to a setting where user behaviour is known to belong to a specific, but often occurring class of request-response behaviours; some quantitative results on the efficiency of the respective so-called response processes were given. In particular, it was shown that in the adapted setting a very simple case of pipelined process with two stages is faster than a comparable atomic processing. In this paper, we determine the performance of general pipelines, study whether the adapted faster-than relation is compatible with chaining (used to build pipelines) and two other operators, and give results on the performance of the resp. compositions, demonstrating also how rich the request-respond setting is.

Flavio Corradini, Walter Vogler

Is Timed Branching Bisimilarity an Equivalence Indeed?

Abstract

We show that timed branching bisimilarity as defined by van der Zwaag [14] and Baeten & Middelburg [2] is not an equivalence relation, in case of a dense time domain. We propose an adaptation based on van der Zwaag’s definition, and prove that the resulting timed branching bisimilarity is an equivalence indeed. Furthermore, we prove that in case of a discrete time domain, van der Zwaag’s definition and our adaptation coincide.

Wan Fokkink, Jun Pang, Anton Wijs

Semantics and Modelling

Implementation of Timed Automata: An Issue of Semantics or Modeling?

Abstract

We examine to what extent implementation of timed automata can be achieved using the standard semantics and appropriate modeling, instead of introducing new semantics. We propose an implementation methodology which allows to transform a timed automaton into a program and to check whether the execution of this program on a given platform satisfies a desired property. This is done by modeling the program and the execution platform, respectively, as an untimed automaton and a collection of timed automata. We also study the problem of property preservation, in particular when moving to a “better” execution platform. We show that some subtleties arise regarding the definition of “better”, in particular for digital clocks. The fundamental issue is that faster clocks result in better “sampling” and therefore can introduce more behaviors.

Karine Altisen, Stavros Tripakis

Timed Abstract Non-interference

Abstract

In this paper, we introduce a timed notion of abstract non-interference. This is obtained by considering semantics which observe time elapsed in computations. Timing channels can be modeled in this way either by letting the attacker to observe time as a public variable or reckon the time elapsed by observing the computational traces’ length, corresponding to observe the program counter. In the first case abstract non-interference provides a model for abstracting the information about time, namely we can for example consider models of attackers that can observe only intervals of time, or other more abstract properties. In the second case abstract non-interference provides a model for attackers able to observe properties of trace length, e.g., the public memory during the whole computation. We investigate when adding the observation of time does not increase the attacker’s power in disclosing confidential information about data. This models the absence of timing channels in language-based security.

Roberto Giacobazzi, Isabella Mastroeni

Springer Professional

Formal Modeling and Analysis of Timed Systems

Third International Conference, FORMATS 2005, Uppsala, Sweden, September 26-28, 2005. Proceedings

Inhaltsverzeichnis

Frontmatter

Invited Talk

Modular Performance Analysis of Distributed Embedded Systems

Logic and Specification

Real Time Temporal Logic: Past, Present, Future

Translating Timed I/O Automata Specifications for Theorem Proving in PVS

Specification and Refinement of Soft Real-Time Requirements Using Sequence Diagrams

Times Games and Synthesis

On Optimal Timed Strategies

Average Reward Timed Games

Beyond Liveness: Efficient Parameter Synthesis for Time Bounded Liveness

Invited Talk

Verification of Parameterized Timed Systems

Model Checking

Model Checking the Time to Reach Agreement

Diagonal Constraints in Timed Automata: Forward Analysis of Timed Systems

A New Verification Procedure for Partially Clairvoyant Scheduling

Invited Talk

Timing Analysis and Simulation Tools for Real-Time Control

Hybrid Systems

Automatic Rectangular Refinement of Affine Hybrid Systems

Reachability Problems on Extended O-Minimal Hybrid Automata

Counterexamples for Timed Probabilistic Reachability

Petri Nets

Time Supervision of Concurrent Systems Using Symbolic Unfoldings of Time Petri Nets

Comparison of the Expressiveness of Timed Automata and Time Petri Nets

Semantics

Quantifying Similarities Between Timed Systems

Performance of Pipelined Asynchronous Systems

Is Timed Branching Bisimilarity an Equivalence Indeed?

Semantics and Modelling

Implementation of Timed Automata: An Issue of Semantics or Modeling?

Timed Abstract Non-interference

Backmatter