|
|
The DisCo Home Page |
       |
Formal BasisThis page gives a short summary of the formal basis of the DisCo method. For a more detailed description see Reino Kurki-Suonio's current research interests. Joint ActionsThe logical foundation of DisCo is TLA, Temporal Logic of Actions. TLA may be used for reasoning about DisCo specifications. The incremental specification methodology using superposition guarantees preservation of safety properties by construction.The closed world approach adopted in DisCo means that we always model a system together with its environment.
Formal VerificationBecause of the formal basis of the DisCo specification language, temporal properties of DisCo specifications may be verified formally. Doing large proofs by hand is an error prone process, and therefore we provide support for mechanical reasoning.The compiler in the current implementation of the animation tool has been modified to produce theories in the logic of the PVS theorem prover. We can currently reason about invariance properties, but liveness properties could be treated as well. A simple example of verifications undertaken with the tool is:
Give feedback. |