Prof. Dr. Ernst-Rüdiger Olderog
On this page:
back to the mainpage.
1
Publications (BibTeX Source)
@INPROCEEDINGS{avacs-h3-dec-11,
AUTHOR = {M. Hilscher AND S. Linker AND E.-R. Olderog AND A.P.
Ravn},
TITLE = {An Abstract Model for Proving Safety of Multi-Lane Traffic
Manoeuvres},
BOOKTITLE = {Int'l Conf.\ on Formal Engineering Methods (ICFEM)},
YEAR = {2011},
EDITOR = {Shengchao Qin AND Zongyan Qiu},
VOLUME = {6991},
SERIES = {Lecture Notes in Computer Science},
MONTH = {Oct.},
PUBLISHER = {Springer-Verlag},
NOTE = {The original publication is available at \url{http://www.springerlink.com}{www.springerlink.com}. (to appear)},
SUBPROJECT = {H3},
ABSTRACT = { We present an approach to prove safety (collision
freedom) of multi-lane motorway trac with lane-change
manoeuvres. This is ultimately a hybrid veri cation problem
due to the continuous dynamics of the cars. We abstract
from the dynamics by introducing a new spatial interval
logic based on the view of each car. To guarantee safety,
we present two variants of a lane-change controller, one
with perfect knowledge of the safety envelopes of
neighbouring cars and one which takes only the size of the
neighbouring cars into account. Based on these controllers
we provide a local safety proof for unboundedly many cars
by showing that at any moment the reserved space of each
car is disjoint from the reserved space of any other car.
}
}
@ARTICLE{FLO+2011,
AUTHOR = {Johannes Faber and Sven Linker and Ernst-R{\"u}diger Olderog and
Jan-David Quesel},
TITLE = {Syspect - Modelling, Specifying, and Verifying Real-Time Systems with
Rich Data},
JOURNAL = {International Journal of Software and Informatics},
YEAR = {2011},
VOLUME = {5},
NUMBER = {1-2},
PART = {1},
PAGES = {117--137},
NOTE = {ISSN 1673-7288.},
URL = {http://www.ijsi.org/IJSI/ch/reader/create_pdf.aspx?file_no=i78&flag=1&journal_id=ijsi},
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. },
}
@INPROCEEDINGS{HMO10,
AUTHOR = {J. Hoenicke and R. Meyer and E.-R. Olderog},
TITLE = {Kleene, Rabin, and Scott Are Available},
EDITOR = {Paul Gastin and Fran\c{c}ois Laroussinie},
BOOKTITLE = {CONCUR 2010 - Concurrency Theory (CONCUR)},
PUBLISHER = {Springer},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {6269},
PAGES = {462-477},
YEAR = {2010},
URL = {http://dx.doi.org/10.1007/978-3-642-15375-4_32}
}
@INPROCEEDINGS{OS10,
AUTHOR = {E.-R. Olderog and M. Swaminathan},
TITLE = {Layered Composition for Timed Automata},
EDITOR = {K. Chatterjee and T. A Henzinger},
BOOKTITLE = {Formal Modeling and Analysis of Timed Systems (FORMATS) },
SERIES = {Lecture Notes in Computer Science},
VOLUME = {6246},
PUBLISHER = {Springer-Verlag},
PAGES = {228-242},
YEAR = {2010},
URL = {http://dx.doi.org/10.1007/978-3-642-15297-9_18}
}
@INPROCEEDINGS{HOP10,
AUTHOR = {J. Hoenicke and E.-R. Olderog and A. Podelski},
TITLE = {Fairness for Dynamic Control},
EDITOR = {J. Esparza and R. Majumdar },
BOOKTITLE = {Tools and Algorithms for the Construction and Analysis of Systems (TACAS) },
SERIES = {Lecture Notes in Computer Science},
VOLUME = {6015},
PUBLISHER = {Springer-Verlag},
PAGES = {251--265},
YEAR = {2010}
}
@INPROCEEDINGS{OlPo10,
AUTHOR = {E.-R. Olderog and A. Podelski},
EDITOR = {D. Dams and U. Hannemann and M. Steffen},
TITLE = { Explicit Fair Scheduling for Dynamic Control },
BOOKTITLE = {Concurrency, Compositionality, and Correctness },
SERIES = {Lecture Notes in Computer Science},
VOLUME = {5930 },
PUBLISHER = {Springer-Verlag },
PAGES = {96--117 },
YEAR = {2010}
}
@INPROCEEDINGS{ero-rm-09,
AUTHOR = {E.-R. Olderog and R. Meyer},
TITLE = {Automata-theoretic verification based on
counterexample specification},
EDITOR = {V. Diekert and K. Weicker and N. Weicker},
BOOKTITLE = {Informatik als Dialog zwischen Theorie und Anwendung},
YEAR = {2009},
PAGES = {217--225},
PUBLISHER = {Vieweg-Teubner},
}
@BOOK{ABO09-Book3,
AUTHOR = { K. R. Apt and F. S. de Boer and E.-R. Olderog },
TITLE = {Verification of Sequential and Concurrent Programs,
3rd Edition},
SERIES = {Texts in Computer Science},
PUBLISHER = {Springer-Verlag},
YEAR = {2009},
NOTE = {502 pp, ISBN 978-1-84882-744-8}
}
@INPROCEEDINGS{ABO09,
AUTHOR = { K.R. Apt and F.S. de Boer and E.-R. Olderog },
EDITOR = { O. Grumberg and M. Kaminski and S. Katz and S. Wintner },
TITLE = { Modular Verification of Recursive Programs },
BOOKTITLE = { Languages: From Formal to Natural },
SERIES = { Lecture Notes in Computer Science},
VOLUME = { 5333 },
PUBLISHER = { Springer-Verlag },
EDITOR = { },
PAGES = { 1--21 },
YEAR = { 2009 }
}
@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/}}
}
@INPROCEEDINGS{Old08,
AUTHOR = {E.-R. Olderog},
TITLE = {Automatic Verification of Combined Specifications},
BOOKTITLE = {Proc. of the 1st Internat. Workshop on Harnessing Theories for
Tool Support in Software (TTSS 2007), Macau},
YEAR = {2008},
EDITOR = {G. Pu and V. Stolz},
SERIES = {ENTCS},
JOURNAL = {Electr. Notes Theor. Comput. Sci.},
ISSN = {1571-0661},
VOLUME = {207},
NUMBER = {},
MONTH = {April},
PAGES = {3--16},
EE = {http://dx.doi.org/10.1016/j.entcs.2008.03.082},
URL = {},
KEYWORDS = {Real-time systems, complex data,
CSP, Object-Z, Duration Calculus,
model checking, abstraction refinement,
UML profile, tool support},
ABSTRACT = { This paper gives an overview of results of the project
``Beyond Timed Automata'' carried out in the Collaborative Research Center AVACS
(Automatic Verification and Analysis of Complex Systems)
of the Universities of Oldenburg, Freiburg, and Saarbr\"ucken.
We discuss how properties of high-level specifications
of real-time systems combining the dimensions of
process behaviour, data, and time
can be automatically verified, exploiting recent advances
in semantics, constraint-based model checking, and
decision procedures for complex data.
As specification language we consider CS-OZ-DC,
which integrates concepts from
Communicating Sequential Processes (CSP), Object-Z (OZ),
and Duration Calculus (DC).
Our approach to automatic verification of CSP-OZ-DC rests
on a compositional semantics of this languages in terms of
Phase-Event-Automata. These can be translated into
Transition Constraint Systems which serve as an input
language of an abstract refinement model checker called
ARMC which can handle constraints covering both real-time
and infinite data.
This is demonstrated by a case study concerning emergency
messages in the European Train Control System (ETCS).
For CSP-OZ-DC we also discuss a UML profile and tool support.
}
}
@ARTICLE{MORW08,
AUTHOR = {M. M{\"o}ller 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 = {2008},
VOLUME = {20},
PAGES = {161--204},
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.},
}
@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}}
}
@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}
}
