DisCo Logo  

The DisCo Home Page


Main Page
Disco in a Nutshell
Formal Issues
Publications
Bugreporting
Members
Links


A Short Tutorial on DisCo (Disco92 version)


This tutorial explains what DisCo is and why it is useful.

Table of Contents

  1. Introduction
  2. The DisCo Language
  3. DisCo in Software Development
  4. Further Information and a Glossary

1. Introduction

DisCo (Distributed Co-operation) is a formal specification method for reactive systems developed at Tampere University of Technology, Finland. It incorporates a specification language, a methodology for developing specifications using the language, and tool support for the methodology.

DisCo is designed for software engineers rather than theoreticians, and thus the DisCo language resembles more a programming language than mathematical formulas. However, every DisCo specification has a precise interpretation in logic, which enables rigorous reasoning.

DisCo focuses on collective behavior, i.e., how objects co-operate. Specifications are developed incrementally. One starts with very simple behavior, and gradually adds details until the specification is at the desired level.

Developing a DisCo specification can be compared to carving a shape out of a block of wood. The original block of wood represents all the possible behaviors, and removing a piece of wood corresponds to a design step that disallows some of the behaviors. In early stages of the process we get a rough sketch, on which we gradually introduce more details.

At an abstract level, we may describe the behavior of the system using concepts that do not explicitly exist in the implementation level. We describe these abstractions using the DisCo language, which means that we can validate and reason about the precise behavior early in the development cycle.

1.1 Action Systems

DisCo is based on the joint action approach by Back and Kurki-Suonio. Joint actions enable us to concentrate on interaction between different components instead of the behavior of individual objects in isolation, thus raising the level of abstraction. Therefore, we can easily reason about high level behavioral properties even when implementation level interfaces have not been fixed yet.

An action system can be regarded as an abstract machine consisting of a set of state variables, and a set of actions, where each action consists of a guard and a body. The guard is a Boolean-valued expression involving state variables, and the body is a set of assignments to state variables. Actions transform one state to another, thus generating a sequence of states. A concrete example of an action system is given below:

    counter is a natural number
 
    when true do
         counter := counter + 1

    when even(counter) do
         counter := counter/2

This action system allows counter, which can be any natural number, to be incremented by one at any time, and to be divided by two when it is even.

The system starts in some initial state. As time passes, actions are executed, changing the system state accordingly. Actions are selected for execution nondeterministically, the only restriction being that the guard of an action must be true in order for the action to be executed. The execution of an action is atomic, meaning that once the execution of an action has been started, it cannot be interrupted or interfered by other actions. The computation model is interleaving, that is, only one action at a time is being executed.

The interleaving model is adopted, because it allows for simpler reasoning. However, it is not a model of execution, it is a model of observation. If two actions do not refer to the same variables at the implementation level, they may be executed in any order, or even simultaneously.

When we use an action system as a specification, we do not imply that the actual implementation should be an action system. We are only interested in the sequences of states that result from executing the system. Any mechanism that produces (in some sense) the same sequences of states suffices as an implementation. For instance, the programs below can be regarded as implementations of the action system above:

    program P1;                             program P2;
    var counter : integer;                  var counter : integer; 
    begin                                   begin
      counter := 0;                           counter := 10;
      while true do                           while true do
        begin                                   counter := counter + 1;
          counter := counter + 1;           end; 
          counter := counter + 1;
          counter := counter + 1;
          if counter mod 2 = 0 then
            counter := counter div 2;
        end;
    end;

The behavior of program P1 as a sequence of states is illustrated in the figure below:

Behavior of program P1 as a sequence of states

Whether P2 is a reasonable implementation of the action system depends entirely on what we interpret the action system to mean. For instance, we have not specified whether any particular action should eventually be executed or not, i.e., there are no fairness requirements. Therefore, even a process doing nothing would be a satisfying implementation.

If the specification of a system also includes actions or variables which belong to the environment of the system, the specification is said to describe a closed world. For example, a closed world specification of a lift which has a call button contains an action which pushes the button. Benefits of this approach compared to the open world approach include that the definition of interfaces between components can be postponed until the desired collective behaviors have been specified.

1.2 Reactive Systems

The simplest model of computation is a function from inputs to outputs. This model can be used when only the initial and final states of the system are important. When the responses of the system between the initial and final states are of interest, we call the system reactive. Reactive systems are systems that are in constant interaction with their environment. Examples include word processors, telephone exchanges, and process controllers.

The sequence of states describing the execution of a reactive system is potentially infinite. Properties of a system can be divided into safety and liveness properties. Informally, safety properties have the form "something bad never occurs" and liveness properties "something good will eventually occur." Example of the former is a property that some state variable is greater than zero in all states of the execution sequence. Then the "bad thing that should not occur" is a state where the variable is not greater than zero. Example of the latter is a property that a state variable is greater than zero in some state. In this case, the "bad thing" is an infinite sequence of states, in which the variable is less than or equal to zero in all states. Violation of a safety property can be pinpointed. Liveness properties can only be violated in infinity.

Reactive systems often have real-time constraints. The DisCo language can be used to specify real-time systems, but real time is beyond the scope of this tutorial.

1.3 Validation of Specifications

The validation of specifications is a substantial part of the DisCo method. In validation the specification is checked against its informal requirements. Informally, it answers the question whether we are building the right product.

DisCo has tool support for validation, enabling animated simulation of specifications. Animation makes specifications much more understandable and promotes communication between the people involved. The DisCo tool also supports graphical representation of execution scenarios (Message Sequence Charts).

Animated simulation has been found to be a good way to test specifications. It makes it easier to find situations where safety properties (assertions) are violated. Because the simulations are finite, due to obvious reasons, liveness properties can not be checked.

1.4 Verification of Specifications

Verification is the process of establishing that a specification has some desired properties. Informally, it answers the question whether we are building the product right. Verification can be done either by formal or informal means.

DisCo specifications can be verified formally using a theorem prover. Currently, there is a prototype tool to support mechanical verification of invariant properties using the PVS theorem prover.

2. The DisCo Language

The DisCo specification language gives a concrete syntax for using action systems for specification of reactive systems. The language includes features to aid in modularization and incremental specification. One of these features is object-orientation, i.e., the language has classes and objects. The systems are specified using the closed world principle, that is, they are modeled together with their assumed environments. We present here the main features of the language using examples.

2.1 Introduction to the Language

A DisCo specification consists of a set of layers, which are used for modularizing specifications. Classes and actions are collected into layers. The basic methods of building new layers are composition of two or more separate layers, and refinement of layers by superposition. Keyword system is used instead of layer in the syntax of DisCo92.

The action system presented in the previous section could be written in DisCo as follows:

system ActionSystem is               

    class Counter is
        x: integer;
        assert x >= 0;
    end Counter;

    action Increment by C: Counter is
    when true do
        C.x := C.x + 1;
    end Increment;

    action Divide by C: Counter is
    when (C.x mod 2 = 0) do
        C.x := C.x / 2;
    end Divide;

end ActionSystem;

Composition of layers allows for bottom-up design, where different parts of the system are first specified separately, and later combined to form a complete specification. A typical example of this is the combination of a layer specifying workstations and a layer specifying a bus, to give a new layer to specify a network of workstations.

Superposition is used for stepwise refinement, or top-down design of layers. By using superposition, one can add new state components and refine actions to handle them, or add new actions. An important application of superposition is to strengthen the guards of previously introduced actions by adding new conjuncts, thereby constraining the allowed behaviors. For example, we might first model a network of workstations by letting any station to send at any time. Later we could impose a ring discipline by allowing only the workstation that has the sending token to send.

The semantics of the specification language guarantees that safety properties are preserved in composition and superposition. Liveness properties, however, are not always preserved.

2.2 Classes and Actions

Actually, the above specification is more general than the previous one because it specifies a class of counters. The universe described by a DisCo specification consists of a set of objects, which are instances of classes. An object has a distinct identity, and it can participate in actions.

The attributes of an object can have simple values such as integer or truth values, or they can be sets or sequences of simple values. Objects can also include finite state machines and references to other objects. As with other object oriented languages, inheritance can be used for building more complex classes from simpler ones.

A simple example of a class definition is the following specification of class Device (comments begin with double hyphen):

system S1 is
    class Device is
        data : integer;
        state *waiting, data_ready;       -- State machine, asterisk
    end Device;                           -- denotes initial state

DisCo actions correspond to actions in an action system roughly in the same way as subroutines correspond to ordinary blocks of code in a programming language. A DisCo action is a template, which tells how the contents of the objects participating in the action are modified. For example, an action to assign a value to the data field of a device object could be written as follows:

    action read (i: integer) by D: Device is
    when D.waiting do
        D.data := i;
        -> D.data_ready;      -- State transition
    end read;

The action read illustrates a number of points about actions. An action consists of a name, parameters, participants, a guard, and a body.

In action read, there is one formal participant D of class Device. When an action is executed, the formal participants are replaced by the actual objects participating in the action. The body of the action then tells, how the attributes of the participants are changed. An object can not participate in an action as more than one participant.

The action has also one parameter i of type integer. When an action is executed, the values for parameters are chosen nondeterministically. A typical use for parameters is the one in this action, where we want to indicate that the data field is changed, but we do not yet want to fix the value that it will contain. In later refinements, constraints can be imposed on the values that data can contain.

An action can only be executed, if there exist participants and parameters so that the guard is true. The guard can refer both to the participants and parameters of the action. It is also possible to refer to the global state by using universal or existential quantification over classes.

The execution of an action means executing the statements given in its body. The body consists of assignments and conditional statements which can refer only to the participants and parameters of the action.

A DisCo specification does not specify how the participants communicate, e.g. whether message passing, shared memory, or some other means of communication is used. Only the effects of the communication and the involvement of the participants is specified. Action propagate_max shows an example of communication between objects:

    action propagate_max by D1, D2 : Device is
    when D1.data_ready and D2.data_ready and D1.data > D2.data do
        D2.data := D1.data;
    end propagate_max;
end S1;

2.3 Stepwise Refinement

Stepwise refinement is achieved by importing an existing layer into a new layer, and extending the classes and refining the actions of the imported layer, or by adding new classes and actions. The refinements are based on superposition, that is, the new properties are defined on top of the old properties. The language takes care that conflicting refinements are not possible.

Consider for example a simple extension of the class Device:

system S2 import S1; is
    extend Device by
        next : Device;         -- Reference to another Device object
    end Device;

The syntax of simple refinement of actions is illustrated by the following refinements of the actions read and propagate_max:

    refined read is
    when ... i > 0 do
        ...
    end read;

    refined propagate_max is
    when ... D1.next = D2 do
        ...
    end propagate_max;
end S2;

The guards and bodies of the original actions are referred to as "..." in the refinements.

2.4 More Constructs

An initial condition expresses a condition that should hold in the initial state, and an assertion expresses a condition that should hold invariantly, that is, in every state. They serve two purposes: on one hand they can be checked when simulating the system, and on the other hand they inform the reader of the specification about intended initial conditions and invariants of the system. Moreover, assertions can be verified formally.

As an example, the initial condition below says that in the initial state there should be at least three instances of the class Device:

    initially NumberOfDevices is (+/ D:Device ::1) >= 3;

Functions in DisCo provide a mechanism to abbreviate complex expressions. They cannot have any side effects. As an example consider the following function PID, which computes a value from three input values:

    function PID(e_n, s_n, e_n_1: integer) return integer is
        7*e_n + 3*s_n + 2*(e_n - e_n_1);
    end PID;

2.5 Requiring Fairness

In DisCo specifications there are no built-in liveness properties, that is, it cannot be assumed that any enabled action will ever be executed. Liveness properties are obtained by giving explicit fairness requirements.

Fairness requirements are stated in DisCo by prefixing a participant name by an asterisk in action definition. If such an action is infinitely often enabled so that the same object could participate as the same prefixed formal participant, then the action has to be executed infinitely often with this object as that formal participant.

If fairness is required for more than one participant, the fairness condition above is required for each combination of such participants.

3. DisCo in Software Development

3.1 Where to use DisCo

The figure below illustrates how DisCo can be used in software development. In the figure, waterfall model is assumed to be the model of life cycle, but in principle, any other model could be used:

DisCo in software life cycle

However, this figure does not reveal the whole truth. In practice, DisCo forces the specifier to be exact in the early phases of the life cycle when specifying at a high level of abstraction. Thus, it is likely that things are better understood and well-defined in later phases also. If we consider each step of the life cycle one at a time, the following list can be formed:

  • Requirements
    The starting point of a DisCo specification is a set of informal requirements, which form a basis for writing a DisCo specification. The DisCo tool, which enables animated simulation of specifications, can be used to validate the requirements. A DisCo specification may conflict with the informal requirements, and the requirements must be clarified. This is not extra work, since these conflicts need to be handled in any case. However, when using traditional methods, the conflicts can hide more easily, and they may not be detected until an implementation is made.
  • Specification
    The DisCo language can be used for representing the behavior of the system. Besides behavior, also data can be modeled. The specification can be composed of several pieces each of which refines the previous specification. Thus, there is a controlled and well-defined way to develop specifications one aspect at a time. Here, the key issue is to focus on a behavioral specification and omit implementation details. In addition to DisCo, also informal methods (e.g. UML) can be used especially for non-critical parts of the specification.
  • Design
    In the design phase, the DisCo specification is typically refined even further. However, now issues effecting the way the system should be implemented are given. For example, properties of the underlying software and hardware architecture can be introduced. Obviously, informal methods can be used, too.
  • Implementation
    A DisCo specification together with other documentation provides the basis for an implementation. This task is fairly straight-forward, if the design is made properly, and the work can be divided in a well-defined manner if the design contains decisions on program modules.
  • Testing
    An exact specification gives a solid base for testing. It has to be ensured that all parts of program code representing actions are executed. Also, invariants can be used, if they can be evaluated during the testing. A formal specification can also be used as an oracle to give answers to questions like "if this is the input, what should the output be?"
  • Maintenance
    A DisCo specification gives a good basis for maintenance of the system, because it documents the functionality of the system precisely. If new properties built during maintenance are added to the specification by using superposition, unmanageable inconsistencies can be avoided.

3.2 Why to use DisCo

In a perfect world, requirements would be a consistent description of the things that should be implemented. These requirements would never change, and it would be possible to implement them in a realistic manner and schedule.

In such case, the development of the system could be understood to proceed as in the V-model illustrated in figure below:

Traditional V-model

In the figure, arrows with white heads denote proceeding from one step to another. Arrows with black heads indicate input from earlier phase, for instance, module testing is done using the results obtained in the design phase. It is always possible to go backwards, which means that in one step an error that cannot be corrected was discovered.

In a perfect world, errors never happen, and all systems are developed correctly. However, in a real world, there are inconsistencies in the requirements, the clients are not sure what they want, and the developers and the clients speak in different terms. During development, critical errors may be discovered, and requirements may be misunderstood. Furthermore, requirements may not be implementable, or there may be ambiguity on what should be developed.

Therefore, in order to define the correct system, it is desirable to be able to animate and execute even the first specifications based on the requirements in order to ensure that the client is really satisfied with the specification. This obviously reduces the need to develop several prototypes of a system that would be used for finding out what errors (if any) have been made in the requirements phase.

In the design phase, the design can be formally proven to be a correct design based on the specification. In addition, similarly to the specification phase, the client can validate the behavior of the design by using the DisCo tool. This enhances the understanding the client has over the system being developed, increasing the probability of success even further.

Obviously, since we can detect behavioral errors already in the specification and design phase, the development cycle becomes more trustworthy. Everything that proceeds to the implementation phase is already validated to behave correctly. When these changes are added to the V-model, we get a triangle model, illustrated in figure below:

Triangle model obtained by using DisCo

As is obvious from earlier figure, when an error is discovered from the given requirements, the specification or the design, it may be as late as in acceptance testing in the traditional V-model. This means that the developers must jump back to the requirements phase and start all over again.

However, if DisCo is used, the triangle model enhances the communication between the client and the developers. Therefore, errors can be detected in each phase of the development, and acceptance testing can be only a step in which the client checks that he or she has got the system that was agreed on during the validation of the specification and the design. Obviously, whenever an error is discovered, we have to go back to the previous phase to see whether the error is also present there.

There is still a possibility to discover errors as late as the acceptance testing. But now there also is a way to test every step of the life cycle in order to check the result, thus increasing the probability that the correct system is being developed.

4. Further Information and a Glossary

We hope that this tutorial has answered your first questions on DisCo. We have also other material available for you, both theoretical and more practical, some of which can be found from our homepage. Any comment on this tutorial is welcomed with pleasure.

The most important terms together with their meanings are listed in the glossary below:

  • Action
    A syntactic unit of execution in DisCo, which consists of a name, parameters, participants, a guard, and a body. Actions are disjoint and atomic. An action can be executed when it is enabled. The execution of an action can only change the states of the participating objects. In a logical sense, an action is a relation between two adjacent states in an infinite sequence of states.
  • Animation
    Graphical visualization of a specification and its execution.
  • Atomicity
    The execution of an action is atomic, if once started it will also end, and no execution of another action can interfere with it. Even if in reality the actions are executed in parallel, we can still use an interleaved sequential model in reasoning because of atomicity.
  • Assertion
    An assertion expresses a condition that should always hold.
  • Behavior
    The way in which a system functions. In a logical sense, a behavior can be modeled as an infinite sequence of states.
  • Class
    A set of similar objects.
  • Closed world
    The principle employed by DisCo, meaning that a specification always describes a system together with its assumed environment.
  • Composition
    Composition of layers allows for bottom-up design, where different parts of the system are first specified separately, and later combined to form a complete specification.
  • Guard
    Every DisCo action has a boolean expression called the guard. If there exist participants and parameters so that the guard evaluates to true, the action is said to be enabled.
  • Importing
    A mechanism used to employ previously defined layers as bases for new layers.
  • Initial condition
    A requirement for the initial state.
  • Initial state
    The first state of a sequence of states.
  • Invariant
    A requirement which holds in every state. Assertions are used to express intended invariants.
  • Fairness
    Liveness properties are obtained by stating fairness requirements. In DisCo, fairness requirement indicates that it is not possible for an action to be enabled infinitely often without being executed infinitely often.
  • Function
    Functions provide a mechanism to abbreviate complex expressions. Their evaluation cannot have any side effects.
  • Layer
    Layers are used for modularizing specifications. A layer is a complete specification consisting of class and action definitions, initial conditions, assertions, functions etc.
  • Liveness property
    A property of a potentially infinite execution which is of the form "something good will eventually occur."
  • Object
    An instance of a class. An object is characterized by its identity, state and capability to participate in actions.
  • Participant
    Execution of an action needs object(s) to participate in it. The number of participants and their classes are indicated in the action definition.
  • Reactive System
    Reactive system is a system that is in constant interaction with its environment.
  • Real Time
    Real-time systems are defined as those in which the correctness of the system depends not only on the logical results of computation, but also on the time at which the results are produced.
  • Safety property
    Property of an execution which is of the form "something bad never occurs."
  • Simulation
    DisCo specifications are executable which enables their animated simulation. Simulation can reveal errors and misconceptions in the early phases of the development, e.g. by checking assertions.
  • Specification
    A definition of a system at some level of abstraction. In DisCo, systems are specified as action systems.
  • State
    An execution of a system can be described as a sequence of states. The global state of a system is composed of local states of the objects, which are composed of the values of their attributes.
  • Superposition
    Superposition is used for stepwise refinement, or top-down design of layers. By superposition, one can add new state components and refine actions to handle them, or add new actions.
  • Validation
    The process of checking a specification against its informal requirements. Informally, answers the question whether we are building the right product.
  • Verification
    The process of establishing that a specification has some desired properties. If verification is done using formal means it is called formal verification. Formal verification requires the specification to be given in formal notation, such as DisCo language. Informally, answers the question whether we are building the product right.