«Syspect»

About the project

On this page:

 

go next top of page

1 Project

Syspect is a graphical development environment for a UML subset with a formal semantics according to the language CSP-OZ-DC. CSP-OZ-DC [1,2] combines the process algebra CSP [3] for the specification of communication and process behaviour, the method Object-Z [4], which describes data and operations, and Duration Calculus [5] 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.

By this means, Syspect offers a development enviroment, that unifies the whole process from the creation of a UML model with a formal semantics to the automatic verification by a model checker.

Syspect was initially developed by a one-year student group at the University of Oldenburg in collaboration with the research center AVACS.

 

go next top of page go back

2 References

  1. J. Hoenicke and E.-R. Olderog. CSP-OZ-DC: A combination of specification techniques for processes, data and time. Nordic Journal of Computing, 9(4):301-334, 2002.
  2. J. Hoenicke. Combination of Processes, Data, and Time. PhD thesis, University of Oldenburg, July 2006.
  3. C. A. R. Hoare. Communicating Sequential Processes http://www.usingcsp.com/cspbooks, 2004.
  4. Graeme Smith. The Object-Z Specification Language. Kluwer Academic Publisher, 2000.
  5. Zhou Chaochen, C.A.R. Hoare, and A.P. Ravn. A calculus of durations.IPL, 40(5):269-276, 1991.

 top of page go back