Prof. Dr. Ernst-Rüdiger Olderog

 

1 Publications (with abstracts)

[OD08]

E.-R. Olderog and H. Dierks. Real-Time Systems - Formal Specification and Automatic Verification. Cambridge University Press, 2008. ISBN 978-0-521-88333-7. For more information see: http://csd.informatik.uni-oldenburg.de/rt-book/.
[ bib ]

[BPD⁺07]

B. Becker, A. Podelski, W. Damm, M. Fränzle, E.-R. Olderog, and R. Wilhelm. SFB/TR 14 AVACS - Automatic Verification and Analysis of Complex Systems. it - Information Technology, 49(2):118-126, 2007. See also http://www.avacs.org.
[ bib ]

[MORW07]

M. Möller, E.-R. Olderog, H. Rasch, and H. Wehrheim. Integrating a formal method into a software engineering process with UML and Java. Formal Apsects of Computing, 2007. To appear.
[ bib ]

We describe how CSP-OZ, a formal method combining the process algebra CSP with the specification language Object-Z, can be integrated into an object-oriented software engineering process employing the UML as a modelling and Java as an implementation language. The benefit of this integration lies in the rigour of the formal method, which improves the precision of the constructed models and opens up the possibility of (1) verifying properties of models in the early design phases, and (2) checking adherence of implementations to models.

The envisaged application area of our approach is the design of distributed reactive systems. To this end, we propose a specific UML profile for reactive systems. The profile contains facilities for modelling components, their interfaces and interconnections via synchronous/broadcast communication, and the overall architecture of a system. The integration with the formal method proceeds by generating a significant part of the CSP-OZ specification from the initially developed UML model. The formal specification is on the one hand the starting point for verifying properties of the model, for instance by using the FDR model checker. On the other hand, it is the basis for generating contracts for the final implementation. Contracts are written in the Java Modeling Language (JML) complemented by , an assertion language for specifying orderings between method invocations. A set of tools for runtime checking can be used to supervise the adherence of the final Java implementation to the generated contracts.

[DMO⁺07]

Werner Damm, Alfred Mikschl, Jens Oehlerking, Ernst-Rüdiger Olderog, Jun Pang, André Platzer, Marc Segelken, and Boris Wirtz. Automating verification of cooperation, control, and design in traffic applications. In Cliff Jones, Zhiming Liu, and Jim Woodcock, editors, Formal Methods and Hybrid Real-Time Systems, volume 4700 of LNCS, pages 115-169. Springer-Verlag, 2007. (c) Springer-Verlag.
[ bib ]

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.

Keywords:

[BOS07]

D. Basin, E.-R. Olderog, and P.E. Sevinç. Specifying and analyzing security automata using CSP-OZ. In Proceedings of the 2007 ACM Symposium on Information, Computer and Communications Security (ASIACCS 2007), pages 70-81. ACM Press, March 2007.
[ bib ]

Security automata are a variant of Büchi 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.

[OS06]

E.-R. Olderog and B. Steffen. Formale Semantik und Programmverifikation. In P. Rechenberg and G. Pomberger, editors, Informatik-Handbuch, 4. Auflage, pages 145-166. Hanser Verlag, 2006.
[ bib ]

[SBO06]

P. E. Sevinç, D. Basin, and E.-R. Olderog. Controlling access to documents: A formal access control model. In Günter Müller, editor, ETRICS 2006, volume 3995 of LNCS, pages 352-367. Springer-Verlag, June 2006.
[ bib ]

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.

[DHO06]

W. Damm, H. Hungar, and E.-R. Olderog. Verification of cooperating traffic agents. International Journal of Control, 79(5):395-421, May 2006.
[ bib ]

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.

[OW05]

E.-R. Olderog and H. Wehrheim. Specification and (property) inheritance in CSP-OZ. Science of Computer Programming, 55:227-257, 2005.
[ bib ]

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. Key words: CSP, Object-Z, failures divergence semantics, inheritance, safety and ``liveness'' properties, model-checking, FDR

References

[Fis97]

C. Fischer. CSP-OZ: A combination of Object-Z and CSP. In H. Bowman and J. Derrick, editors, Formal Methods for Open Object-Based Distributed Systems (FMOODS'97), volume 2, pages 423-438. Chapman & Hall, 1997.

[Fis00]

C. Fischer. Combination and Implementation of Processes and Data: From CSP-OZ to Java. PhD thesis, Bericht Nr. 2/2000, University of Oldenburg, April 2000.

[Weh02]

H. Wehrheim. Behavioural subtyping in object-oriented specification formalisms. University of Oldenburg, Habilitation Thesis, 2002.

[DHO04]

W. Damm, H. Hungar, and E.-R. Olderog. On the verification of cooperating traffic agents. In F.S. de Boer, M.M. Bonsangue, S. Graf, and W.-P. de Roever, editors, FMCO 2003: Formal Methods for Components and Objects, volume 3188 of LNCS, pages 77-110, 2004.
[ bib ]

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.

[MORW04]

M. Möller, E.-R. Olderog, H. Rasch, and H. Wehrheim. Linking CSP-OZ with UML and Java: A Case Study. In E. Boiten, J. Derrick, and G. Smith, editors, Integrated Formal Methods, number 2999 in Lecture Notes in Computer Science, pages 267-286. Springer-Verlag, March 2004.
[ bib | .pdf ]

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.

[OW03]

E.-R. Olderog and H. Wehrheim. Specification and Inheritance in CSP-OZ. In F. de Boer, M. Bosangue, S. Graf, and W.-P. de Roever, editors, Formal Methods for Components and Objects, volume 2852 of LNCS, pages 361-379. Springer, 2003.
[ bib ]

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.

References

[Fis97]

C. Fischer. CSP-OZ: A combination of Object-Z and CSP. In H. Bowman and J. Derrick, editors, Formal Methods for Open Object-Based Distributed Systems (FMOODS'97), volume 2, pages 423-438. Chapman & Hall, 1997.

[Fis00]

C. Fischer. Combination and Implementation of Processes and Data: From CSP-OZ to Java. PhD thesis, Bericht Nr. 2/2000, University of Oldenburg, April 2000.

[Weh02]

H. Wehrheim. Behavioural subtyping in object-oriented specification formalisms. University of Oldenburg, Habilitation Thesis, 2002.

[OD03]

E.-R. Olderog and H. Dierks. Moby/RT: A Tool for Specification and Verification of Real-Time Systems. Journal of Universal Computer Science, 9:88-105, 2003.
[ bib ]

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.

References

[Kle00]

Kleuker, C. (2000). Constraint Diagrams. PhD thesis, University of Oldenburg.

[Die00]

Dierks, H. (2000). PLC-Automata: A New Class of Implementable Real-Time Automata. TCS, 253(1):61-93.

[DO03]

H. Dierks and E.-R. Olderog. Temporale Spezifikationslogiken. at-Automatisierungstechnik, 51(2):A1-A4, 2003.
[ bib ]

Logiken sind in der Informatik ein weitverbreitetes Mittel zur Spezifikation. Dazu werden Logiken verschiedener Ausprägung benutzt, z.B. temporale Logiken für reaktive Systeme, zu denen die Systeme der Automatisierungstechnik zählen. Dieser Beitrag enthält eine Einführung in die wichtigsten temporalen Logiken und Literaturverweise.

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.

[HO02b]

J. Hoenicke and E.-R. Olderog. CSP-OZ-DC: A combination of specification techniques for processes, data and time. Nordic Journal of Computing, 9(4):301-334, 2002. appeared March 2003.
[ bib ]

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 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.

References

[BLL97]

J. Bengtsson, K.G. Larsen, F. Larsson, P. Pettersson, and Wang Yi. Uppaal - a tool suite for automatic verification of real-time systems. In R. Alur, T.A. Henzinger, and E.D. Sonntag, editors, Hybrid Systems III - Verification and Control, volume 1066 of LNCS, pages 232-243. Springer, 1997.

[Hoa85]

C.A.R. Hoare. Communicating Sequential Processes. Prentice Hall, 1985.

[Ros94]

A.W. Roscoe. Model-checking CSP. In A.W. Roscoe, editor, A Classical Mind - Essays in Honour of C.A.R.Hoare, pages 353-378. Prentice-Hall, 1994.

[Smi00]

G. Smith. The Object-Z Specification Language. Kluwer Academic Publisher, 2000.

[ZHR91]

C. Zhou, C.A.R. Hoare, and A.P. Ravn. A calculus of durations. Information Processing Letters, 40(5):269-276, 1991.

[HO02a]

J. Hoenicke and E.-R. Olderog. Combining Specification Techniques for Processes Data and Time. In M. Butler, L. Petre, and K. Sere, editors, Integrated Formal Methods, volume 2335 of Lecture Notes in Computer Science, pages 245-266. Springer-Verlag, May 2002.
[ bib | .pdf ]

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.

[FOW01]

C. Fischer, E.-R. Olderog, and H. Wehrheim. A CSP view on UML-RT structure diagrams. In H. Husmann, editor, Fundamental Approaches to Software Engineering, volume 2029 of Lecture Notes in Computer Science, pages 91-108. Springer-Verlag, 2001.
[ bib | .ps ]

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.

[BO01]

M. Broy and E.-R. Olderog. Trace-Oriented Models of Concurrency. In J.A. Bergstra, A. Ponse, and S.A. Scott, editors, Handbook of Process Algebra, pages 101-195. Elsevier Science B.V., 2001.
[ bib ]

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 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.

[OR00]

E.-R. Olderog and A.P. Ravn. Documenting design refinement. In M.P.E. Heimdahl, editor, Proc. of the Third Workshop on Formal Methods in Software Practice, pages 89-100. ACM, 2000.
[ bib | .ps ]

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.

[KBPOB99]

B. Krieg-Brückner, J. Peleska, E.-R. Olderog, and A. Baer. The UniForM Workbench, a Universal Development Environment for Formal Methods. In J.M. Wing, J. Woodcock, and J. Davies, editors, FM'99 - Formal Methods, volume 1709 of Lecture Notes in Computer Science, pages 1186-1205. Springer, 1999.
[ bib ]

[ER99]

E.-R.Olderog. Sichere Bahnsteuerungen. Log IN, (1):64-65, 1999.
[ bib ]

[Old99a]

E.-R. Olderog. Correct Real-Time Software for Programmable Logic Controllers. In Correct System Design - Recent Insights and Advances, volume 1710 of Lecture Notes in Computer Science, pages 342-362. Springer, 1999.
[ bib ]

[Old99b]

E.-R. Olderog. Entwicklung korrekter zeitkritischer Systeme. In K. Spies and B. Schätz, editors, Formale Beschreibungstechniken für verteilte Systeme, volume 9 of GI/ITG Fachgespräch, pages 7-16. Utz Verlag, 1999.
[ bib ]

[SO99]

Michael Schenke and E.-R. Olderog. Transformational design of real-time systems - part 1: from requirements to program specifications. Acta Informatica 36, pages 1-65, 1999.
[ bib | .ps.gz ]

[GDO98]

V. Grabowski, C. Dietz, and E.-R. Olderog. Semantics for Timed Message Sequence Charts via Constraint Diagrams. In Y. Lahav, A. Wolisz, J. Fischer, and E. Holz, editors, Proceedings of the 1st Workshop of the SDL Forum Society on SDL and MSC, Informatik-Bericht Nr. 104, pages 251-260. Humbold-Universitaet zu Berlin/Germany, Juli 1998.
[ bib ]

[Old98]

E.-R. Olderog. Formal methods in real-time systems. In Proceedings of the 10th EuroMicro Workshop on Real Time Systems, pages 254-263. IEEE Computer Society, June 1998.
[ bib ]

[OD98]

E.-R. Olderog and H. Dierks. Decomposing Real-Time Specifications. In H. Langmaack, A. Pnueli, and W.P. de Roever, editors, Compositionality: The Significant Difference, volume 1536 of Lecture Notes in Computer Science, pages 465-489. Springer-Verlag, 1998. An abstract is available on-line.
[ bib ]

[FKO97]

C. Fischer, S. Kleuker, and E.-R. Olderog. Beweisbar korrekte Telekommunikationssysteme. Informationstechnik und Technische Informatik, 3:22-28, 1997. An extended abstract is available on-line.
[ bib ]

[AO97]

K.-R. Apt and E.-R. Olderog. Verification of Sequential and Concurrent Programs. Springer-Verlag, 2nd edition, 1997. ISBN 0-387-94896-1. This book in the Springer catalogue. More Information.
[ bib ]

[ORS96]

E.-R. Olderog, A. P. Ravn, and J. U. Skakkebæk. Refining system requirements to program specifications. In C. Heitmeyer and D. Mandrioli, editors, Formal Methods for Real-Time Computing, volume 5 of Trends in Software, chapter 5, pages 107-134. Wiley, 1996. An abstract is available on-line.
[ bib ]

[OS95]

E.-R. Olderog and M. Schenke. Design of real-time systems: The interface between duration calculus and program specifications. In J. Desel, editor, Structures in Concurrency Theory, Workshops in Computing, pages 32-54. Springer-Verlag, 1995.
[ bib | .ps.gz ]

[AO94]

K. R. Apt and E.-R. Olderog. Programmverifikation. Springer-Verlag, 1994. Errata-Liste bzw. Errata-Liste mit Tippfehlern.
[ bib ]

[HHF⁺94]

Jifeng He, C. A. R. Hoare, M. Fränzle, M. Müller-Olm, E.-R. Olderog, M. Schenke, M. R. Hansen, A. P. Ravn, and H. Rischel. Provably correct systems. In H. Langmaack, W. P. de Roever, and J. Vytopil, editors, Formal Techniques in Real-Time and Fault-Tolerant Systems (FTRTFT'94), volume 863 of Lecture Notes in Computer Science, pages 288-335. Springer-Verlag, 1994.
[ bib ]

[BFOR93]

J. P. Bowen, M. Fränzle, E.-R. Olderog, and A. P. Ravn. Developing correct systems. In Proceedings of the 5th EUROMICRO Workshop on Real-Time Systems (Oulu, Finland), pages 176-189. IEEE Computer Society Press, 1993.
[ bib ]

[HOS⁺93]

M. R. Hansen, E.-R. Olderog, M. Schenke, M. Fränzle, B. von Karger, M. Müller-Olm, and H. Rischel. A Duration Calculus semantics for real-time reactive systems. ProCoS II document [OLD MRH 1/1], University of Oldenburg, Department of Computer Science, Oldenburg, Germany, September 1993.
[ bib | .ps.gz ]

[OR93]

E.-R. Olderog and S. Rössig. A case study in transformational design of concurrent systems. In M.-C. Gaudel and J.-P. Jouannaud, editors, Theory and Practice of Software Development (TAPSOFT'93), volume 668 of Lecture Notes in Computer Science, pages 90-104. Springer-Verlag, 1993.
[ bib ]

[Old92b]

E.-R. Olderog. Systematic derivation of communicating programs. In M. Broy, editor, Programming and Mathematical Method, pages 369-407. Springer-Verlag, 1992.
[ bib ]

[Old92a]

E.-R. Olderog. Interfaces between languages for communicating systems. In W. Kuich, editor, Automata, Languages and Programming. Proceedings of the 19th ICALP 1992, volume 623 of Lecture Notes in Computer Science, pages 641-655. Springer-Verlag, 1992. Invited paper.
[ bib ]

[OA91]

E.-R. Olderog and K. R. Apt. Using transformations to verify parallel programs. In J. A. Bergstra and L. M. G. Feijs, editors, Algebraic Methods II: Theory, Tools and Applications, volume 490 of Lecture Notes in Computer Science, pages 55-81. Springer-Verlag, 1991.
[ bib ]

[Old91c]

E.-R. Olderog. Towards a design calculus for communicating programs. In J. C. M. Baeten and J. F. Groote, editors, Proceedings of the 2nd International Conference on Concurrency Theory (CONCUR'91) (Amsterdam, The Netherlands), volume 527 of Lecture Notes in Computer Science, pages 61-77. Springer-Verlag, 1991.
[ bib ]

[Old91a]

E.-R. Olderog. Correctness of concurrent processes. Theoret. Comput. Sci., 80:263-288, 1991.
[ bib ]

[AO91]

K. R. Apt and E.-R. Olderog. Introduction to program verification. In E. J. Neuhold and M. Paul, editors, Formal Description of Programming Concepts, IFIP State-of-the-Art Reports, pages 363-429. Springer-Verlag, 1991.
[ bib ]

[Old91b]

E.-R. Olderog. Nets, Terms and Formulas: Three Views of Concurrent Processes and Their Relationship. Cambridge University Press, 1991. Paperback Edition 2005.
[ bib ]

[Old90]

E.-R. Olderog. From trace specifications to process terms. In J. W. de Bakker, W.-P. de Roever, and G. Rozenberg, editors, Stepwise Refinement of Distributed Systems: Models, Formalisms, Correctness, volume 430 of Lecture Notes in Computer Science, pages 592-621. Springer-Verlag, 1990.
[ bib ]

[MO90]

J.-J. Ch. Meyer and E.-R. Olderog. Hiding in stream semantics of uniform concurrency. Acta Informatica, 27:381-397, 1990.
[ bib ]

[AdO90]

K. R. Apt, F. S. de Boer, and E.-R. Olderog. Proving termination of parallel programs. In W. H. J. Feijen, A. J. M. van Gasteren, D. Gries, and J. Misra, editors, Beauty is our Business - A Birthday Salute to Edsger W. Dijkstra. Springer-Verlag, 1990.
[ bib ]

[BHB⁺89]

D. Bjørner, C. A. R. Hoare, J. P. Bowen, He Jifeng, H. Langmaack, E.-R. Olderog, U. H. Martin, V. Stavridou, F. Nielson, H. R. Nielson, H. Barringer, D. Edwards, H. H. Løvengreen, A. P. Ravn, and H. S. Rischel. A ProCoS project description. Bulletin of the European Association for Theoretical Computer Science (EATCS), 39:60-73, October 1989.
[ bib ]

[dMOZ88]

J. W. de Bakker, J.-J. Ch. Meyer, E.-R. Olderog, and J. I. Zucker. Transition systems, metric spaces and ready sets in the semantics of uniform concurrency. Journal of Computer and System Sciences, 36:158-224, 1988.
[ bib ]

[BKO88]

J. A. Bergstra, J. W. Klop, and E.-R. Olderog. Readies and failures in the algebra of communicating processes. SIAM J. Comput., 17:1134-1177, 1988.
[ bib ]

[OA88]

E.-R. Olderog and K. R. Apt. Fairness in parallel programs: the transformational approach. ACM TOPLAS, 10:420-455, 1988.
[ bib ]

[dBMO87]

J. W. de Bakker, J.-J. Ch. Meyer, and E.-R. Olderog. Infinite streams and finite observations in the semantics of uniform concurrence. Theoret. Comput. Sci., 49:87-112, 1987.
[ bib ]

[BKO87]

J.A. Bergstra, J.W. Klop, and E.-R. Olderog. Failures without chaos: a process semantics for fair abstraction. In M. Wirsing, editor, Formal Description of Programming Concepts - III, Lecture Notes in Computer Science, pages 77-101, Amsterdam, 1987. North-Holland.
[ bib ]

[OH86]

E.-R. Olderog and C. A. R. Hoare. Specification-oriented semantics for communicating processes. Acta Informatica, 23:9-66, 1986.
[ bib ]

[dBMOZ85]

J.W. de Bakker, J.-J. Ch. Meyer, E.-R. Olderog, and J.I. Zucker. Transition systems, infinitary languages and the semantics of uniform concurrency. In Proc. 17th ACM Symp. on Theory of Computing, pages 252-262. ACM Press, 1985. Providence, R.I.
[ bib ]

[Old84b]

E.-R. Olderog. Hoare's logic for programs with procedures-what has been achieved? In E.M. Clarke and D. Kozen, editors, Proc. Logics of Programs, volume 164 of Lecture Notes in Computer Science, pages 383-395. Springer, 1984.
[ bib ]

[Old84a]

E.-R. Olderog. Correctness of programs with Pascal-like procedures without global variables. Theoretical Computer Science, 30:49-90, 1984.
[ bib ]

[Old83a]

E.-R. Olderog. A characterization of Hoare's logic for programs with Pascal-like procedures. In Proc. 15th ACM Symp. on Theory of Computing, pages 320-329. ACM Press, April 1983. Boston, Mass.
[ bib ]

[AO83]

K.R. Apt and E.-R. Olderog. Proof rules and transformations dealing with fairness. Science of Computer Programming, 3:65-100, 1983.
[ bib ]

[Old83b]

E.-R. Olderog. On the notion of expressiveness and the rule of adaptation. Theoretical Computer Science, 24:337-347, 1983.
[ bib ]

[Old81]

E.-R. Olderog. Sound and complete Hoare-like calculi based on copy rules. Acta Informatica, 16:161-197, 1981.
[ bib ]

[LO80]

H. Langmaack and E.-R. Olderog. Present-day Hoare-like systems for programming languages with procedures: power, limits and most likely extensions. In J.W. de Bakker and J. van Leeuwen, editors, Automata, Languages and Programming (Proc. 7th ICALP), volume 85 of Lecture Notes in Computer Science, pages 363-373. Springer, 1980.
[ bib ]