Publications 1991-1994

 

6 Publications 1991-1994 (with Abstracts)

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

[Boh94a]

Jürgen Bohn. Formal reasoning about specification and transformation of reactive systems, 1994. Draft version.
[ bib ]

[Boh94b]

Jürgen Bohn. Formal transformational reasoning about reactive systems in the theorem prover LAMBDA. In T. Melham and J. Camilleri, editors, Supplementary proceedings of the 7th international workshop on Higher Order Logic Theorem Proving and its Applications. University of Malta, 1994.
[ bib ]

[Sch94b]

M. Schenke. A timed specification language for concurrent reactive systems. In D. J. Andrews, J. F. Groote, and C. A. Middelburg, editors, Semantics of Specification Languages, Workshops in Computing, pages 152-167. Springer-Verlag, 1994.
[ bib | .ps.gz ]

[Sch94a]

M. Schenke. Specification and transformation of reactive systems with time restrictions and concurrency. 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 605-621. Springer-Verlag, 1994.
[ bib | .ps.gz ]

[Kle94]

S. Kleuker. Case study: Stepwise refinement of a communication processor using trace logic. In D. J. Andrews, J. F. Groote, and C. A. Middelburg, editors, Semantics of Specification Languages, Workshops in Computing, pages 252-269. Springer-Verlag, 1994.
[ bib ]

This paper shows a stepwise development of a complex parallel system. Both the initial requirements and the subsequent design stages are formulated in trace logic and so every proof of correctness boils down to reasoning about trace predicates. The relation between trace logic and a program language is shown by a transformation from trace logic into a program specification language, called SL. The advantage is that a large set of verified SL-specifications can be automatically transformed into correct OCCAM programs. In contrast to trace logic, SL-specifications describe the process behaviour in more detail.

[R94]

S. Rössig. A Transformational Approach to the Design of Communicating Systems. PhD thesis, University of Oldenburg, Department of Computer Science, Oldenburg, Germany, October 1994.
[ bib ]

[DS94]

C. Dietz and G. Schreiber. A term representation of P/T systems. In R. Valette, editor, Application and Theory of Petri Nets, volume 815 of Lecture Notes in Computer Science, pages 239-257. Springer-Verlag, 1994. An extended abstract is available on-line.
[ bib ]

[FL93]

Hans Fleischhack and Ulrike Lichtblau. MOBY - A tool for high level Petri Nets with objects. In Proceedings of the IEEE-SMC'93-Conference (Le Touquet, France, 1993), pages 644-649, 1993.
[ bib ]

[FLSWt93]

Hans Fleischhack, Ulrike Lichtblau, Michael Sonnenschein, and Ralf Wieting. Abstraktion und Zeitbegriff in höheren Netzen. In G. Scheschonk, editor, Petri-Netze im Einsatz für Entwurf und Entwicklung von Informationssystemen, Berlin [u.a.], 1993.
[ bib ]

[Fis93]

Clemens Fischer. Fehleranalyse bei der Spezifikationsentwicklung von intelligenten Telefonnetzen. University of Oldenburg, Department of Computer Science, Oldenburg, Germany, November 1993.
[ 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 ]

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

[Boh93b]

Jürgen Bohn. Interaktive Synthese kommunizierender Systeme mit LAMBDA. In Th. Kropf, R. Kumar, and D. Schmid, editors, Formale Methoden zum Entwurf korrekter Systeme. GI/ITG-Workshop, University of Karlsruhe, Germany, 1993.
[ bib ]

[Boh93a]

Jürgen Bohn. Formalizing the transformational design of communicating systems in the theorem prover LAMBDA. In J. Heering, K. Meinke, and B. Möller, editors, Higher Order Algebra, Logic and Term Rewriting (HOA'93). CWI, Amsterdam, The Netherlands, 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 ]

[Sch92]

M. Schenke. Predicative specification of timed processes. In J. W. de Bakker, W.-P. de Roever, and G. Rozenberg, editors, Real-Time: Theory in Practice, volume 600 of Lecture Notes in Computer Science, pages 603-617. Springer-Verlag, 1992.
[ bib | .ps.gz ]

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

[RS91]

S. Rössig and M. Schenke. Specification and stepwise development of communicating systems. In S. Prehn and W. J. Toetenel, editors, Formal Software Development Methods (VDM'91), volume 551 of Lecture Notes in Computer Science, pages 149-163. Springer-Verlag, 1991.
[ bib | .ps.gz ]