Equivalences, preorders and compositional verification for linear time temporal logic and concurrent systems

Roope Kaivola: Equivalences, preorders and compositional verification for linear time temporal logic and concurrent systems. PhD Thesis, Report A-1996-1, Department of Computer Science, University of Helsinki, March 1996. 176+9 pages. <http://www.cs.helsinki.fi/TR/A-1996/1>

Full paper: gzip'ed Postscript file
Metadata: XML file

Abstract

A promising approach to formal specification and verification of finite-state concurrent systems is using propositional temporal logic as a specification language and applying automated model-checking algorithms for the verification task. However, the so-called state explosion-problem caused by representing concurrency by interleaving makes model-checking in many cases practically intractable. One way of attacking this problem is replacing the modules of a system by smaller ones so that the visible properties of the system are not affected. This approach leads to notions of compositional property-preserving equivalences and preorders between modules.

This work examines the uses of equivalences and preorders in verifying nexttime-less linear temporal logic properties. Concurrent systems are modelled here by labelled transition systems augmented with state information, and both synchronization and read-shared variables are considered as methods of communication. We examine a novel equivalence notion, called the non-divergent failures divergences or NDFD-equivalence. It is shown that NDFD preserves all nexttime-less linear temporal logic properties, and that it is compositional with respect to parallel composition and abstraction by hiding and encapsulation. Conversely, it is shown that NDFD is the weakest such equivalence, i.e. that it is fully abstract with respect to preserving nexttime-less linear temporal logic properties in an arbitrary context. The computational complexity of determining NDFD-equivalence is also examined and the problem is shown to be PSPACE-complete.

Analogous to NDFD-equivalence, the theory of NDFD-preorder is developed and the compositionality, full abstractness and computational complexity results extended to it. Moreover, it is shown that the verification technique of modular validity introduced by Manna and Pnueli corresponds to an extremal case of NDFD-preorder. As a larger case study illustrating the practical applications of the results, we use the NDFD-preorder to verify semi-automatically both safety and liveness properties of the sliding window communication protocol for arbitrary channel lengths and realistic parameter values. In this process we locate a previously undiscovered fault leading to lack of liveness in a version of the protocol.

Index Terms

Categories and Subject Descriptors:
F.3.1 [Specifying and verifying and reasoning about programs]: logics of programs, mechanical verification, specification techniques,
F.1.2 [Modes of computation]: concurrency
D.2.4 [Program verification]
C.2.2 [Network protocols]: protocol verification

General Terms: Theory, Verification

Additional Key Words and Phrases: concurrency, equivalences, preorders, specification, temporal logic