Superposition-Based Specification of Distributed Reactive Systems: the DisCo Approach

The talk will give an overview of how distributed reactive systems are specified using the DisCo approach. The method is distinguished by the use of objects, joint actions, superposition and closed world modeling.

DisCo is a specification language and a specification methodology based on the Temporal Logic of Actions. Specifications are constructed by starting with a very abstract view of the system, specified using objects and their multi-way synchronizations called joint actions. Details are then superimposed layerwise in superposition steps that preserve safety properties by construction. Each layer describes a closed world with respect to some state variables, i.e. it completely characterizes how the values of the variables can change. A system is thus always effectively specified together with its environment. In contrast to many other approaches, a DisCo layer can introduce state variables and functionality to several objects of the system, specifying one aspect of the collective behavior.

We also describe ongoing work in the area of formal verification. By parameterizing a DisCo layer with assumptions about how it may be applied, it is possible to verify safety properties of the layer. These properties become properties of a specification obtained by applying the layer, provided the assumptions can be verified to hold. This makes it possible to package design solutions with verified behavioral properties using DisCo layers. Specifications can then be constructed by composing instantiations of such layers, similarly to how design patterns are used in object-oriented specification.

As part of this work, we have started to build a deep embedding of the DisCo specification language in the logic of the PVS theorem prover. In a deep embedding, semantics of the syntactical forms of DisCo specifications are directly expressed in the embedding logic. This allows us to reason about properties of the DisCo language, which is not a case in a shallow embedding where DisCo specifications are mapped to equivalent theories in PVS. A deep embedding may also be more convenient for the verification of individual specifications, as DisCo specifications contain implicit assumptions about which objects are changed. In a shallow embedding, these assumptions need to be made explicit in the form of large quantified formulas, while in a deep embedding they can be expressed implicitly using recursive functions in PVS.