Entwicklung korrekter Systeme

Prof. Dr. Ernst-Rüdiger Olderog

Anschrift: Prof. Dr. Ernst-Rüdiger Olderog
Universität Oldenburg
Fakultät II
Department für Informatik
26111 Oldenburg
Foto
Raum: A3 2-211
Telefon: (04 41) 798-2439
Fax: (04 41) 798-2965
E-Mail: Ernst-Ruediger.Olderog


Neues Buch

[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 ]

 


zum Seitenanfang

Curriculum Vitae

1974-1979 Studium der Informatik, Mathematik und Logik an der Universität Kiel
1979 Diplom
1981 Promotion zum Dr.rer.nat.
1981-1983 Programming Research Group an der Oxford University
1984-1989 diverse Forschungsbesuche in Amsterdam, Edinburgh, Yorktown Heights und Saarbrücken
1989 Habilitation in Informatik
1989-1994 C3-Professur im Fachbereich Informatik der Universität Oldenburg
seit 1994 C4-Professur im Fachbereich Informatik der Universität Oldenburg
1994-1999 Leibniz-Preis der DFG
1995-2005 Vorsitz der IFIP Working Group 2.2 on Formal Description of Programming Concepts


zum Seitenanfang

Projekte

  • ESPRIT Basic Research Actions ProCoS I and II (Provably Correct Systems, 1989-95)
  • KORSO (Korrekte Software, 1990-93)
  • CoCoN (Provably Correct Communication Networks, mit Philips Research Lab in Aachen, 1993-96)
  • UniForM (Universal Workbench for Formal Methods, 1995-98)
  • Kombination von Prozessen, Daten und Zeit (DFG, 1999-2001)
  • ForMooS (Einbettung einer objekt-orientierten formalen Methode in einen objekt-orientierten Software-Entwicklungsprozess, DFG, 2001-2005)
  • Beteiligung am Virtuellen Software-Engineering Kompetenzzentrum ViSEK im OFFIS (BMBF, 2000-2003)
  • Beteiligung am Transregio-SFB AVACS (DFG, seit 2004)
  • Teilnahme am Projekt IMoST (Integrated Modeling for Safe Transportation) (MWK, seit 2007)

zum Seitenanfang

Herausgeber

 [Acta]
Managing Editor der Zeitschrift 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 ]


zum Seitenanfang

Bücher

[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 ]

[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 ]


zum Seitenanfang

Publikationen

[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 | 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 ]