|
|
The DisCo Home Page |
       |
MethodologyDeveloping a specification in DisCo is an incremental process. One starts with very simple behavior, and gradually adds details until the specification is at the desired level. Development focuses on collective behavior, that is, how objects co-operate. 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, in which details are then gradually added. DisCo employs the closed world principle, meaning that a DisCo specification always describes a system together with its environment. The model of the environment may be highly nondeterministic, however.
SuperpositionA DisCo specification is built of layers, which introduce new details about the system. Each new layer is superimposed on the existing layers, and the end result contains everything in the layers. Nothing is ever removed. The use of superposition guarantees preservation of safety properties by construction.Nondeterminism plays a central role. Whenever we introduce a new state component (variable), we must describe all the possible ways its value may be changed. In later design steps it is not possible to allow changes that were not allowed in the step that introduced the variable. It is, however, possible to allow arbitrary changes, and later add restrictions that disallow some of them.
Joint ActionsDisCo is based on the joint action approach of Back and Kurki-Suonio. A joint action system consists of a set of objects, and a set of actions. Whenever the guard of an action is true for some combination of participating objects, the action can be executed for them. The body of an action gives the state changes that take place when the action is executed.The execution of an action is atomic, and actions take place in a sequential order. Parallelism is modeled by interleaving, that is, allowing independent activities to occur in any order. The meaning of a DisCo specification is the set of execution sequences it allows. The execution model does not distinguish between ``active'' and ``passive'' objects. We are only interested in what information is exchanged between the participants, not who initiates such exchange.
AbstractionsLike all modern specification methods, DisCo encourages the use of abstractions. 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 already at the abstract level.The use of superposition means that the high level abstractions are a part of the final detailed specification. We can, however, justify not implementing some variables explicitly if we can establish how their values may be computed from other variables. Such "ghost" or "shadow" variables may then be omitted from an implementation. Similarly, actions that only assign to shadow variables may be omitted. Refining the atomicity of actions is an important application of the shadow concept. The behavior of distributed systems is often best understood with synchronous intuition. We can make the intuition explicit as an action that modifies two objects simultaneously, and later show that the same effects can be achieved with asynchronous communication between the objects. Verifying that abstractions are implemented correctly incurs proof obligations, which may be verified informally or formally. Give feedback. |