Dr. Andreas Schäfer
On this page:
back to the mainpage.
1
Publications (BibTeX Source)
@ARTICLE{schaefer2008,
AUTHOR = {A. Sch\"afer},
TITLE = {{Beschreibung und Verifikation r\"aumlicher und zeitlicher Eigenschaften
mobiler Systeme}},
JOURNAL = {it -- Information Technology},
YEAR = {2008},
VOLUME = {50},
PAGES = {324-326},
NUMBER = {5},
DOI = {DOI 10.1524/itit.2008.0503},
URL = {http://csd.informatik.uni-oldenburg.de/pub/Papers/itti0805_324a.pdf},
NOTE = {\url{http://it-Information-Technology.de}{http://it-Information-Technology.de}},
ABSTRACT = {
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.}
}
@ARTICLE{sch07b,
AUTHOR = {A. Sch\"afer},
TITLE = {{PhD Abstract: Specification and Verification of Mobile Real-Time
Systems}},
EDITOR = {V. Sassone},
YEAR = {2007},
PAGES = {193-195},
PUBLISHER = {EATCS},
JOURNAL = {Bulletin of the EATCS},
VOLUME = {92},
URL = {http://csd.informatik.uni-oldenburg.de/pub/Papers/as07b.pdf}
}
@INPROCEEDINGS{sch07a,
AUTHOR = {A. Sch\"afer},
TITLE = {{Spezifikation und Verifikation mobiler Realzeitsysteme}},
BOOKTITLE = {{Ausgezeichnete Informatikdissertationen 2007}},
EDITOR = {D. Wagner},
YEAR = {2007},
PAGES = {169-177},
SERIES = {GI-Edition-Lecture Notes in Informatics (LNI)},
PUBLISHER = {Gesellschaft f\"ur Informatik},
URL = {http://csd.informatik.uni-oldenburg.de/pub/Papers/as07a.pdf}
}
@ARTICLE{schaefer07,
AUTHOR = {A. Sch\"afer},
TITLE = {Axiomatisation and Decidability of Multi-Dimensional Duration
Calculus},
JOURNAL = {TIME'05 special issue of Information and Computation},
YEAR = {2007},
VOLUME = {205},
NUMBER = {1},
NOTE = {DOI
\url{http://dx.doi.org/10.1016/j.ic.2006.08.005}{10.1016/j.ic.2006.08.005}
},
ABSTRACT = {
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.
}
}
@INPROCEEDINGS{QS06,
AUTHOR = {J.-D. Quesel and A. Sch\"afer},
TITLE = {Spatio-Temporal Model Checking for Mobile Real-Time Systems},
BOOKTITLE = {3rd International Colloquium on Theoretical Aspects
of Computing, ICTAC},
YEAR = {2006},
EDITOR = {K. Barkaoui and A. Cavalcanti and A. Cerone},
SERIES = {LNCS},
PAGES = {347--361},
ABSTRACT = {
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.
}
}
@INPROCEEDINGS{BS05,
AUTHOR = {R. Boute and A. Sch\"afer},
TITLE = {The Timer Cascade: Functional Modelling and Real Time Calculi},
BOOKTITLE = {Theoretical Aspects of Computing, ICTAC 2005},
PAGES = {242 - 256},
YEAR = {2005},
EDITOR = {D.V. Hung and M. Wirsing},
VOLUME = {3722},
SERIES = {LNCS},
PUBLISHER = {Springer},
URL = {http://csd.Informatik.Uni-Oldenburg.DE/~skript/pub/Papers/bs05.pdf},
NOTE = {This publication is available at
\url{
http://www.springerlink.com/openurl.asp?genre=article&id=doi:10.1007/11560647_16
}
{SpringerLink}
},
ABSTRACT = {
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.
}
}
@INPROCEEDINGS{sch05b,
AUTHOR = {A. Sch\"afer},
TITLE = {{Axiomatisation and Decidability of Multi-Dimensional Duration
Calculus}},
BOOKTITLE = {Proceedings of the 12th International Symposium on Temporal
Representation and Reasoning, {TIME} 2005},
PAGES = {122-130},
MONTH = {June},
YEAR = {2005},
EDITOR = {J. Chomicki and D. Toman},
VOLUME = {},
SERIES = {},
URL = {http://csd.Informatik.Uni-Oldenburg.DE/pub/Papers/as05.pdf},
PUBLISHER = {IEEE Computer Society},
NOTE = {This publication is available at
\url{http://doi.ieeecomputersociety.org/10.1109/TIME.2005.15}
{IEEE Digital Library}
},
ABSTRACT = {
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.
}
}
@INPROCEEDINGS{sch05,
AUTHOR = {A. Sch\"afer},
TITLE = {A calculus for shapes in time and space},
BOOKTITLE = {Theoretical Aspects of Computing, ICTAC 2004},
PAGES = {463-478},
YEAR = {2005},
EDITOR = {Z. Liu and K. Araki},
VOLUME = {3407},
SERIES = {LNCS},
URL = {http://csd.Informatik.Uni-Oldenburg.DE/pub/Papers/as05a.pdf},
PUBLISHER = {Springer},
NOTE = {This publication is available at
\url{
http://springerlink.metapress.com/openurl.asp?genre=article&issn=0302-9743&volum
e=3407&spage=463}
{SpringerLink}
},
ABSTRACT = {
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.
}
}
@INPROCEEDINGS{sch03,
AUTHOR = {A. Sch\"afer},
TITLE = {Combining Real-Time Model-Checking and Fault Tree Analysis},
BOOKTITLE = {FM 2003: the 12th International FME Symposium },
YEAR = {2003},
EDITOR = {D. Mandrioli and K. Araki and S. Gnesi},
VOLUME = {2805},
SERIES = {LNCS},
PAGES = {522-541},
PUBLISHER = {Springer},
URL = {http://csd.Informatik.Uni-Oldenburg.DE/pub/Papers/as03.pdf},
NOTE = {This publication is available at
\url{
http://www.springerlink.com/openurl.asp?genre=article&issn=0302-9743&volume=2805
&spage=522}
{SpringerLink}
},
ABSTRACT = {
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.
}
}
