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.
Furthermore, 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.
