The DisCo Home Page

The DisCo Language

The DisCo language has been designed for the specification of reactive systems, with emphasis on distributed systems. It is capable of describing a system together with its environment at a high level of abstraction. The level of abstraction can be refined stepwise towards an implementation. Specifications written in DisCo are executable in the sense that there is a well-defined execution model and an animation tool that can be used for exploring the behaviors induced by a DisCo specification. A straightforward implementation using the execution model of the specification language may not be practical, however.

The language outlined here is DisCo98, but most of the discussion also applies to DisCo92. For a complete description of DisCo92, see the reference manual.

Objects, Actions, and Relations

The world described by a DisCo specification consists of objects, actions, and relations. Objects are described by class definitions, actions by action definitions, and relations by relation definitions. A simple example illustrating the definitions is the following:

layer example is

  class node is
    value : integer;
  end;

  relation neighbors(left, right : node) : 1:1;

  action swap
  by l, r : node            -- participants
  when neighbors(l,r)       -- guard
     and l.value < r.value
  do
    l.value := r.value      -- body
    || r.value := l.value;  
  end;
end;

As given, the definition of node does not restrict the number of nodes in any way. The specification is thus a template describing a class of systems. If a specification for a specific number of nodes is desired, additional constraints may be given.

The relation neighbors associates nodes with each other, and the constraint 1:1 specifies that neighbors is a one-to-one relationship.

An action specifies the participants of the action by a collection of roles. The roles are formal names, similar to the parameters of a subroutine. When the action is executed, the roles are bound to actual objects. The guard specifies when the action is enabled. When several actions are enabled, or one is enabled for several combinations of participants, the selection is nondeterministic. Executing the body changes the attributes of the object bound to the roles, so after executing swap the values held by the participants have been swapped.

An action may also have optional parameters, which represent nondeterministically chosen values. Such values are usefulf for example when modeling arbitrary user input.

Structure of Objects

An object forms a statechart-like hierarchical structure with the possibility for both nested and parallel states. Each data component of the object is associated with some state in this structure. A state therefore provides a scope for data components and substates.

Each object belongs to a class of similar objects that determines the structure of the object. A mechanism for inheritance provides the possibility for subclassing. The language allows multiple inheritance, which has a natural interpretation in a specification language.

Global State and Assertions

The global state of execution is determined by relations and the local states of the objects. Assertions may be used for expressing desired invariance properties of the global state. The assertions in a specification are checked during animation , which provides for a crude form of state space exploration. This has proved to be very useful when a specification is being developed. Assertions may also be verifed using informal reasoning, or with a mechanical theorem prover.

Give feedback.