Syspect is a free and open source, graphical development environment for a UML subset with a formal semantics according to the language CSP-OZ-DC.

CSP-OZ-DC combines the process algebra CSP for the specification of communication and process behaviour, the method Object-Z, which describes data and operations, and Duration Calculus to characterise time-based requirements. Syspect allows the user to design Component- ,Class- and Statediagrams.

Problems occurring during an export will be identified and visually marked. For the formalisation of data the tool offers different input possibilities, like a graphical input for the specification-language Z.

The tool comprises an editor for Duration Calculus formulae. Syspect supports saving of models in XMI as well as its own data format. In addition to a graphical export for the common image types, the development enviroment Syspect supports a LaTeX export for a convenient presentation of a specification.

Syspect offers a translation of the specification into Phase Event Automata. These can be read by model checking tools to verifiy (safety-)properties of the specification.

Currently, a automated connection to the model checker ARMC is available: the Syspect model can automatically be verified against Duration Calculus formulae. If ARMC detects an error and returns a counter example Syspect visualises this counter example in a user-friendly way.