**Thomas S. Hune**

**March 2001**

The main topic of this dissertation is the development and use
of methods for formal reasoning about the correctness of real-time systems,
in particular methods and tools to handle new classes of problems. In
real-time systems the correctness of the system does not only depend on the
order in which actions take place, but also the timing of the actions. The
formal reasoning presented here is based on (extensions of) the model of
timed automata and tools supporting this model, mainly UPPAAL.
Real-time systems are often part of safety critical systems e.g. control
systems for planes, trains, or factories, though also everyday electronics as
audio/video equipment and (mobile) phones are considered real-time systems.
Often these systems are concurrent systems with a number of components
interacting, and reasoning about such systems is notoriously difficult.
However, since most of the systems are either safety critical or errors in
the systems are costly, ensuring correctness is very important, and hence
formal reasoning can play a role in increasing the reliability of real-time
systems.

We present two classes of cost extended timed automata, where a cost
is associated to an execution of the automaton. We show that
calculating the minimum cost of reaching a location in the automaton,
the minimum-cost reachability problem, is decidable for both
classes. Since a number of optimization problems, e.g. scheduling
problems in a natural way, can be modeled using cost extended timed
automata, we can now solve these problems using extensions of timed
model checkers. The state-space of the simpler class, *uniformly
priced timed automata* (UPTA), which is a subclass of *linearly
priced timed automata* (LPTA), can effectively be represented using a
slightly modified version of the well known difference bounded matrix
(DBM) data-structure for representing zones, used in most timed model
checkers. Using an extension of the region construction, the
minimum-cost reachability problem can also be solved for
LPTAs. However, the standard way of using zones for representing the
state-space cannot be used for LPTAs, since there is no way of
capturing the cost of states. Based on the notion of facets, zones can
be split into smaller zones which can be represented by extended DBMs
in an effective way. Minimum-cost reachability for both UPTAs and
LPTAs have been implemented in extensions of UPPAAL, and
successfully tested on a number of case studies. In particular, part
of the Sidmar steel production plant, which is a case study of the
Esprit VHS project, has been studied. Schedulability, without
considering cost and optimality, has also been addressed using
standard timed automata and UPPAAL. In order to solve the
schedulability problem in UPPAAL it proved crucial to add a
number of *guides* to the model, in order to limit the search
space. In the cost extended versions of UPPAAL, guiding in terms
of changing the order in which states are searched has also been used,
and shown to be effective both for finding solutions to optimization
problems and in ordinary timed model checking.

The second extension of timed automata is parametric timed automata, where parameters can be used in expressions for guards and invariants. We consider the problem of synthesizing values for the parameters ensuring satisfiability of reachability properties. Since there are in most cases infinitely many values ensuring that a property is satisfied, the result is presented in terms of constraints for the parameters. We present a semi-decision procedure synthesizing the constraints. The problem of synthesizing constraints for the parameters has been show to be undecidable. To represent the state-space we extend the DBM data-structure to parametric DBMs, capable of representing zones were the bounds are given by expressions including parameters. The semi-decision procedure is implemented in UPPAAL and constraints ensuring correctness of a number of industrial protocols is synthesized.

Since (timed) reachability checking requires large amounts of resources in terms of memory and CPU time, we have studied the possibility of distributing the reachability checking to a network of computers. We have implemented a distributed version of UPPAAL and tested it on a number of the largest known case studies for UPPAAL. Not only did we achieve effective usage of all the connected computers (close to linear speedup in the number of computers) we also discovered that the breadth-first search order, which previously has been considered to be the best known, is not optimal.

We apply the general categorical framework of *open maps* to timed
automata by presenting a category where the elements are timed
automata, and a subcategory suitably for representing observations,
timed words. Following the framework, maps in the category can be
seen as simulations, and two timed automata and
are timed bisimilar if and only if there exists a timed
automaton and open maps
and
. We show that
this notion of timed bisimulation coincides with the know notion of
timed bisimulation, and using the region construction show that the
bisimulation is decidable.

Building timed automata models of systems can be an error prone and time consuming task. We address this problem by presenting a translation from a low level programming language used in the programmable LEGOpsy226 RCXpsy228 brick to timed automata. Programs for the RCXpsy228 brick can consist of several tasks running concurrently. Therefore an important part of the model of the program is a model of the scheduler. The translation has been implemented and tested on a control program for a car.

Finally, we consider a kind of partial program synthesis for untimed
systems. Given a safety specification written in monadic second order
logic, we use the *Mona* tool to derive an automaton accepting the
language of the specification. The automaton is used to restrict the
executions of a handwritten control program, ensuring that the safety
requirements are met. To demonstrate the approach we consider a
control program for a crane, written for the RCXpsy228
brick. We also discuss more generally what should happen when there is
a conflict between the actions of the control program and the
specification.

Available as *PostScript*,
*PDF*.

BRICS WWW home page