| | All
sessions take place in auditorium 10.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. |
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. |
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. |
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. |
| |