
Correct System Design
Prof. Dr. Ernst-Rüdiger Olderog
| Address: | Prof. Dr. Ernst-Rüdiger Olderog University of Oldenburg Faculty II Department of Computing Science D-26111 Oldenburg Germany |
|
| Room: | A3 2-211 | |
| Phone: | +49 441 798-2439 | |
| Fax: | +49 441 798-2965 | |
| email: | Ernst-Ruediger.Olderog | |
New Book
- [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 ]
Curriculum Vitae
| 1974-1979 | study of informatics, mathematics and logics at the University of Kiel |
| 1979 | diploma degree in informatics |
| 1981 | Ph.D. in computer science |
| 1981-1983 | Programming Research Group at Oxford University |
| 1984-1989 | Various research visits in Amsterdam, Edinburgh, Yorktown Heights, and Saarbrücken |
| 1989 | Habilitation for computer science |
| 1989-1994 | Associate professor of computer science at the University of Oldenburg |
| since 1994 | Full professor of computer science at the University of Oldenburg |
| 1994-1999 | Leibniz Award of the German Research Council (DFG) |
| 1995-2005 | Chairman of IFIP Working Group 2.2 on Formal Description of Programming Concepts |
Projects
- ESPRIT Basic Research Actions ProCoS I and II (Provably Correct Systems, 1989-95)
- KORSO (Korrekte Software, 1990-93)
- CoCoN (Provably Correct Communication Networks, with Philips Research Lab Aachen, 1993-96)
- UniForM (Universal Workbench for Formal Methods, 1995-98)
- Combination of Processes, Data and Time (DFG, 1999-2001)
- ForMooS (Embedding of an object-oriented formal method in an object-oriented software development process, DFG, 2001-2005)
- Participation in the Virtual Competence Centre for Software-Engineering ViSEK at OFFIS (BMBF, 2000-2003)
- Participation in the Transregio-SFB AVACS (DFG, since 2004)
- Participation in the project IMoST (Integrated Modeling for Safe Transportation) (MWK, since 2007)
Publisher
- [Acta]
-
Managing Editor of the journal
Acta Informatica
- [DO02]
-
W. Damm and E.-R. Olderog, editors.
Formal
Techniques in Real-Time and Fault-Tolerant Systems, volume
2496 of Lecture Notes in Computer Science, 2002.
[ bib ] - [OS99]
-
E.-R. Olderog and B. Steffen, editors.
Correct System Design - Recent Insights and Advances, volume
1710
of Lecture Notes in Computer Science: State-of-the-Art-Survey.
Springer, 1999.
[ bib ] - [Old94]
-
E.-R. Olderog, editor.
Programming Concepts, Methods and Calculi (PROCOMET'94), volume
A-56 of IFIP Transactions.
North-Holland, Amsterdam, 1994.
[ bib ] - [dBOPdV94]
-
F.S. de Boer, E.-R. Olderog, A. Ponse, and F.-J. de Vries, editors.
Special Issue on Assertional Methods, volume 6 (number 6A) of
Formal Aspects of Computing.
1994.
[ bib ]
Books
- [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 ] - [AO94]
-
K. R. Apt and E.-R. Olderog.
Programmverifikation.
Springer-Verlag, 1994.
Errata-Liste bzw.
Errata-Liste mit Tippfehlern.
[ bib ] - [Old91]
-
E.-R. Olderog.
Nets, Terms and Formulas: Three Views of Concurrent Processes
and Their Relationship.
Cambridge University Press, 1991.
Paperback Edition 2005.
[ bib ]
Publications
- [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 | Abstract ] - [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 | Abstract ] - [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 | Abstract ] - [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 | Abstract ] - [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 | Abstract ] - [OW05]
-
E.-R. Olderog and H. Wehrheim.
Specification and (property) inheritance in CSP-OZ.
Science of Computer Programming, 55:227-257, 2005.
[ bib | Abstract ] - [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 | Abstract ] - [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 | Abstract ] - [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 | Abstract ] - [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 | Abstract ] - [DO03]
-
H. Dierks and E.-R. Olderog.
Temporale Spezifikationslogiken.
at-Automatisierungstechnik, 51(2):A1-A4, 2003.
[ bib | Abstract ] - [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 | Abstract ] - [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 | Abstract ] - [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 | Abstract ] - [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 | Abstract ] - [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 | Abstract ] - [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 ]