The DisCo Home Page

Examples of DisCo Specifications

The following examples are in a roughly increasing order of complexity. Some of the examples have been formally verified, as indicated. Unfortunately some of the examples are written in DisCo92 and some in the DisCo, but at this level the differences should not be too great.

Distributed sort with termination detection (DisCo92). This example includes a Java applet that illustrates animation of DisCo specifications.
Distributed sort (DisCo98).
Taxi cabs.
Seat reservation system. This example illustrates how a distributed system is first specified using DisCo and then implemented with CORBA and C++.
Mobile robot case study. This case study illustrates how DisCo can be used to specify real-time control software.
Verifying a real-time DisCo specification using Kronos. This case study shows how to use an existing model-checking tool to verify finite instances of DisCo specifications.
Distributed water tanks. This example tries to extend DisCo to the direction of hybrid stochastic systems.

Give feedback.