Home > Research > Publications & Outputs > Syspect

Research

Associated organisational unit

Links

View graph of relations

Syspect: Modelling, specifying, and verifying real-time systems with rich data.

Research output: Contribution to Journal/Magazine › Journal article › peer-review

Published

Standard

Syspect: Modelling, specifying, and verifying real-time systems with rich data. / Faber, Johannes; Linker, Sven; Quesel, Jan-David et al.
In: International Journal of Software and Informatics, Vol. 5, No. 1-2, 2011, p. 117-137.

Research output: Contribution to Journal/Magazine › Journal article › peer-review

Harvard

Faber, J, Linker, S, Quesel, J-D & Olderog, E-R 2011, 'Syspect: Modelling, specifying, and verifying real-time systems with rich data.', International Journal of Software and Informatics, vol. 5, no. 1-2, pp. 117-137. <http://www.ijsi.org/ijsi/article/abstract/i78>

APA

Faber, J., Linker, S., Quesel, J-D., & Olderog, E-R. (2011). Syspect: Modelling, specifying, and verifying real-time systems with rich data. International Journal of Software and Informatics, 5(1-2), 117-137. http://www.ijsi.org/ijsi/article/abstract/i78

Vancouver

Faber J, Linker S, Quesel J-D, Olderog E-R. Syspect: Modelling, specifying, and verifying real-time systems with rich data. International Journal of Software and Informatics. 2011;5(1-2):117-137.

Author

Faber, Johannes ; Linker, Sven ; Quesel, Jan-David et al. / Syspect : Modelling, specifying, and verifying real-time systems with rich data. In: International Journal of Software and Informatics. 2011 ; Vol. 5, No. 1-2. pp. 117-137.

Bibtex

@article{e58bdce5c1c047439ba7997f6ba11786,
title = "Syspect: Modelling, specifying, and verifying real-time systems with rich data.",
abstract = "We introduce the graphical tool Syspect for modelling, specifying, and automatically verifying reactive systems with continuous real-time constraints and complex, possibly infinite data. For modelling these systems, a UML profile comprising component diagrams, protocol state machines, and class diagrams is used; for specifying the formal semantics of these models, the combination CSP-OZ-DC of CSP (Communicating Sequential Processes), OZ (Object-Z) and DC (Duration Calculus) is employed; for verifying properties of these specifications, translators are provided to the input formats of the model checkers ARMC (Abstraction Refinement Model Checker) and SLAB (Slicing Abstraction model checker) as well as the tool H-PILoT (Hierarchical Proving by Instantiation in Local Theory extensions). The application of the tool is illustrated by a selection of examples that have been successfully analysed with Syspect",
author = "Johannes Faber and Sven Linker and Jan-David Quesel and Ernst-R{\"u}diger Olderog",
year = "2011",
language = "English",
volume = "5",
pages = "117--137",
journal = "International Journal of Software and Informatics",
issn = "1673-7288",
number = "1-2",

}

RIS

TY - JOUR

T1 - Syspect

T2 - Modelling, specifying, and verifying real-time systems with rich data.

AU - Faber, Johannes

AU - Linker, Sven

AU - Quesel, Jan-David

AU - Olderog, Ernst-Rüdiger

PY - 2011

Y1 - 2011

N2 - We introduce the graphical tool Syspect for modelling, specifying, and automatically verifying reactive systems with continuous real-time constraints and complex, possibly infinite data. For modelling these systems, a UML profile comprising component diagrams, protocol state machines, and class diagrams is used; for specifying the formal semantics of these models, the combination CSP-OZ-DC of CSP (Communicating Sequential Processes), OZ (Object-Z) and DC (Duration Calculus) is employed; for verifying properties of these specifications, translators are provided to the input formats of the model checkers ARMC (Abstraction Refinement Model Checker) and SLAB (Slicing Abstraction model checker) as well as the tool H-PILoT (Hierarchical Proving by Instantiation in Local Theory extensions). The application of the tool is illustrated by a selection of examples that have been successfully analysed with Syspect

AB - We introduce the graphical tool Syspect for modelling, specifying, and automatically verifying reactive systems with continuous real-time constraints and complex, possibly infinite data. For modelling these systems, a UML profile comprising component diagrams, protocol state machines, and class diagrams is used; for specifying the formal semantics of these models, the combination CSP-OZ-DC of CSP (Communicating Sequential Processes), OZ (Object-Z) and DC (Duration Calculus) is employed; for verifying properties of these specifications, translators are provided to the input formats of the model checkers ARMC (Abstraction Refinement Model Checker) and SLAB (Slicing Abstraction model checker) as well as the tool H-PILoT (Hierarchical Proving by Instantiation in Local Theory extensions). The application of the tool is illustrated by a selection of examples that have been successfully analysed with Syspect

M3 - Journal article

VL - 5

SP - 117

EP - 137

JO - International Journal of Software and Informatics

JF - International Journal of Software and Informatics

SN - 1673-7288

IS - 1-2

ER -