«Syspect»

Publications (Abstracts)

On this page:

 

go next top of page

1 Publications (Abstracts)

[FLOQ11]
Johannes Faber, Sven Linker, Ernst-Rdiger Olderog, and Jan-David Quesel. Syspect - modelling, specifying, and verifying real-time systems with rich data. International Journal of Software and Informatics, 5(1-2):117-137, 2011. ISSN 1673-7288.
[ bib | http ]

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.

[FIJSS10]
Johannes Faber, Carsten Ihlemann, Swen Jacobs, and Viorica Sofronie-Stokkermans. Automatic verification of parametric specifications with complex topologies. Reports of SFB/TR 14 AVACS 66, SFB/TR 14 AVACS, 2010. ISSN: 1860-9821, http://www.avacs.org.
[ bib | .pdf ]

The focus of this paper is on reducing the complexity in verification by exploiting modularity at various levels: in specification, in verification, and structurally. For specifications, we use the modular language CSP-OZ-DC, which allows us to decouple verification tasks concerning data from those concerning durations. At the verification level, we exploit modularity in theorem proving for rich data structures and use this for invariant checking. At the structural level, we analyze possibilities for modular verification of systems consisting of various components which interact. We illustrate these ideas by automatically verifying safety properties of a case study from the European Train Control System standard, which extends previous examples by comprising a complex track topology with lists of track segments and trains with different routes.

[MORW08]
M. Mller, E.-R. Olderog, H. Rasch, and H. Wehrheim. Integrating a formal method into a software engineering process with UML and Java. Formal Apsects of Computing, 20:161-204, 2008.
[ bib ]

We describe how CSP-OZ, a formal method combining the process algebra CSP with the specification language Object-Z, can be integrated into an object-oriented software engineering process employing the UML as a modelling and Java as an implementation language. The benefit of this integration lies in the rigour of the formal method, which improves the precision of the constructed models and opens up the possibility of (1) verifying properties of models in the early design phases, and (2) checking adherence of implementations to models. The envisaged application area of our approach is the design of distributed reactive systems. To this end, we propose a specific UML profile for reactive systems. The profile contains facilities for modelling components, their interfaces and interconnections via synchronous/broadcast communication, and the overall architecture of a system. The integration with the formal method proceeds by generating a significant part of the CSP-OZ specification from the initially developed UML model. The formal specification is on the one hand the starting point for verifying properties of the model, for instance by using the FDR model checker. On the other hand, it is the basis for generating contracts for the final implementation. Contracts are written in the Java Modeling Language (JML) complemented by , an assertion language for specifying orderings between method invocations. A set of tools for runtime checking can be used to supervise the adherence of the final Java implementation to the generated contracts.

[MFHR08]
R. Meyer, J. Faber, J. Hoenicke, and A. Rybalchenko. Model checking duration calculus: A practical approach. Formal Aspects of Computing, 20(4-5):481-505, July 2008. ISSN 0934-5043 (Print) 1433-299X (Online).
[ bib | .pdf ]

Model checking of real-time systems against Duration Calculus (DC) specifications requires the translation of DC formulae into automata-based semantics. The existing algorithms provide a limited DC coverage and do not support compositional verification. We propose a translation algorithm that advances the applicability of model checking tools to realistic applications. Our algorithm significantly extends the subset of DC that can be checked automatically. The central part of the algorithm is the automatic decomposition of DC specifications into sub-properties that can be verified independently. The decomposition is based on a novel distributive law for DC. We implemented the algorithm in a tool chain for the automated verification of systems comprising data, communication, and real-time aspects. We applied the tool chain to verify safety properties in an industrial case study from the European Train Control System (ETCS).

Keywords: Model checking, Verification, Duration Calculus, Timed automata, Real-time systems, European Train Control System, Case study

 top of page go back