RT-TOOLS on Thursday

Detailed program
Thursday August 1st, 2002
See also the unified by-slot program

All sessions take place in auditorium 10.

Session 1: Design and Synthesis

09:15-09:30  Welcome

09:30-10:00  Goran Frehse, U Dortmund, Germany
Solving simulation relations of timed automata for the design and verification of timed discrete controllers
The design specifications for timed, but discrete controllers can be verified in the framework of abstractions of timed automata. They are expressed as a simulation relation S||C<P, where S is the plant, C the controller and P the specification. While currently a lot of research, mainly in computer science, goes into refining and verifying abstractions, this contribution emphasises the context of control applications. It presents a compositional proof rule to solve the above inequality for C and is applicable to both verification and design of controllers for systems with a chain-like structure. The concept of a brute force algorithm for solving simulation relations of timed automata is proposed that enables the algorithmic application of the compositional proof rule.

10:00-10:30  Robert P. Goldman, Smart Information Flow Technologies, USA
Michael J. S. Pelican, Honeywell, USA
David J. Musliner, Honeywell, USA
Verifier trace-directed backjumping for controller synthesis
Conventionally, model-checking verification systems return counterexample traces when desired properties are shown to be violated. Unfortunately, these traces often do not directly guide users to system repairs. In this paper, we describe a technique for extracting repair candidates from counterexample traces, in the context of an on-the-fly algorithm for timed automaton controller synthesis (reactive planning). We provide a technique for mapping counterexample traces into nogoods: sets of search stack entries. In turn, these nogoods allow us to use backjumping search in the controller synthesis. Backjumping search is guaranteed to visit fewer nodes than conventional chronological backtracking search, and in many problems visits far less. We present data to show that, in large controller synthesis problem, the use of backjumping provides substantial speedup by removing large portions of the search space, at no sacrifice in completeness.

Session 2: Model-Checking

11:00-11:30  Jesper Møller, IT U of Copenhagen, Denmark
Simplifying fixpoint computations in verification of real-time systems
Symbolic verification of real-time systems consists of computing the least fixpoint of a functional which given a set of states φ returns the states that are reachable from φ (in forward reachability), or that can reach φ (in backward reachability). This paper presents two techniques for simplifying the fixpoint computation: First, I demonstrate that in backwards reachability, clock resets and discrete state changes can be performed as substitutions instead of existential quantifications over reals and Booleans, respectively. Second, I introduce a local-time model for real-time systems which allows clocks to advance asynchronously, thus resulting in an over-approximation of the least fixpoint, but which in some cases is sufficient for verifying a temporal property.

11:30-12:00  Gilles Audemard, ITC-irst, Italy
Alessandro Cimatti, ITC-irst, Italy
Artur Kornilowicz, ITC-irst, Italy
Roberto Sebastiani, ITC-irst, Italy
Bounded model checking for timed systems
Enormous progress has been achieved in the last decade in the verification of timed systems, making it possible to verify significant real-world protocols. An open challenge is the identification of fully symbolic verification techniques, able to deal effectively with the finite state component as well as with the timing aspects. In this paper we propose a new, symbolic verification technique that extends the Bounded Model Checking (BMC) approach for the verification of timed systems. The approach is based on the following ingredients. First, a BMC problem for timed systems is reduced to the satisfiability of a math-formula, i.e., a boolean combination of propositional variables and linear mathematical relations over real variables (used to represent clocks). Then, an appropriate solver, called MathSAT, is used to check the satisfiability of the math-formula. The solver is based on the integration of SAT techniques with some specialized decision procedures for linear mathematical constraints, and requires polynomial memory. Our methods allow for handling expressive properties in a fully-symbolic way. A preliminary experimental evaluation confirms the potential of the approach.

12:00-12:30  Dragan Bosnacki, Eindhoven U of Techn., The Netherlands
Partial order and symmetry reductions for discrete time
Symmetry and partial order reductions are among the most effective techniques for alleviating the state space explosion problem in model checking of untimed systems. In this paper we show how these two techniques can be combined for verification of discrete-time systems. In particular, we work with the discrete-time model used in DT Spin, an extension of the model checker Spin which features partial order reduction for discrete (integer) time. Based on the theoretical results presented in the paper, we combined DT Spin with SymmSpin, an extension of Spin with symmetry reduction, with promising preliminary results.

Session 3: Tool Development

14:00-14:30  Karine Altisen, INRIA Rhône-Alpes, France
Stavros Tripakis, IMAG Grenoble, France
Tools for controller synthesis of timed systems
We present tools for controller synthesis of timed systems. The problem is to find, given a model of a system in the form of a timed automaton with controllable and uncontrollable actions, a state feedback controller such that the closed loop system satisfies a given property. A state feedback controller observes the state the system is in and decides which of the controllable actions to disable and which to enable (or force). We are interested in controllers that ensure invariance properties (an unsafe state is never reached) or inevitability properties (a target state is eventually reached), without blocking the system. We present two tools, based on two different approaches. The module KroSynth of the tool-suite Kronos is based on a backward fix-point iteration of an appropriate symbolic predecessor operator. The tool FlySynth which performs forward on-the-fly synthesis on finite graphs. We show how FlySynth can be used for timed synthesis, either by assuming a discrete-time semantics, or by generating first the time-abstracting bisimulation quotient of a timed automaton. We illustrate the two tools with a number of case studies.

14:30-15:00  Alexandre David, Uppsala U, Sweden
Gerd Behrmann, Aalborg U, Denmark
Kim Guldstrand Larsen, Aalborg U, Denmark
Wang Yi, Uppsala U, Sweden
New uppaal architecture
We present the design and internal data structures for the next generation of UPPAAL. Early experimental results demonstrate that the new implementation based on these structures improves the efficiency of UPPAAL by about 80% in both time and space. In addition, the new version is built to handle hierarchical models. The challenge in handling hierarchy comes from the very dynamic structure of hierarchical systems: the levels of concurrency and the scope of data variables and clocks are changing. We present data structures and a searching scheme for state space exploration of hierarchical models.

15:00-15:30  Anton Cervin, Lund Inst. of Techn., Sweden
Dan Henriksson, Lund Inst. of Techn., Sweden
Bo Lincoln, Lund Inst. of Techn., Sweden
Karl-Erik Årzén, Lund Inst. of Techn., Sweden
Jitterbug and TrueTime: Analysis tools for real-time control systems
The paper presents two recently developed, MATLAB based analysis tools for real-time control systems. The first tool, called JITTERBUG, is used to compute a performance criterion for a control loop under various timing conditions. The tool makes it easy to quickly judge how sensitive a controller is to implementation effects such as slow sampling, delays, jitter, etc. The second tool, called TRUETIME, allows detailed co-simulation of process dynamics, control task execution, and network communication in a distributed real-time control system. Arbitrary scheduling policies may be used, and the tasks may be written in C code, MATLAB code, or implemented as Simulink block diagrams.

Session 4: Applications

16:00-16:30  Béatrice Bérard, ENS Cachan, France
Patricia Bouyer, Aalborg U, Denmark
Antoine Petit, ENS Cachan, France
Analysing the PGM protocol with uppaal
Pragmatic General Multicast (PGM) is a reliable multicast protocol, designed to minimize both the probability of negative acknowledgements (NAK) implosion and the loading of the network due to retransmissions of lost packets. This protocol was presented to the Internet Engineering Task Force as an open reference specification. In this paper, we focus on the main reliability property which PGM intends to guarantee: a receiver either receives all data packets from transmissions and repairs or is able to detect unrecoverable data packet loss. To this purpose, we propose a modelization of (a simplified version of) PGM via a network of timed automata. Using UPPAAL model-checker, we then study the validity of the reliability property above, which turns out to not be always verified but to depend of the values of several parameters that we underscore.

16:30-17:00  Martin Carlsson, Enea OSE Systems AB, Sweden
Jakob Engblom, IAR Systems AB, Sweden
Andreas Ermedahl, Uppsala U, Sweden
Jan Lindblad, Enea OSE Systems AB, Sweden
Björn Lisper, Mälardalen U, Sweden
Worst-case execution time analysis of disable interrupt regions in a commercial real-time operating system
Worst-Case Execution Time (WCET) analysis has been around for some time now, but has so far not been much used to analyse real production codes. Here, we present a case study where static WCET analysis was used to find upper time bounds for time-critical regions in a commercial real-time operating system. We report on practical experiences from the work, like the reverse engineering required to find these regions and prepare them for the analysis. We give the results of the WCET analysis and discuss the precision. We also present some qualitative and quantitative data on the program structure of the regions. This information is useful to judge whether WCET analysis could provide any useful results for this class of real codes, without excessive manual labour. Finally, we present a "wishlist" for features of WCET analysis tools, which has emerged during the project, and comment on the feasibility of implementing these features.