|
|
The DisCo Home Page |
       |
DisCo in a NutshellDisCo (Distributed Co-operation) is a formal specification method for reactive systems. It incorporates a specification language, a methodology for developing specifications using the language, and tool support for the methodology. Currently the support tools include an animation facility for executing specifications, a tool for visualizing execution histories as scenarios, and a link to a mechanical theorem prover for verification. The method has a solid formal basis but the specification language uses concepts and notations familiar to people with a conventional software engineering background. To get a taste of DisCo see the distributed sort and other examples. DisCo focuses on early verification and validation of behavioral properties. Emphasis is on collective behavior, rather than on behavior of individual objects. The joint action model of execution enables modeling of behavior at a high level of abstraction. In particular, collective behavior can be specified without fixing the interfaces of objects and without indicating which objects initiate communication.
Examples of DisCo specifications Animation Availability The Next Generation A Tutorial on DisCo92 The same tutorial on DisCo98 Funding Give feedback. |