Parosh Abdulla  Jurgen Giesl  Radu Grosu  Neil Jones  Orna Kupferman  Kim Larsen  Chin Soon Lee  Axel Legay  Berhard Steffen  Wang Yi 

We consider verification of safety properties for parameterized systems of timed processes, so called timed networks. A timed network consists of a finite state process, called a controller, and an arbitrary set of identical timed processes. We show that checking safety properties and some simple classes of liveness properties are decidable in the case where each timed process is equipped with a single real-valued clock. We show that these problems become undecidable when each timed process has two clocks.

On the other hand, we show that the problems are decidable when clocks range over a discrete time domain. The decidability results hold when processes have any finite number of clocks.

A "liveness property" states that eventually (after a finite number of steps) some requirement holds. One of the most essential liveness properties in software verification is termination. Methods for automated termination analysis have been studied for decades in areas like logic programming and term rewriting. We give an overview on techniques to prove termination of term rewrite systems automatically. Starting from classical approaches, we also present new methods like the "dependency pair" approach, which extends the applicability of classical techniques for automated termination analysis significantly. The talk also includes a demonstration of our automated termination prover AProVE which illustrates that the techniques discussed can be mechanized efficiently.

Moreover, we demonstrate that techniques for termination analysis are also useful to verify other liveness properties as well. To this end, we show how dependency pairs were applied at Ericsson Telecom in order to verify liveness properties of a protocol for concurrent telecommunication processes.

We present what we believe to be the first randomized, Monte Carlo algorithm for model checking, the problem of deciding whether or not a property specified in temporal logic holds of a system specification. Given an epsilon, delta, a succinct representation S of the system under investigation, and a Linear Temporal Logic formula varphi, our algorithm computes an estimate of the probability that S satisfies varphi within a factor of 1 +/- epsilon with probability at least 1 - delta. It does so using a number of samples N that is optimal to within a constant factor, and in expected time O(N*(|S|+|varphi|)) and expected space O(|S|+|varphi|).

Real software in application areas, such as avionic controls, primarily concerns {\em reactive systems} that are intended to run indefinitely in acontext of continual interactions,e.g., with an operatingsystem, with the outside world via sensors/actuators, and with inputs provided online by humans.

{\em Safety properties} ensure that nothing can go wrong (e.g.,divide by zero or dereference an invalid pointer), and {\em livenessproperties} ensure that the system will continue to provideservices, and thus be responsive (rather than loop indefinitely or ignorecertain kinds of requests).

We propose to develop and experiment with {\em resource-usage analyses}well-suited to the kinds of problems of interest to real software systems,in particular unboundedness of resource usage. Resource-usage analyses will require detection methods stronger than traditional abstract interpretation or program flow analysis in optimising compilers. Some relevant concepts come from model-checking(although it is most often applied to circuits and embedded systems).Safety and liveness cannot be studied in isolation, since (un)safety can have an impact on liveness. Roughly: an unsafe systemthat crashes due to a single illegal operation can no longer respond, and is thus no longer live. Further, an {\em unbounded usage} of a limited resource will {\em eventually compromise liveness by violating safety}, once an overrun occurs. Such ``overflow'' can be of: stack or heap size, buffer size, or integer or floating point word sizes.The core problem is how to detect potentially unbounded resource usage. This is not solvable in practice by assigning fixed a priori limits to buffer length, stack size, etc. since the number of possibleconfigurations in real systems is far too large to analyse exhaustively.We plan to address some problems by analytic and type-based methods:- Program termination (stronger, and applicable to more programs). - Avoiding unboundedness in values of variables.- Avoiding unboundedness in stack and heap usage.- Bounding program running times. A novel program analysis that is particularly relevant is ``quasi-termination analysis.'' This analysis determines whether a program, for every one of its inputs, executes within a finite total state space, and therefore can be executed if given sufficiently large resources.

Two basic liveness properties are reachability (T holds eventually) and repeated reachability (T holds infinitely often). The talk relates reachability in a probabilistic setting with repeated reachability in a non-probabilistic setting. Intuitively, requiring an event T to hold eventually with probability 1 has the same flavor as requiring events that lead to T to hold infinitely often. The intuition can be formalized by means of reductions between probabilistic reachability games and non-probabilistic repeated reachability games. The above phenomenon of probability being traded for a stronger fairness condition, and vice-versa, is general, and can be shown for other fairness conditions.

The "size-change" approach for termination analysis of first-order functional programs with well-founded data, as proposed by Lee, Jones and Ben-Amram (2001), is divided into 2 stages.

In the first stage, abstract interpretation is used to deduce parameter size-changes observed at potential function calls. (Of interest are size decreases and non-increases.) This information is summarized in a set of "size-change graphs." In the second stage, it is decided _precisely_ whether every infinite call sequence would give rise to infinite descent in the size of some parameter values, _according to the graphs_. If this is the case, the graphs are said to satisfy "size-change termination" (SCT). It follows that no infinite call sequence is possible, therefore the subject program is terminating.

Since this work, SCT has been incorporated in the Agda Theorem Prover (Wahlstedt 2000), adapted for term-rewriting systems (Thiemann and Giesl 2001), used in a running-time analysis (Frederiksen and Jones 2003), and applied to higher-order programs (Jones and Bohr 2004). Part of the attractiveness of the SCT approach is its simplicity. Wahlstedt, Thiemann and Giesl also believe it to be an efficient way to "simulate the main ingredients of RPOS, i.e., the concept of lexicographic and multiset comparison."

However, the SCT condition is complete for PSPACE. Moreover, "permuted arguments" trigger exponential behaviour in its decision procedure. In this talk, we present a worst-case quadratic-time approximation that captures common parameter-descent behaviours. We have empirical evidence that the approximation is efficient and sufficiently precise in practice.

Since the topic emerged several years ago, work on regular model checking has mostly been devoted to the verification of state reachability and safety properties. Though it was known that liveness properties could also be checked within this framework, little has been done about working out the corresponding details, and experimentally evaluating the approach. This work addresses these issues in the context of regular model checking based on the encoding of states by finite or infinite words. It works out the exact constructions to be used in both cases, and solves the problem resulting from the fact that infinite computations of unbounded configurations might never contain the same configuration twice, thus making cycle detection problematic. Several experiments showing the applicability of the approach were successfully conducted.

The talk will discuss what (liveness) properties make sense as a basis for optimizing program transformations. In this course it will distinguish three kinds of liveness properties
- bounded liveness
- conditional liveness
- unconditional liveness

In many real-time computing environments, there are some tasks that are time-critical and others that are not. To ensure that every critical task is completed before its deadline, it may be necessary to deny entry -- into the ready queue -- for some non-critical tasks. We address an abstract version of this problem in the framework of controller synthesis. Our goal is to come up with an \emph{admission controller} which admits or rejects a task request, so that no admitted task misses its deadline and the admitted patterns of task releases satisfy an LTL specification. We show that it is decidable to determine if such an admission controller exists. Further, if the answer is positive, it is possible to effectively construct a controller in the form of a timed automata that has a finite number of control locations and clock variables.