Subsequence Invariants
Klaus Dräger
In this thesis, we introduce subsequence invariants, a new class of invariants for the specification and verification of systems. Unlike state invariants, which refer to the state variables of the system, subsequence invariants characterize the behavior of a concurrent system in terms of the occurrences of sequences of synchronization events.
The first type of such invariants, pure subsequence invariants, are linear constraints over the possible numbers of such occurrences, where we allow every occurrence of a subsequence to be interleaved arbitrarily with other events. We then describe the more general class of phased subsequence invariants, in which additional restrictions can be placed on the events that may occur between those of a given sequence. In either case, subsequence invariants are preserved when a given process is composed with additional processes. subsequence invariants can therefore be computed individually for each process and then be used to reason about the full system.
We present an efficient algorithm for the computation of subsequence invariants of finite-state systems. Our construction can be applied incrementally to obtain a growing set of invariants given a growing set of event sequences. We then address the problem of proving subsequence invariants of infinite-state systems. For this we use an abstraction refinement procedure that uses small, incrementally transformed graph-based abstractions. In order to explain the techniques we use, we first introduce a simpler version of this method for statebased properties, and then show how to verify subsequence invariants.
PhD Thesis.