Verification of Large Systems: Some recent Approaches

Amir Pnueli

Department of Computer Science, Weizmann Institute

In this talk we will survey some recent new developments in the methods for verification of large reactive systems, including developments in the two most prominent approaches to verification: the Deductive and Algorithmic (Model-Checking) approaches. We will introduce the notion of symbolic model checking over an arbitrarily expressive assertional language, and show how it can be used for the uniform verification of parameterized designs for any configuration. We will show that this method, developed in the model-checking context, is dual to the "successive strengthening" algorithm used in deductive verification in order to derive inductive invariants. Considering verification of large hardware designs, we will formulate the problem of verifying designs for out-of-order execution by micro-processors. First, we will present a deductive method based on refinement (proved by simulation) for comparing the out-of-order design with the reference model of sequential execution. Then, we indicate some cases for which the problem can be algorithmically solved.


Types as Processes

Vaughan Pratt

Department of Computer Science, Stanford University

Data and events are ordinarily regarded as static and dynamic respectively. We propose a common organization of types and processes, based on a blend of linear logic and process algebra, aimed at transcending this distinction. This unification works better with some combinators of type theory and process algebra than others. In particular linear logic's plus or coproduct connective corresponds nicely to process algebra's noninteracting parallel composition operator, and tensor product matches up perfectly with orthocurrence. However linear implication (function spaces) and par defy our dynamic intuitions, while process algebra's choice operations have no obvious role in type theory, and the obvious link between function composition or cut and sequential composition matches not types but transformations to processes. We pose the question of whether these mismatches are intrinsic or cultural, and explore some of the surrounding issues.


Tiles for Concurrent and Causal Calculi

GianLuigi Ferrari and Ugo Montanari

Dipartimento di Informatica, Universita' di Pisa

A large number of non-interleaving models of process calculi have been developed. Usually these models take the form of labelled transition systems whose labels are enriched with additional features that make {\em deriving} causal dependencies possible. In this paper, we consider the problem of providing an abstract setting where (truly) concurrent and causal behaviours are captured {\em directly} as a result of structural definitions. More precisely we introduce a tile-based operational semantics for CCS and we show it equivalent to the ordinary causal (i.e. history preserving bisimulation) and concurrent (i.e. permutation of transitions) semantics. Tiles are rewrite rules with side effects, reminiscent of both Plotkin SOS and Meseguer rewriting logic rules. We argue that the tile model is particularly well suited for defining non interleaving semantics of process calculi directly in a SOS style.


Last Updated: 24 July 1997 by Catuscia Palamidessi