Dr. Andreas Schäfer

 

1 Publications (with abstracts)

[Sch08]

A. Schäfer. Beschreibung und Verifikation räumlicher und zeitlicher Eigenschaften mobiler Systeme. it - Information Technology, 50(5):324-326, 2008. http://it-Information-Technology.de.
[ bib | .pdf ]

This paper provides an overview over a formal method for the analysis of mobile real-time systems. Control systems for cars and trains as well as mobile robots are examples of such systems. We develop a spatio-temporal logic that is used to model both the systems and safety requirements. We investigate the theoretical foundations like decidability and axiomatisability and develop a prototype tool for the automatic verification based on these results. The application of this logic is exemplified with an industrial case study.

[Sch07b]

A. Schäfer. PhD Abstract: Specification and Verification of Mobile Real-Time Systems. Bulletin of the EATCS, 92:193-195, 2007.
[ bib | .pdf ]

[Sch07c]

A. Schäfer. Spezifikation und Verifikation mobiler Realzeitsysteme. In D. Wagner, editor, Ausgezeichnete Informatikdissertationen 2007, GI-Edition-Lecture Notes in Informatics (LNI), pages 169-177. Gesellschaft für Informatik, 2007.
[ bib | .pdf ]

[Sch07a]

A. Schäfer. Axiomatisation and decidability of multi-dimensional duration calculus. TIME'05 special issue of Information and Computation, 205(1), 2007. DOI 10.1016/j.ic.2006.08.005.
[ bib ]

The Shape Calculus is a spatio-temporal logic based on an n-dimensional Duration Calculus tailored for the specification and verification of mobile real-time systems. After showing non-axiomatisability, we give a complete embedding in n-dimensional interval temporal logic and present two different decidable subsets, which are important for tool support and practical use.

[QS06]

J.-D. Quesel and A. Schäfer. Spatio-temporal model checking for mobile real-time systems. In K. Barkaoui, A. Cavalcanti, and A. Cerone, editors, 3rd International Colloquium on Theoretical Aspects of Computing, ICTAC, LNCS, pages 347-361, 2006.
[ bib ]

This paper presents an automatic verification method for combined temporal and spatial properties of mobile real-time systems. To this end, we provide a translation of the Shape Calculus (SC), a spatio-temporal extension of Duration Calculus, into weak second order logic of one successor (WS1S). A prototypical implementation facilitates successful verification of spatio-temporal properties by translating SC specifications into the syntax of the WS1S checker MONA. For demonstrating the formalism and tool usage, we apply it to the benchmark case study ``generalised railroad crossing'' (GRC) enriched by requirements inexpressible in non-spatial formalisms.

[BS05]

R. Boute and A. Schäfer. The timer cascade: Functional modelling and real time calculi. In D.V. Hung and M. Wirsing, editors, Theoretical Aspects of Computing, ICTAC 2005, volume 3722 of LNCS, pages 242 - 256. Springer, 2005. This publication is available at SpringerLink.
[ bib | .pdf ]

Case studies can significantly contribute towards improving the understanding of formalisms and thereby to their applicability in practice. One such case, namely a cascade of the familiar 24-hour timers (in suitably generalized form) provides interesting gedanken experiments and illustrations for presenting, illustrating and comparing various formalisms for modelling real-time behaviour of systems. The timer cascade is first modelled in a general-purpose functional formalism (Funmath) and various properties are derived, including an interesting algebraic monoid structure of timer programs. Then it is described and analyzed in duration calculus, thereby highlighting, similarities and differences in the approach to modelling and reasoning, and also the link between the formalisms. Future work consists in using this case as a running example for exploring the same issues for other formalisms intended for real time and hybrid systems. The underlying idea is that other authors join this effort and contribute towards extending it, finally arriving at a broad comparative survey of such formalisms.

[Sch05a]

A. Schäfer. Axiomatisation and Decidability of Multi-Dimensional Duration Calculus. In J. Chomicki and D. Toman, editors, Proceedings of the 12th International Symposium on Temporal Representation and Reasoning, TIME 2005, pages 122-130. IEEE Computer Society, June 2005. This publication is available at IEEE Digital Library.
[ bib | .pdf ]

We investigate properties of a spatio-temporal logic based on an n-dimensional Duration Calculus tailored for the specification and verification of mobile real-time systems. After showing non-axiomatisability, we give a complete embedding in n-dimensional interval temporal logic and present two different decidable subsets, which are important for tool support and practical use.

[Sch05b]

A. Schäfer. A calculus for shapes in time and space. In Z. Liu and K. Araki, editors, Theoretical Aspects of Computing, ICTAC 2004, volume 3407 of LNCS, pages 463-478. Springer, 2005. This publication is available at SpringerLink.
[ bib | .pdf ]

We present a spatial and temporal logic based on Duration Calculus for the specification and verification of mobile real-time systems. We demonstrate the use of the formalism and apply it to a case study. We extend a pure Duration Calculus specification for the controller by spatial assumptions to reason about spatial system properties. We prove that the formalism is undecidable in general for discrete and continuous domains and present a decidable fragment.

[Sch03]

A. Schäfer. Combining real-time model-checking and fault tree analysis. In D. Mandrioli, K. Araki, and S. Gnesi, editors, FM 2003: the 12th International FME Symposium, volume 2805 of LNCS, pages 522-541. Springer, 2003. This publication is available at SpringerLink.
[ bib | .pdf ]

We present a semantics for fault tree analysis, a technique used for the analysis of safety critical systems, in the real-time interval logic Duration Calculus with Liveness and show how properties of fault trees can be checked automatically. We apply this technique in two examples and show how it can be connected to other verification techniques.