International Journal of Foundations of Computer Science

We study the problem of generating a test sequence that achieves maximal coverage for a reactive system under test. We formulate the problem as a repeated game between the tester and the system, where the system state space is partitioned according to some coverage criterion and the objective of the tester is to maximize the set of partitions (or coverage goals) visited during the game. We show the complexity of the maximal coverage problem for non-deterministic systems is PSPACE-complete, but is NP-complete for deterministic systems. For the special case of non-deterministic systems with a re-initializing “reset” action, which represent running a new test input on a re-initialized system, we show that the complexity is coNP-complete. Our proof technique for reset games uses randomized testing strategies that circumvent the exponentially large memory requirement of deterministic testing strategies. We also discuss the memory requirement for deterministic strategies and extensions of our results to other models, such as pushdown systems and timed systems.

We investigate the use of monotonic abstraction and backward reachability analysis as means of performing shape analysis on programs with multiply pointed structures. By encoding the heap as a vertex- and edge-labeled graph, we can model the low level behaviour exhibited by programs written in the C programming language. Using the notion of signatures, which are predicates that define sets of heaps, we can check properties such as absence of null pointer dereference and shape invariants. We report on the results from running a prototype based on the method on several programs such as insertion into and merging of doubly-linked lists.

We identify sufficient conditions to automatically establish the termination of a backward reachability procedure for infinite state systems by using well-quasi-orderings. Besides showing that backward reachability succeeds on many instances of problems covered by general termination results, we argue that it could predict termination also on interesting instances of the reachability problem that are outside the scope of applicability of such general results. We work in the declarative framework of Model Checking Modulo Theories that permits us to exploit recent advances in Satisfiability Modulo Theories solving and model-theoretic notions of first-order logic.

Hybrid systems combine continuous and discrete behavior. Hybrid Automata are a powerful formalism for the modeling and verification of such systems. A common problem in hybrid system verification is the good parameters problem, which consists in identifying a set of parameter valuations which guarantee a certain behavior of a system. Recently, a method has been presented for attacking this problem for Timed Automata. In this paper, we show the extension of this methodology for hybrid automata with linear and affine dynamics. The method is demonstrated with a hybrid system benchmark from the literature.

For each odd n ≥ 5 we present a synchronizing Eulerian automaton with n states for which the minimum length of reset words is equal to . We also discuss various connections between the reset threshold of a synchronizing automaton and a sequence of reachability properties in its underlying graph.

The definition of bisimulation suggests a partition-refinement step, which we show to be suitable for a saturation-based implementation. We compare our fully symbolic saturation-based implementation with the fastest extant bisimulation algorithms over a set of benchmarks, and conclude that it appears to be the fastest algorithm capable of computing the largest bisimulation over very large quotient spaces.

In this work we present an algorithm for solving the reachability problem in finite systems that are modelled with process algebras. Our method is based on Static Analysis, in particular, Data Flow Analysis, of the syntax of a process algebraic system with multi-way synchronisation. The results of the Data Flow Analysis are used in order to build a set of Horn clauses whose least model corresponds to an overapproximation of the reachable states. The computed model can be refined after each transition, and the algorithm runs until either a state whose reachability should be checked is encountered or it is not in the least model for all constructed states and thus is definitely unreachable. The advantages of the algorithm are that in many cases only a part of the Labelled Transition System will be built which leads to lower time and memory consumption. Also, it is not necessary to save all the encountered states which leads to further reduction of the memory requirements of the algorithm.