Correct System Design

Publications 1991-1994

 

go next top of page

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