Prof. Dr. Ernst-Rüdiger Olderog
On this page:
back to the mainpage.
1
Publications (BibTeX Source)
@BOOK{OD08,
AUTHOR = {E.-R. Olderog and H. Dierks},
TITLE = {Real-Time Systems --- Formal Specification and Automatic
Verification},
PUBLISHER = {Cambridge University Press},
YEAR = 2008,
NOTE = {ISBN 978-0-521-88333-7. For more information see: \url{http://csd.informatik.uni-oldenburg.de/rt-book/}{http://csd.informatik.uni-oldenburg.de/rt-book/}}
}
@ARTICLE{AVACS07,
AUTHOR = {B. Becker and A. Podelski and W. Damm and M. Fr{\"a}nzle and
E.-R. Olderog and R. Wilhelm},
TITLE = {{SFB/TR 14 AVACS -- Automatic Verification and Analysis of
Complex Systems}},
JOURNAL = {it -- Information Technology},
PUBLISHER = {Oldenbourg},
YEAR = {2007},
NUMBER = {2},
VOLUME = {49},
PAGES = {118--126},
NOTE = {See also \url{http://www.avacs.org}{http://www.avacs.org}}
}
@ARTICLE{MORW07,
AUTHOR = {M. M\"oller and E.-R. Olderog and H. Rasch and H. Wehrheim},
TITLE = {Integrating a Formal Method into a Software Engineering Process with
{UML} and {Java}},
JOURNAL = {Formal Apsects of Computing},
YEAR = {2007},
VOLUME = {},
NUMBER = {},
NOTE = {To appear.},
ABSTRACT = {
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 {\em reactive systems}. To this end, we propose a
specific UML {\em 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 {\em verifying} properties of the model,
for instance by using the FDR model checker.
On the other hand, it is the basis
for generating {\em contracts} for the final implementation.
Contracts are written in the Java Modeling Language (JML) complemented
by \CSPjassda{}, 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.
}
}
@INPROCEEDINGS{DammMOOPPSW07,
AUTHOR = {Werner Damm and Alfred Mikschl and Jens Oehlerking and
Ernst-R{\"u}diger Olderog and Jun Pang and Andr{\'e} Platzer and Marc
Segelken and Boris Wirtz},
TITLE = {Automating Verification of Cooperation, Control, and Design in
Traffic Applications.},
YEAR = {2007},
PAGES = {115--169},
EDITOR = {Cliff Jones and Zhiming Liu and Jim Woodcock},
BOOKTITLE = {Formal Methods and Hybrid Real-Time Systems},
PUBLISHER = {Springer-Verlag},
SERIES = {LNCS},
VOLUME = {4700},
DOI = {10.1007/978-3-540-75221-9_6},
ISSN = {},
KEYWORDS = {},
ABSTRACT = {
We present a verification methodology for cooperating traffic
agents covering analysis of cooperation strategies, realization
of strategies through control, and implementation of control.
For each layer, we provide dedicated approaches to formal
verification of safety and stability properties of the design.
The range of employed verification techniques invoked to span
this verification space includes application of pre-verified
design patterns, automatic synthesis of Lyapunov functions,
constraint generation for parameterized designs, model-checking
in rich theories, and abstraction refinement. We illustrate
this approach with a variant of the European Train Control
System (ETCS), employing layer specific verification techniques
to layer specific views of an ETCS design.},
NOTE = {\url{http://dx.doi.org/10.1007/978-3-540-75221-9_6}{(c)
Springer-Verlag}}
}
@INPROCEEDINGS{BSO07,
AUTHOR = {D. Basin and E.-R. Olderog and P.E. Sevin\c{c}},
TITLE = {Specifying and analyzing security automata using {CSP-OZ}},
BOOKTITLE = {Proceedings of the 2007 ACM Symposium on Information, Computer
and Communications Security (ASIACCS 2007)},
PAGES = {70--81},
YEAR = 2007,
MONTH = {March},
PUBLISHER = {ACM Press},
LOCATION = {Singapore},
ABSTRACT = {
Security automata are a variant of B\"uchi automata used to specify
security policies that can be enforced by monitoring system execution.
In this paper, we propose using CSP-OZ, a specification language
combining Communicating Sequential Processes (CSP) and Object-Z (OZ), to
specify security automata, formalize their combination with target
systems, and analyze the security of the resulting system
specifications. We provide theoretical results relating CSP-OZ
specifications and security automata and show how
refinement can be used to reason about specifications of security
automata and their combination with target systems. Through a case
study, we provide evidence for the practical usefulness of this approach.
This includes the ability to specify concisely complex operations and
complex control, support for structured specifications, refinement, and
transformational design, as well as automated, tool-supported analysis.
}
}
@INPROCEEDINGS{erobs06,
AUTHOR = {E.-R. Olderog and B. Steffen},
TITLE = {{F}ormale {S}emantik und {P}rogrammverifikation},
BOOKTITLE = {Informatik-Handbuch, 4. Auflage},
EDITOR = {P. Rechenberg and G. Pomberger},
YEAR = 2006,
PUBLISHER = {Hanser Verlag},
PAGES = {145--166}
}
@INPROCEEDINGS{SBO06,
AUTHOR = {P. E. Sevin\c{c} and D. Basin and E.-R. Olderog},
BOOKTITLE = {ETRICS 2006},
EDITOR = {G\"unter M\"uller},
MONTH = {June},
PAGES = {352--367},
PUBLISHER = {Springer-Verlag},
SERIES = {LNCS},
TITLE = {Controlling Access to Documents: A Formal Access Control Model},
VOLUME = 3995,
YEAR = 2006,
ABSTRACT = {
Current access-control systems for documents suffer from one or
more of the following limitations: they are coarse-grained,
limited to XML documents, ot unable to maintain control over
copies of documents once they are released by the system. We
present a formal model of a system that overcomes all of these
restrictions. It is very fine-grained, supporst a general class of
documents, and provides a foundation for usage control.
}
}
@ARTICLE{DHO06,
AUTHOR = {W. Damm and H. Hungar and E.-R. Olderog},
TITLE = {Verification of cooperating traffic agents},
JOURNAL = {International Journal of Control},
YEAR = {2006},
VOLUME = {79},
NUMBER = {5},
MONTH = {May},
PAGES = {395--421},
ABSTRACT = {
This paper exploits design patterns employed in coordinating
autonomous transport vehicles so as to ease the burden in
verifying cooperating hybrid systems. The presented verification
methodology is equally applicable for avionics applications (such
as TCAS, the Traffic Alert and Collision Avoidance System), train
applications (such as ETCS, the European Train Control System), or
automotive applications (such as platooning). We present a
verification rule explicating the essence of employed design
patters, guaranteeing global safety properties of the kind ``a
collision will never occur'', and whose premises can either be
established by off-line analysis of the worst-case behavior of the
involved traffic agents, or by purely local proofs, involving only
a single traffic agent. A companion paper will show how such local
proof obligations can be discharged automatically.
}
}
@ARTICLE{OW05,
AUTHOR = {E.-R. Olderog and H. Wehrheim},
TITLE = {{Specification and (property) inheritance in CSP-OZ}},
JOURNAL = {Science of Computer Programming},
YEAR = {2005},
VOLUME = {55},
PAGES = {227--257},
ABSTRACT = {
CSP-OZ [Fis97, Fis00] is a combination of Communicating Sequential
Processes (CSP) and Object-Z (OZ). It enables the specification of
systems having both a state-based and a behaviour-oriented view
using the object-oriented concepts of classes, instantiation and
inheritance. CSP-OZ has a process semantics in the failure
divergence model of CSP. In this paper we explain CSP-OZ and
investigate the notion of inheritance. Furthermore, we study the
issue of property inheritance among classes. We prove in a uniform
way that behavioural subtyping relations between classes
introduced in [Weh02] guarantee the inheritance of safety and
``liveness'' properties.
\emph{Key words}: CSP, Object-Z, failures divergence semantics,
inheritance, safety and ``liveness'' properties, model-checking,
FDR
\begin{thebibliography}
\bibitem{Fis97}
C.~Fischer.
\newblock {CSP-OZ}: A combination of {Object-Z} and {CSP}.
\newblock In H.~Bowman and J.~Derrick, editors, {\em Formal Methods for Open
Object-Based Distributed Systems (FMOODS'97)}, volume~2, pages 423--438.
Chapman \& Hall, 1997.
\bibitem{Fis00}
C.~Fischer.
\newblock {\em Combination and Implementation of Processes and Data: From
{CSP-OZ} to {Java}}.
\newblock PhD thesis, Bericht Nr. 2/2000, University of Oldenburg, April 2000.
\bibitem{Weh02}
H.~Wehrheim.
\newblock Behavioural subtyping in object-oriented specification formalisms.
\newblock University of Oldenburg, Habilitation Thesis, 2002.
\end{thebibliography}
}
}
@INPROCEEDINGS{DaHuOl04,
AUTHOR = {W. Damm and H. Hungar and E.-R. Olderog},
TITLE = {On the Verification of Cooperating Traffic Agents},
BOOKTITLE = {FMCO 2003: Formal Methods for Components and Objects},
YEAR = {2004},
EDITOR = {F.S. de Boer and M.M. Bonsangue and S. Graf and W.-P. de Roever},
VOLUME = {3188},
PAGES = {77--110},
SERIES = {LNCS},
ABSTRACT = {
This paper exploits design patterns employed in coordinating
autonomous transport vehicles so as to ease the burden in
verifying cooperating hybrid systems. The presented veri cation
methodology is equally applicable for avionics applications (such
as TCAS), train applications (such as ETCS), or automotive
applications (such as platooning). We present a veri cation rule
explicating the essence of employed design patters, guaranteeing
global safety properties of the kind ``a collision will never
occur'', and whose premises can either be established by o -line
analysis of the worst-case behavior of the involved tra c agents,
or by purely local proofs, involving only a single tra c agent. In
a companion paper we will show, how such local proof obligations
can be discharged automatically.
}
}
@INPROCEEDINGS{MORW04,
AUTHOR = {M. M\"oller and E.-R. Olderog and H. Rasch and H. Wehrheim},
TITLE = {{Linking CSP-OZ with UML and Java: A Case Study}},
EDITOR = {E. Boiten and J. Derrick and G. Smith},
BOOKTITLE = {Integrated Formal Methods},
SERIES = {Lecture Notes in Computer Science},
NUMBER = {2999},
PUBLISHER = {Springer-Verlag},
ISSN = {0302-9743},
PAGES = {267--286},
YEAR = {2004},
MONTH = {March},
ABSTRACT = {
We describe how CSP-OZ, an integrated formal method combining the
process algebra CSP with the specification language Object-Z, can
be linked to standard software engineering languages, viz.\ UML
and Java. Our aim is to generate a significant part of the CSP-OZ
specification from an initially developed UML model using a UML
profile for CSP-OZ, and afterwards transform the formal
specification into assertions written in the Java Modelling
Language JML complemented by CSP$_{jassda}$. The intermediate
CSP-OZ specification serves to verify correctness of the UML
model, and the assertions control at runtime the adherence of a
Java implementation to these formal requirements. We explain this
approach using the case study of a ``holonic manufacturing
system'' in which coordination of transportation and processing is
distributed among stores, machine tools and agents without central
control.
},
URL = {http://csd.informatik.uni-oldenburg.de/pub/Papers/morw04.pdf},
}
@INPROCEEDINGS{OlWe02,
AUTHOR = {E.-R. Olderog and H. Wehrheim},
TITLE = {{Specification and Inheritance in CSP-OZ}},
EDITOR = {F. de Boer and M. Bosangue and S. Graf and W.-P. de Roever},
BOOKTITLE = {Formal Methods for Components and Objects},
VOLUME = {2852},
SERIES = {LNCS},
PAGES = {361--379},
PUBLISHER = {Springer},
YEAR = {2003},
ABSTRACT = {
CSP-OZ [Fis97,Fis00] is a combination of Communicating Sequential
Processes (CSP) and Object-Z (OZ). It enables the specification
of systems having both a state-based and a behaviour-oriented view
using the object-oriented concepts of classes, instantiation and
inheritance. CSP-OZ has a process semantics in the failures
divergence model of CSP. In this paper we explain CSP-OZ and
investigate the notion of inheritance. Behavioural subtyping
relations between classes introduced in [Weh02] guarantee the
inheritance of safety and ``liveness'' properties.
\begin{thebibliography}
\bibitem{Fis97}
C.~Fischer.
\newblock {CSP-OZ}: A combination of {Object-Z} and {CSP}.
\newblock In H.~Bowman and J.~Derrick, editors, {\em Formal Methods for Open
Object-Based Distributed Systems (FMOODS'97)}, volume~2, pages 423--438.
Chapman \& Hall, 1997.
\bibitem{Fis00}
C.~Fischer.
\newblock {\em Combination and Implementation of Processes and Data: From
{CSP-OZ} to {Java}}.
\newblock PhD thesis, Bericht Nr. 2/2000, University of Oldenburg, April 2000.
\bibitem{Weh02}
H.~Wehrheim.
\newblock Behavioural subtyping in object-oriented specification formalisms.
\newblock University of Oldenburg, Habilitation Thesis, 2002.
\end{thebibliography}
}
}
@ARTICLE{OD03,
AUTHOR = {E.-R. Olderog and H. Dierks},
TITLE = {{Moby/RT: A Tool for Specification and Verification of
Real-Time Systems}},
JOURNAL = {Journal of Universal Computer Science},
YEAR = {2003},
VOLUME = {9},
PAGES = {88--105},
ABSTRACT = {
The tool Moby/RT supports the design of real-time systems at the
levels of requirements, design specifications and programs.
Requirements are expressed by constraint diagrams [Kle00], design
specifications by PLC-Automata [Die00], and programs by Structured
Text, a programming language dedicated for programmable logic
controllers (PLCs), or by programs for LEGO Mindstorm robots. In
this paper we outline the theoretical background of Moby-RT by
discussing its semantic basis and its use for automatic
verification by utilising the model-checker UPPAAL.
\begin{thebibliography}
\bibitem{Kle00}
Kleuker, C. (2000).
\newblock {\em {Constraint Diagrams}}.
\newblock PhD thesis, University of Oldenburg.
\bibitem[Dierks, 2000]{Die00}
Dierks, H. (2000).
\newblock {PLC-Automata: A New Class of Implementable Real-Time Automata}.
\newblock {\em TCS}, 253(1):61--93.
\end{thebibliography}
}
}
@ARTICLE{DO03,
AUTHOR = {H. Dierks and E.-R. Olderog},
TITLE = {{Temporale Spezifikationslogiken}},
JOURNAL = {at-Automatisierungstechnik},
YEAR = {2003},
VOLUME = {51},
NUMBER = {2},
PAGES = {A1--A4},
ABSTRACT = {
Logiken sind in der Informatik ein weitverbreitetes Mittel zur
Spezifikation. Dazu werden Logiken verschiedener Auspr{\"a}gung
benutzt, z.B. temporale Logiken f{\"u}r reaktive Systeme, zu
denen die Systeme der Automatisierungstechnik z{\"a}hlen. Dieser
Beitrag enth{\"a}lt eine Einf{\"u}hrung in die wichtigsten
temporalen Logiken und Literaturverweise.
\textbf{English}\\
Logics are often used in computer science as specification
languages. There is a rich variety of logics to choose from
depending on the problem. Systems in automation technology are
typically reactive systems for which temporal logics are
adequate. We introduce the most important temporal logics and
give reference for further reading.
}
}
@ARTICLE{HO02b,
AUTHOR = {J. Hoenicke and E.-R. Olderog},
TITLE = {{CSP-OZ-DC}: A Combination of Specification Techniques for
Processes,
Data and Time},
JOURNAL = {Nordic Journal of Computing},
YEAR = {2002},
VOLUME = {9},
NUMBER = {4},
PAGES = {301--334},
NOTE = {appeared March 2003},
ABSTRACT = {
CSP-OZ-DC is a new combination of three well researched formal
techniques for the specification of processes, data and time: CSP
[Hoa85], Object-Z [Smi00], and Duration Calculus [ZHR91]. This
combination is illustrated by specifying the train controller of a
case study on radio controlled railway crossings. The technical
contribution of the paper is a smooth integration of the
underlying semantic models and its use for verifying timing
properties of CSP-OZ-DC specifications. This is done by combining
the model-checkers FDR [Ros94] for CSP and UPPAAL [BLL97] for
timed automata with a new tool \emph{f2u} that transforms FDR
transition systems and certain patterns of Duration Calculus
formulae into timed automata. This approach is illustrated by the
example of a vending machine.
\begin{thebibliography}
\bibitem{BLL97}
J.~Bengtsson, K.G. Larsen, F.~Larsson, P.~Pettersson, and Wang Yi.
\newblock Uppaal -- a tool suite for automatic verification of real-time
systems.
\newblock In R.~Alur, T.A. Henzinger, and E.D. Sonntag, editors, {\em Hybrid
Systems III -- Verification and Control}, volume 1066 of {\em LNCS}, pages
232--243. Springer, 1997.
\bibitem{Hoa85}
C.A.R. Hoare.
\newblock {\em Communicating Sequential Processes}.
\newblock Prentice Hall, 1985.
\bibitem{Ros94}
A.W. Roscoe.
\newblock Model-checking {CSP}.
\newblock In A.W. Roscoe, editor, {\em A Classical Mind --- Essays in Honour of
C.A.R.Hoare}, pages 353--378. Prentice-Hall, 1994.
\bibitem{Smi00}
G.~Smith.
\newblock {\em The Object-Z Specification Language}.
\newblock Kluwer Academic Publisher, 2000.
\bibitem{ZHR91}
C.~Zhou, C.A.R. Hoare, and A.P. Ravn.
\newblock A calculus of durations.
\newblock {\em Information Processing Letters}, 40(5):269--276, 1991.
\end{thebibliography}
}
}
@INPROCEEDINGS{ho02,
AUTHOR = {J. Hoenicke and E.-R. Olderog},
TITLE = {{Combining Specification Techniques for Processes Data and
Time}},
EDITOR = {M. Butler and L. Petre and K. Sere},
BOOKTITLE = {Integrated Formal Methods},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {2335},
PUBLISHER = {Springer-Verlag},
URL = {http://csd.Informatik.Uni-Oldenburg.DE/~skript/pub/Papers/ho02-ifm.pdf},
YEAR = {2002},
MONTH = {May},
PAGES = {245--266},
ABSTRACT = {
We present a new combination CSP-OZ-DC of three well researched
formal techniques for the specification of processes, data and
time: CSP [Hoa85], Object-Z [Smi00], and Duration Calculus
[ZHR91]. The emphasis is on a smooth integration of the underlying
semantic models and its use for verifying properties of CSP-OZ-DC
specifications by a combined application of the model-checkers FDR
[Ros94] for CSP and UPPAAL [BLL97] for Timed Automata. This
approach is applied to part of a case study on radio controlled
railway crossings.
}
}
@INPROCEEDINGS{fow01,
AUTHOR = {C. Fischer and E.-R. Olderog and H. Wehrheim},
TITLE = {{A CSP view on UML-RT structure diagrams}},
BOOKTITLE = {{Fundamental Approaches to Software Engineering}},
PAGES = {91-108},
YEAR = {2001},
EDITOR = {H. Husmann},
VOLUME = {2029},
SERIES = {Lecture Notes in Computer Science},
PUBLISHER = {Springer-Verlag},
ABSTRACT = {
UML-RT is an extension of UML for modelling embedded reactive and
real-time software systems. Its particular focus lies on system
descriptions on the architectural level, defining the overall
system structure. In this paper we propose to use UML-RT structure
diagrams together with the formal method CSP-OZ combining CSP and
Object-Z. While CSP-OZ is used for specifying the system
components themselves (by CSP-OZ classes), UML-RT diagrams provide
the architecture description. Thus the usual architecture
specification in terms of the CSP operators parallel composition,
renaming and hiding is replaced by a graphical description. To
preserve the formal semantics of CSP-OZ specifications, we develop
a translation from UML-RT structure diagrams to CSP. Besides
achieving a more easily accessible, graphical architecture
modelling for CSP-OZ, we thus also give a semantics to UML-RT
structure diagrams.
},
URL = {http://csd.informatik.uni-oldenburg.de/~wehrheim/fase01.ps}
}
@INPROCEEDINGS{bo01,
AUTHOR = {M. Broy and E.-R. Olderog},
TITLE = {{Trace-Oriented Models of Concurrency}},
BOOKTITLE = {Handbook of Process Algebra},
PAGES = {101-195},
YEAR = {2001},
EDITOR = {J.A. Bergstra and A. Ponse and S.A. Scott},
PUBLISHER = {Elsevier Science B.V.},
ABSTRACT = {
This chapter provides an in-depth presentation of trace-oriented
models of concurrent processes. We begin by introducing and
investigating finite traces as a simple abstraction of the
transition behaviour of automata. Using finite traces safety
properties of processes can be modelled. Later infinite traces or
{\it streams} together with stream processing functions are
studied. Using infinite traces more advanced phenomena like
fairness and liveness properties can be modelled. We discuss and
relate operational, denotational, algebraic and logical approaches
to trace-oriented models and explain methods for the specification
and verification of process behaviour based on these models.
}
}
@INPROCEEDINGS{or00,
AUTHOR = {E.-R. Olderog and A.P. Ravn},
TITLE = {Documenting Design Refinement},
EDITOR = {M.P.E. Heimdahl},
BOOKTITLE = {Proc. of the Third Workshop on Formal Methods in Software
Practice},
PAGES = {89--100},
PUBLISHER = {ACM},
YEAR = {2000},
ABSTRACT = {
We show how UML class diagrams can be used to document design by
refinement in the early design stages. This is illustrated by an
example from the area of embedded real-time and hybrid systems. A
precise semantics is given for the UML class diagrams by
translation to the Z schema calculus.
},
URL = {http://csd.Informatik.Uni-Oldenburg.DE/pub/Papers/or00.ps}
}
@INPROCEEDINGS{uniform99,
AUTHOR = {B. Krieg-Br\"uckner and J. Peleska and E.-R. Olderog and A.
Baer},
TITLE = {{The UniForM Workbench, a Universal Development
Environment for Formal Methods}},
EDITOR = {J.M. Wing and J. Woodcock and J. Davies},
BOOKTITLE = {{FM'99 -- Formal Methods}},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {1709},
PUBLISHER = {Springer},
YEAR = {1999},
PAGES = {1186--1205}
}
@ARTICLE{ero99-login,
AUTHOR = {E.-R.Olderog},
TITLE = {Sichere {B}ahnsteuerungen},
JOURNAL = {Log {IN}},
PAGES = {64--65},
NUMBER = {1},
YEAR = {1999}
}
@INPROCEEDINGS{ero99,
AUTHOR = {E.-R. Olderog},
TITLE = {{Correct Real-Time Software for Programmable Logic
Controllers}},
BOOKTITLE = {{Correct System Design - Recent Insights and Advances}},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {1710},
PUBLISHER = {Springer},
YEAR = {1999},
PAGES = {342--362}
}
@INPROCEEDINGS{ero99-gi/itg,
AUTHOR = {E.-R. Olderog},
TITLE = {Entwicklung korrekter zeitkritischer {Systeme}},
BOOKTITLE = {{Formale} {Beschreibungstechniken} f\"ur verteilte
{Systeme}},
EDITOR = {K. Spies and B. Sch\"atz },
SERIES = {GI/ITG Fachgespr\"ach},
VOLUME = {9},
PUBLISHER = {Utz Verlag},
YEAR = {1999},
PAGES = {7--16}
}
@ARTICLE{msero99,
AUTHOR = {Michael Schenke and E.-R. Olderog},
TITLE = {Transformational design of real-time systems -- Part 1:
from requirements to program specifications.},
JOURNAL = {Acta Informatica 36},
PAGES = {1-65},
YEAR = {1999},
URL = {http://csd.informatik.uni-oldenburg.de/pub/Papers/msero97_1.ps.gz}
}
@INPROCEEDINGS{erocd98,
AUTHOR = {V. Grabowski and C. Dietz and E.-R. Olderog},
TITLE = {{Semantics for Timed Message Sequence Charts via
Constraint Diagrams}},
BOOKTITLE = {Proceedings of the 1st Workshop of the SDL Forum Society
on SDL and MSC},
EDITOR = {Y. Lahav and A. Wolisz and J. Fischer and E. Holz},
SERIES = {Informatik-Bericht Nr. 104},
YEAR = {Juli 1998},
PAGES = {251-260},
PUBLISHER = {Humbold-Universitaet zu Berlin/Germany}
}
@INPROCEEDINGS{ero98:formalmethodrealtimesystem,
AUTHOR = {E.-R. Olderog},
TITLE = {Formal Methods in Real-Time Systems},
BOOKTITLE = {Proceedings of the 10th EuroMicro Workshop on Real Time
Systems},
YEAR = 1998,
ORGANIZATION = {IEEE Computer Society},
MONTH = {June},
PAGES = {254--263}
}
@INPROCEEDINGS{erohd98,
AUTHOR = {E.-R. Olderog and H. Dierks},
TITLE = {{Decomposing Real-Time Specifications}},
BOOKTITLE = {{Compositionality: The Significant Difference}},
EDITOR = {H. Langmaack and A. Pnueli and W.P. de Roever},
VOLUME = {1536},
SERIES = {Lecture Notes in Computer Science},
YEAR = {1998},
PUBLISHER = {Springer-Verlag},
PAGES = {465--489},
NOTE = {{\url{http://csd.informatik.uni-oldenburg.de/pub/Papers/erohd97.ps.gz}
{An abstract is available on-line}}}
}
@ARTICLE{cfskero97,
AUTHOR = {C. Fischer and S. Kleuker and E.-R. Olderog},
TITLE = {{B}eweisbar korrekte {T}elekommunikationssysteme},
JOURNAL = {Informationstechnik und Technische Informatik},
YEAR = 1997,
VOLUME = 3,
PAGES = {22--28},
NOTE = {\url{http://csd.informatik.uni-oldenburg.de/pub/Papers/cfskero97-a.ps.gz}
{An extended abstract is available on-line}},
}
@BOOK{ero97-verification,
AUTHOR = {K.-R. Apt and E.-R. Olderog},
TITLE = {Verification of Sequential and Concurrent Programs.},
EDITION = {2nd},
PUBLISHER = {Springer-Verlag},
YEAR = 1997,
NOTE = {ISBN 0-387-94896-1.
\url{http://www.springer-ny.com/catalog/np/mar97np/DATA/0-387-94896-1.html}
{This book in the Springer catalogue}.
\url{
http://csd.informatik.uni-oldenburg.de/pub/Papers/ero97-verification-a.ps.gz}
{More Information}.
}
}
@INCOLLECTION{ero96,
AUTHOR = {E.-R. Olderog and A. P. Ravn and J. U. Skakkeb{\ae}k},
TITLE = {Refining System Requirements to Program Specifications},
EDITOR = {C. Heitmeyer and D. Mandrioli},
BOOKTITLE = {Formal Methods for Real-Time Computing},
CHAPTER = 5,
PAGES = {107--134},
PUBLISHER = {Wiley},
SERIES = {Trends in Software},
VOLUME = 5,
YEAR = 1996,
NOTE = {\url{http://csd.informatik.uni-oldenburg.de/pub/Papers/ero96.ps.gz}
{An abstract is available on-line}}
}
@INPROCEEDINGS{eroms95,
AUTHOR = {E.-R. Olderog and M. Schenke},
TITLE = {Design of Real-Time Systems: The Interface between
Duration Calculus and Program Specifications},
EDITOR = {J. Desel},
BOOKTITLE = {Structures in Concurrency Theory},
PUBLISHER = {Springer-Verlag},
SERIES = {Workshops in Computing},
YEAR = 1995,
PAGES = {32--54},
URL = {http://csd.informatik.uni-oldenburg.de/pub/Papers/eroms95.ps.gz}
}
@BOOK{ero94,
AUTHOR = {K. R. Apt and E.-R. Olderog},
TITLE = {Programm\-verifikation},
PUBLISHER = {Springer-Verlag},
NOTE = {{\url{http://csd.Informatik.Uni-Oldenburg.DE/~skript/pub/Papers/Errata.ps}
{Errata-Liste}}
bzw.
{\url{http://csd.Informatik.Uni-Oldenburg.DE/~skript/pub/Papers/Errata\_long.ps}
{Errata-Liste mit Tippfehlern}}},
YEAR = 1994
}
@INPROCEEDINGS{eroms94-ftrtft,
AUTHOR = {Jifeng He and C. A. R. Hoare and M. Fr\"anzle and M.
M\"uller-Olm
and E.-R. Olderog and M. Schenke and M. R. Hansen and A. P. Ravn and H.
Rischel},
TITLE = {Provably Correct Systems},
EDITOR = {H. Langmaack and W. P. {de Roever} and J. Vytopil},
BOOKTITLE = {Formal Techniques in Real-Time and Fault-Tolerant Systems
(FTRTFT'94)},
SERIES = {Lecture Notes in Computer Science},
PUBLISHER = {Springer-Verlag},
YEAR = 1994,
VOLUME = 863,
PAGES = {288--335}
}
@INPROCEEDINGS{ero93,
AUTHOR = {J. P. Bowen and M. Fr\"anzle and E.-R. Olderog and A. P.
Ravn},
TITLE = {Developing Correct Systems},
BOOKTITLE = {Proceedings of the 5th EUROMICRO Workshop on Real-Time
Systems
(Oulu, Finland)},
PAGES = {176--189},
PUBLISHER = {IEEE Computer Society Press},
YEAR = 1993
}
@TECHREPORT{eroms93,
AUTHOR = {M. R. Hansen and E.-R. Olderog and M. Schenke and M.
Fr\"anzle and
B. {von Karger} and M. M\"uller-Olm and H. Rischel},
TITLE = {A {Duration Calculus} Semantics for Real-Time Reactive
Systems},
TYPE = {ProCoS II document},
NUMBER = {[OLD MRH 1/1]},
INSTITUTION = {University of Oldenburg, Department of Computer Science, Oldenburg, Germany},
MONTH = SEP,
YEAR = 1993,
URL = {http://csd.informatik.uni-oldenburg.de/pub/Papers/eroms93.ps.gz}
}
@INPROCEEDINGS{erosr93,
AUTHOR = {E.-R. Olderog and S. R\"ossig},
TITLE = {A Case Study in Transformational Design of Concurrent
Systems},
EDITOR = {M.-C. Gaudel and J.-P. Jouannaud},
BOOKTITLE = {Theory and Practice of Software Development (TAPSOFT'93)},
SERIES = {Lecture Notes in Computer Science},
VOLUME = 668,
PUBLISHER = {Springer-Verlag},
YEAR = 1993,
PAGES = {90--104}
}
@INCOLLECTION{ero92,
AUTHOR = {E.-R. Olderog},
TITLE = {Systematic derivation of communicating programs},
BOOKTITLE = {Programming and Mathematical Method},
PUBLISHER = {Springer-Verlag},
YEAR = 1992,
EDITOR = {M. Broy},
PAGES = {369--407}
}
@INPROCEEDINGS{ero92-icalp,
AUTHOR = {E.-R. Olderog},
TITLE = {Interfaces between Languages for Communicating Systems},
EDITOR = {W. Kuich},
BOOKTITLE = {Automata, Languages and Programming. Proceedings of the 19th
ICALP 1992},
SERIES = {Lecture Notes in Computer Science},
VOLUME = 623,
PUBLISHER = {Springer-Verlag},
YEAR = 1992,
PAGES = {641--655},
NOTE = {Invited paper}
}
@INPROCEEDINGS{ero91-algebraic,
AUTHOR = {E.-R. Olderog and K. R. Apt},
TITLE = {Using transformations to verify parallel programs},
BOOKTITLE = {Algebraic Methods II: Theory, Tools and Applications},
EDITOR = {J. A. Bergstra and L. M. G. Feijs},
VOLUME = 490,
SERIES = {Lecture Notes in Computer Science},
YEAR = 1991,
PUBLISHER = {Springer-Verlag},
PAGES = {55--81}
}
@INPROCEEDINGS{ero91-concur,
AUTHOR = {E.-R. Olderog},
TITLE = {Towards a Design Calculus for Communicating Programs},
BOOKTITLE = {Proceedings of the 2nd International Conference on
Concurrency Theory (CONCUR'91) (Amsterdam, The Netherlands)},
EDITOR = {J. C. M. Baeten and J. F. Groote},
VOLUME = 527,
SERIES = {Lecture Notes in Computer Science},
YEAR = 1991,
PUBLISHER = {Springer-Verlag},
PAGES = {61--77}
}
@ARTICLE{ero91-correctness,
AUTHOR = {E.-R. Olderog},
TITLE = {Correctness of Concurrent Processes},
JOURNAL = {Theoret.\ Comput.\ Sci.},
YEAR = 1991,
VOLUME = 80,
PAGES = {263--288}
}
@INCOLLECTION{ero91-intro,
AUTHOR = {K. R. Apt and E.-R. Olderog},
TITLE = {Introduction to Program Verification},
BOOKTITLE = {Formal Description of Programming Concepts},
SERIES = {IFIP State-of-the-Art Reports},
PUBLISHER = {Springer-Verlag},
YEAR = 1991,
EDITOR = {E. J. Neuhold and M. Paul},
PAGES = {363--429}
}
@BOOK{Old05-nets,
AUTHOR = {E.-R. Olderog},
TITLE = {Nets, Terms and Formulas: Three Views of Concurrent
Processes and Their Relationship},
PUBLISHER = {Cambridge University Press},
YEAR = 1991,
PAGES = {267},
NOTE = {Paperback Edition 2005}
}
@INCOLLECTION{ero90,
AUTHOR = {E.-R. Olderog},
TITLE = {From trace specifications to process terms},
BOOKTITLE = {Stepwise Refinement of Distributed Systems: Models,
Formalisms, Correctness},
PUBLISHER = {Springer-Verlag},
YEAR = 1990,
EDITOR = {J. W. {de Bakker} and W.-P. {de Roever} and G. Rozenberg},
VOLUME = 430,
SERIES = {Lecture Notes in Computer Science},
PAGES = {592--621}
}
@ARTICLE{ero90-acta,
AUTHOR = {J.-J. Ch. Meyer and E.-R. Olderog},
TITLE = {Hiding in Stream Semantics of Uniform Concurrency},
JOURNAL = {Acta Informatica},
YEAR = 1990,
VOLUME = 27,
PAGES = {381--397}
}
@INCOLLECTION{ero90-dijkstra,
AUTHOR = {K. R. Apt and F. S. {de Boer} and E.-R. Olderog},
TITLE = {Proving termination of parallel programs},
BOOKTITLE = {Beauty is our Business --- A Birthday Salute to Edsger W.
Dijkstra},
PUBLISHER = {Springer-Verlag},
YEAR = 1990,
EDITOR = {W. H. J. Feijen and A. J. M. {van Gasteren} and D. Gries and
J. Misra}
}
@ARTICLE{ero89,
TITLE = {A {ProCoS} Project Description},
AUTHOR = {D. Bj\o{}rner and C. A. R.\ Hoare and J. P. Bowen and {He
Jifeng}
and H. Langmaack and E.-R. Olderog and U. H. Martin and V. Stavridou and F.
Nielson
and H. R. Nielson and H. Barringer and D. Edwards and H. H. L\o{}vengreen
and
A. P. Ravn and H. S. Rischel},
JOURNAL = {Bulletin of the European Association for
Theoretical Computer Science (EATCS)},
VOLUME = 39,
PAGES = {60--73},
MONTH = {October},
YEAR = 1989
}
@ARTICLE{ero88-jcss,
AUTHOR = {J. W. {de Bakker} and J.-J. Ch. Meyer and E.-R. Olderog and
J. I. Zucker},
TITLE = {Transition Systems, Metric Spaces and Ready Sets in the
Semantics of Uniform Concurrency},
JOURNAL = {Journal of Computer and System Sciences},
YEAR = 1988,
VOLUME = 36,
PAGES = {158--224}
}
@ARTICLE{ero88-siam,
AUTHOR = {J. A. Bergstra and J. W. Klop and E.-R. Olderog},
TITLE = {Readies and Failures in the Algebra of Communicating
Processes},
JOURNAL = {SIAM J.\ Comput.},
YEAR = 1988,
VOLUME = 17,
PAGES = {1134--1177}
}
@ARTICLE{ero88-toplas,
AUTHOR = {E.-R. Olderog and K. R. Apt},
TITLE = {Fairness in Parallel Programs: the Transformational
Approach},
JOURNAL = {ACM TOPLAS},
YEAR = 1988,
VOLUME = 10,
PAGES = {420--455}
}
@ARTICLE{ero87,
AUTHOR = {J. W. de Bakker and J.-J. Ch. Meyer and E.-R. Olderog},
TITLE = {Infinite Streams and Finite Observations in the Semantics
of Uniform Concurrence},
JOURNAL = {Theoret.\ Comput.\ Sci.},
YEAR = 1987,
VOLUME = 49,
PAGES = {87--112}
}
@INPROCEEDINGS{bko87,
AUTHOR = {J.A. Bergstra and J.W. Klop and E.-R. Olderog},
TITLE = {Failures without Chaos: a Process Semantics for Fair
Abstraction},
BOOKTITLE = {Formal Description of Programming Concepts -- III},
EDITOR = {M. Wirsing},
SERIES = {Lecture Notes in Computer Science},
YEAR = {1987},
PUBLISHER = {North-Holland},
ADDRESS = {Amsterdam},
PAGES = {77--101}
}
@ARTICLE{ero86,
AUTHOR = {E.-R. Olderog and C. A. R. Hoare},
TITLE = {Specification-oriented Semantics for Communicating
Processes},
JOURNAL = {Acta Informatica},
YEAR = 1986,
VOLUME = 23,
PAGES = {9--66}
}
@INPROCEEDINGS{bmoz85,
AUTHOR = {J.W. de Bakker and J.-J. Ch. Meyer and E.-R. Olderog and J.I.
Zucker},
TITLE = {Transition systems, infinitary languages and the semantics
of uniform concurrency},
BOOKTITLE = {Proc.~17th ACM Symp.~on Theory of Computing},
YEAR = {1985},
PUBLISHER = {ACM Press},
PAGES = {252--262},
NOTE = {Providence, R.I.}
}
@INPROCEEDINGS{ol84-overview,
AUTHOR = {E.-R. Olderog},
TITLE = {Hoare's logic for programs with procedures---what has been
achieved?},
BOOKTITLE = {Proc. Logics of Programs},
EDITOR = {E.M. Clarke and D. Kozen},
VOLUME = {164},
SERIES = {Lecture Notes in Computer Science},
YEAR = {1984},
PUBLISHER = {Springer},
PAGES = {383--395}
}
@ARTICLE{ol84,
AUTHOR = {E.-R. Olderog},
TITLE = {Correctness of Programs with {P}ascal-like Procedures without
Global
Variables},
JOURNAL = {Theoretical Computer Science},
YEAR = {1984},
VOLUME = {30},
PAGES = {49--90}
}
@INPROCEEDINGS{ol83-phd,
AUTHOR = {E.-R. Olderog},
TITLE = {A Characterization of {H}oare's logic for programs with
{P}ascal-like procedures},
BOOKTITLE = {Proc.~15th ACM Symp.~on Theory of Computing},
YEAR = {1983},
PUBLISHER = {ACM Press},
MONTH = {April},
PAGES = {320--329},
NOTE = {Boston, Mass.}
}
@ARTICLE{ao83,
AUTHOR = {K.R. Apt and E.-R. Olderog},
TITLE = {Proof Rules and Transformations Dealing with Fairness},
JOURNAL = {Science of Computer Programming},
YEAR = {1983},
VOLUME = {3},
PAGES = {65--100}
}
@ARTICLE{ol83,
AUTHOR = {E.-R. Olderog},
TITLE = {On the Notion of Expressiveness and the Rule of Adaptation},
JOURNAL = {Theoretical Computer Science},
YEAR = {1983},
VOLUME = {24},
PAGES = {337--347}
}
@ARTICLE{ol81-msc,
AUTHOR = {E.-R. Olderog},
TITLE = {Sound and Complete {H}oare-like Calculi based on Copy Rules},
JOURNAL = {Acta Informatica},
YEAR = {1981},
VOLUME = {16},
PAGES = {161--197}
}
@INPROCEEDINGS{lo80-l4,
AUTHOR = {H. Langmaack and E.-R. Olderog},
TITLE = {Present-day {H}oare-like systems for programming languages
with procedures: power, limits and most likely extensions},
BOOKTITLE = {Automata, Languages and Programming (Proc.~7th ICALP)},
EDITOR = {J.W. de Bakker and J. van Leeuwen},
VOLUME = {85},
SERIES = {Lecture Notes in Computer Science},
YEAR = {1980},
PUBLISHER = {Springer},
PAGES = {363--373}
}
