
Correct System Design
Publications 1991-1994
On this page:
- Recent Publications (since 2007)
- Publications 2004-2006
- Publications 2001-2003
- Publications 1998-2000
- Publications 1995-1997
- Publications 1991-1994 (BibTeX Source)
- Publications 1980-1990
back to the mainpage.
6 Publications 1991-1994 (BibTeX Source)
@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} } @MISC{jb94, AUTHOR = { J{\"u}rgen Bohn }, TITLE = { Formal Reasoning about Specification and Transformation of Reactive Systems }, YEAR = 1994, NOTE = {Draft version} } @INPROCEEDINGS{jb94-hol, AUTHOR = { J{\"u}rgen Bohn }, TITLE = { Formal Transformational Reasoning about Reactive Systems in the Theorem Prover {LAMBDA} }, BOOKTITLE = { Supplementary proceedings of the 7th international workshop on Higher Order Logic Theorem Proving and its Applications }, YEAR = 1994, EDITOR = { T. Melham and J. Camilleri }, PUBLISHER = { University of Malta } } @INPROCEEDINGS{ms94, AUTHOR = {M. Schenke}, TITLE = {A Timed Specification Language for Concurrent Reactive Systems}, EDITOR = { D. J. Andrews and J. F. Groote and C. A. Middelburg}, BOOKTITLE = {Semantics of Specification Languages}, SERIES = {Workshops in Computing}, PUBLISHER = {Springer-Verlag}, YEAR = 1994, PAGES = {152--167}, URL = {http://csd.informatik.uni-oldenburg.de/pub/Papers/ms94.ps.gz} } @INPROCEEDINGS{ms94-ftrtft, AUTHOR = {M. Schenke}, TITLE = {Specification and Transformation of Reactive Systems with Time Restrictions and Concurrency}, BOOKTITLE = {Formal Techniques in Real-Time and Fault-Tolerant Systems (FTRTFT'94)}, EDITOR = {H. Langmaack and W.-P. {de Roever} and J. Vytopil}, SERIES = {Lecture Notes in Computer Science}, PUBLISHER = {Springer-Verlag}, YEAR = 1994, VOLUME = 863, PAGES = {605--621}, URL = {http://csd.informatik.uni-oldenburg.de/pub/Papers/ms94-ftrtft.ps.gz} } @INPROCEEDINGS{sk94, AUTHOR = {S. Kleuker}, TITLE = {Case Study: Stepwise Refinement of a Communication Processor Using Trace Logic}, BOOKTITLE = {Semantics of Specification Languages}, EDITOR = {D. J. Andrews and J. F. Groote and C. A. Middelburg}, PUBLISHER = {Springer-Verlag}, SERIES = {Workshops in Computing}, YEAR = 1994, PAGES = {252--269}, ABSTRACT = { 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. } } @PHDTHESIS{sr94-phd, AUTHOR = {S. R\"ossig}, TITLE = { A Transformational Approach to the Design of Communicating Systems}, SCHOOL = {University of Oldenburg, Department of Computer Science, Oldenburg, Germany}, MONTH = OCT, YEAR = 1994 } @INPROCEEDINGS{cd94, AUTHOR = {C. Dietz and G. Schreiber}, TITLE = {A Term Representation of {P/T} systems}, BOOKTITLE = {Application and Theory of Petri Nets}, EDITOR = {R. Valette}, VOLUME = 815, SERIES = {Lecture Notes in Computer Science}, YEAR = 1994, PUBLISHER = {Springer-Verlag}, PAGES = {239--257}, NOTE = {\url{http://csd.informatik.uni-oldenburg.de/pub/Papers/cd94-ea.ps.gz} {An extended abstract is available on-line}} } @INPROCEEDINGS{hf93-ieee, AUTHOR = {Hans Fleischhack and Ulrike Lichtblau}, TITLE = {{MOBY} --- {A} tool for high level {P}etri {N}ets with objects}, BOOKTITLE = {Proceedings of the IEEE-SMC'93-Conference (Le Touquet, France, 1993)}, PAGES = {644--649}, YEAR = 1993 } @INPROCEEDINGS{hf93, AUTHOR = {Hans Fleischhack and Ulrike Lichtblau and Michael Sonnenschein and Ralf Wie\-ting}, TITLE = {{A}bstraktion und {Z}eitbegriff in h\"oheren {N}etzen}, BOOKTITLE = {{P}etri-{N}etze im {E}insatz f\"ur {E}ntwurf und {E}ntwicklung von {I}nformationssystemen}, EDITOR = {G. Scheschonk}, ADDRESS = {Berlin [u.a.]}, YEAR = {1993} } @UNPUBLISHED{cf93, AUTHOR = {Clemens Fischer}, TITLE = {{Fehleranalyse bei der Spezifikationsentwicklung von intelligenten Telefonnetzen}}, YEAR = 1993, MONTH = NOV, TYPE = {Studienarbeit}, NOTE = {University of Oldenburg, Department of Computer Science, Oldenburg, Germany} } @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 } @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} } @INPROCEEDINGS{jb93-gi, AUTHOR = { J{\"u}rgen Bohn }, TITLE = { {I}nteraktive {S}ynthese kommunizierender {S}ysteme mit {LAMBDA}}, BOOKTITLE = { Formale Methoden zum Entwurf korrekter Systeme }, YEAR = 1993, EDITOR = { Th. Kropf and R. Kumar and D. Schmid }, ORGANIZATION = { GI/ITG--Workshop }, PUBLISHER = { University of Karlsruhe, Germany } } @INPROCEEDINGS{jb93-hoa, AUTHOR = { J{\"u}rgen Bohn }, TITLE = { Formalizing the Transformational Design of Communicating Systems in the Theorem Prover {LAMBDA} }, BOOKTITLE = { Higher Order Algebra, Logic and Term Rewriting (HOA'93)}, YEAR = 1993, EDITOR = {J. Heering and K. Meinke and B. M\"oller }, PUBLISHER = { CWI, Amsterdam, The Netherlands } } @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{ms92, AUTHOR = {M. Schenke}, TITLE = {Predicative Specification of Timed Processes}, BOOKTITLE = {Real-Time: Theory in Practice}, EDITOR = {J. W. {de Bakker} and W.-P. {de Roever} and G. Rozenberg}, SERIES = {Lecture Notes in Computer Science}, PUBLISHER = {Springer-Verlag}, VOLUME = 600, PAGES = {603--617}, YEAR = 1992, URL = {http://csd.informatik.uni-oldenburg.de/pub/Papers/ms92.ps.gz} } @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} } @INPROCEEDINGS{srms91, AUTHOR = {S. R\"ossig and M. Schenke}, TITLE = {Specification and Stepwise Development of Communicating Systems}, BOOKTITLE = {Formal Software Development Methods (VDM'91)}, EDITOR = {S. Prehn and W. J. Toetenel}, VOLUME = 551, SERIES = {Lecture Notes in Computer Science}, YEAR = 1991, PUBLISHER = {Springer-Verlag}, PAGES = {149--163}, URL = {http://csd.informatik.uni-oldenburg.de/pub/Papers/srms91.ps.gz} }