|
|
The DisCo Home Page |
       |
A Short Tutorial on DiscoThis tutorial explains what DisCo is and why it is useful. Table of Contents1. IntroductionDisCo (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 SystemsDisCo 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:
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 SystemsThe 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 SpecificationsThe 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 SpecificationsVerification 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 LanguageThe 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 LanguageA 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. The action system presented in the previous section could be written in DisCo as follows:
layer ActionSystem is
class Counter is
x: integer;
assert x >= 0;
end Counter;
action Increment (C: Counter) is
when true do
C.x := C.x + 1;
end Increment;
action Divide (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 ClassesActually, 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, real or truth values, or they can be sets or sequences of simple values. Objects can also include references to other objects. Enumerated types can be used to represent finite state machines. As with other object oriented languages, inheritance can be used for building more complex classes from simpler ones. A special case of inheritance is the extension of types. All record types can be extended to contain more fields. A simple example of a class definition is the following specification of class Device (comments begin with double hyphen):
layer L1 is
class Device is
data : integer;
state : (waiting, data_ready); -- State machine
end Device;
2.3 ActionsDisCo 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 (D: Device; i: integer) is
when D.state'waiting do
D.data := i;
D.state -> data_ready(); -- State transition
end read;
The action read illustrates a number of points about actions. An action consists of a name, a list of participants and parameters, 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 (D1, D2 : Device) is
when D1.state'data_ready and D2.state'data_ready and D1.data > D2.data do
D2.data := D1.data;
end propagate_max;
end L1;
2.4 Stepwise RefinementStepwise 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:
layer L2 is import L1;
extend Device by
next : reference 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 L2;
The guards and bodies of the original actions are referred to as "..." in the refinements. 2.5 More ConstructsRelations provide a mechanism to describe relationships among two or more objects. A constant relation cannot be altered by actions. As an example consider a total function defined as a relation. Relation total_function describes a relationship between a set of objects of class C_x and an object of class C_y:
relation total_function(C_x, C_y) is 0..infinity : 1;
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;
Furthermore, it is possible to define constants. As an example consider constant definition of type real given below:
constant K_P : real := 2.7;
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 using constants K_P, K_I and K_D:
function PID(e_n, s_n, e_n_1: real) : real is
return K_P*e_n + K_I*s_n + K_D*(e_n - e_n_1);
end PID;
2.6 Requiring FairnessIn 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 Development3.1 Where to use DisCoThe 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:
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:
3.2 Why to use DisCoIn 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:
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:
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 GlossaryWe 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 home page. Any comment on this tutorial is welcomed with pleasure. The most important terms together with their meanings are listed in the glossary below:
|
