Publications 1998-2000

 

4 Publications 1998-2000 (BibTeX Source)

@ARTICLE{weh00d,
  AUTHOR = {H. Wehrheim},
  TITLE = {{Data Abstraction Techniques in the Validation of CSP-OZ
                  Specifications}},
  JOURNAL = {Formal Aspects of Computing},
  YEAR = {2000},
  VOLUME = {12},
  PAGE = {147--164}
}


@ARTICLE{dt00,
  AUTHOR = {H. Dierks and J. Tapken},
  TITLE = {{Modelling and Verifying of `Cash-Point Service' Using
      Moby/PLC}},
  JOURNAL = {Formal Aspects of Computing},
  YEAR = {2000},
  VOLUME = {12},
  PAGES = {222--221},
  URL = {http://csd.informatik.uni-oldenburg.de/pub/Papers/hdjt00.ps.gz},
}


@INPROCEEDINGS{or00,
  AUTHOR = {E.-R. Olderog and A.P. Ravn},
  TITLE = {Documenting Design Refinement},
  EDITOR = {M.P.E. Heimdahl},
  BOOKTITLE = {Proc. of the Third Workshop on Formal Methods in Software
Practice},
  PAGES = {89--100},
  PUBLISHER = {ACM},
  YEAR = {2000},
  ABSTRACT = {
    We show how UML class diagrams can be used to document design by
    refinement in the early design stages. This is illustrated by an
    example from the area of embedded real-time and hybrid systems.  A
    precise semantics is given for the UML class diagrams by
    translation to the Z schema calculus.
  },
  URL = {http://csd.Informatik.Uni-Oldenburg.DE/pub/Papers/or00.ps}
}


@INPROCEEDINGS{cfhw2000,
  AUTHOR = {Clemens Fischer and Heike Wehrheim},
  TITLE = {{Behavioural Subtyping Relations for Object-Oriented
                  Formalisms}},
  EDITOR = {T. Rus},
  BOOKTITLE = {{Algebraic Methodology and Software Technology}},
  SERIES = {LNCS},
  VOLUME = {1816},
  PUBLISHER = {Springer},
  PAGES = {469--483},
  NOTE = {},
  ABSTRACT = {
    In this paper we investigate the object-oriented notion of
    subtyping in the context of behavioural formalisms. Subtyping in
    OO-formalisms is closely related to the concept of inheritance.
    The central issue in the choice of subtyping relations among
    classes is the principle of substitutability: an instance of the
    subtype should be usable wherever an instance of the supertype was
    expected. Depending on the interpretation of ``usable'', we obtain
    a variety of subtyping relations: stronger subtyping relations,
    allowing one to share the subtype instance among different clients
    without any change compared with the supertype, and weaker
    relations, restricting the possibilities of interference of
    different clients on the subtype instance. The subtyping relations
    are taxonomically ordered in a hierarchy.  The concept of
    ``usability'' is formalised via testing scenarios, which provide
    alternative characterisations for the subtyping relations.
  },
  URL = {http://csd.informatik.uni-oldenburg.de/~wehrheim/amast00.ps},
  YEAR = {2000}
}


@INPROCEEDINGS{weh2000,
  AUTHOR = {Heike Wehrheim},
  TITLE = {Specification of an Automatic Manufacturing System -- A
    case study in using integrated formal methods},
  EDITOR = {},
  BOOKTITLE = {FASE 2000, Fundamental Approaches to Software
                  Engineering},
  SERIES = {LNCS},
  VOLUME = {1783},
  NOTE = {},
  ABSTRACT = {
    An automatic manufacturing system serves as a case study for the
    applicability of an integrated formal method to the specification
    of software systems. The formal method chosen is CSP-OZ, an
    integration of the state-oriented formalism Object-Z with the
    process algebra CSP. The practicability as well as limitations of
    CSP-OZ are studied. We furthermore employ a graphical notation
    (class diagrams) from the Unified Modelling Language to describe
    the architectural view of the system. The correctness of the
    obtained specification is checked by a translation into the input
    language of the CSP model checker FDR and a following property
    check.
  },
  URL = {http://csd.informatik.uni-oldenburg.de/~wehrheim/fase00.ps},
  YEAR = {2000}
}


@ARTICLE{die00,
  AUTHOR = {H. Dierks},
  TITLE = {{PLC-Automata: A New Class of Implementable Real-Time
                  Automata }},
  JOURNAL = {Theoret.\ Comput.\ Sci.},
  YEAR = {2000},
  VOLUME = {253},
  NUMBER = {1},
  MONTH = DEC,
  PAGES = {61--93},
  NOTE = {full version of \cite{hd97-arts}},
}


@INPROCEEDINGS{die00b,
  AUTHOR = {H. Dierks},
  TITLE = {{A Process Algebra for Real-Time Programs}},
  BOOKTITLE = {FASE 2000: Fundamental Approaches to Software
                  Engineering},
  EDITOR = {T. Maibaum},
  VOLUME = {1783},
  SERIES = {Lecture Notes in Computer Science},
  YEAR = {2000},
  PUBLISHER = {Springer-Verlag},
  PAGES = {66--81},
}


@INPROCEEDINGS{die00c,
  AUTHOR = {H. Dierks},
  TITLE = {{Specification and Verification of Polling Real-Time
                  Systems}},
  BOOKTITLE = {{Ausgezeichnete Informatikdissertationen 1999}},
  EDITOR = {H. Fiedler and O. G{\"u}nther and W. Grass and
    S. H{\"o}lldobler and G. Hotz and R. Reischuk and B. Seeger and D. Wagner},
  YEAR = {2000},
  PUBLISHER = {Teubner},
  URL = {http://csd.informatik.uni-oldenburg.de/pub/Papers/hd00.ps.gz},
}


@INPROCEEDINGS{bre:fiw00,
  AUTHOR = {Jan Bredereke},
  TITLE = {Families of Formal Requirements in Telephone Switching},
  BOOKTITLE = {Feature Interactions in Telecommunications and Software
                  Systems {VI}},
  PUBLISHER = {{IOS Press}},
  YEAR = {2000},
  MONTH = {May},
  ADDRESS = {Amsterdam},
  NOTE = {Submitted. An abstract is available
    {\url{http://csd.informatik.uni-oldenburg.de/~jan/abstracts/Bre99e.html}
      {here}}},
}


@INPROCEEDINGS{weh00b,
  AUTHOR = {Heike Wehrheim},
  TITLE = {Behavioural Subtyping and Property Preservation},
  BOOKTITLE = {FMOODS'00: Formal Methods for Open Object-Based
                  Distributed Systems},
  EDITOR = {S. Smith and C. Talcott},
  PUBLISHER = {Kluwer},
  ABSTRACT = {
    Inheritance is one of the key features in object-oriented design
    and analysis. It especially supports an incremental development by
    allowing to stepwise add new functionality to an existing system
    design.  When using a subclass which is a specialisation of a
    certain superclass, the question arises which of the superclass'
    properties still hold for the subclass. We investigate this topic
    for three behavioural subtyping relations, which formalise the
    subtype - supertype relationship among classes on the basis of
    process algebra correctness relations. According to the degree of
    change allowed by the subtyping relations, safety and liveness
    properties of the superclass are preserved up to different
    extents.
  },
  URL = {http://csd.informatik.uni-oldenburg.de/~wehrheim/fmoods00.ps},
  YEAR = {2000}
}


@INPROCEEDINGS{weh00c,
  AUTHOR = {Heike Wehrheim},
  TITLE = {Subtyping patterns for active objects},
  EDITOR = {H. Giese and S. Philippi},
  BOOKTITLE = {Proceedings 8ter Workshop des GI-Arbeitskreises GROOM:
    Visuelle Verhaltensmodellierung verteilter und nebenl\"aufiger
Software-Systeme},
  PUBLISHER = {Universit\"at M\"unster},
  NOTE = {No. 24/00-I},
  YEAR = {2000}
}


@ARTICLE{fiwe00b,
  AUTHOR = {Clemens Fischer and Heike Wehrheim},
  TITLE = {Failure-Divergence Semantics as a Formal Basis for an
    Object-Oriented Integrated Formal Method},
  JOURNAL = {Bulletin of the EATCS (European Association of Theoretical
                  Computer Science)},
  VOLUME = {71},
  PAGES = {92 -- 101},
  URL = {http://csd.informatik.uni-oldenburg.de/~wehrheim/Eatcs.ps},
  ABSTRACT = {
    The integration of several different modelling techniques into a
    single formal method has turned out to be advantageous in the
    formal design of software systems.  Giving a semantics to an
    integrated formal method is currently a very active area of
    research. In this paper we discuss the advantages of a
    failure-divergence semantics for data and process integrating
    formal methods, in particular for those with a concept of
    inheritance. The discussion proceeds along the lines of the formal
    method CSP-OZ, a combination of CSP and Object-Z, developed in
    Oldenburg.
  },
  YEAR = {2000}
}


@INPROCEEDINGS{schd99,
  TITLE = {Provably Correct Hardware Compilation using Timing
                  Diagrams},
  AUTHOR = {M. Schenke and M. Dossis},
  BOOKTITLE = {FORTE/PSTV'99},
  PUBLISHER = {Kluwer},
  PAGES = {313--331},
  YEAR = {1999}
}


@INPROCEEDINGS{schla99,
  AUTHOR = {M. Schenke and A. Lavrov},
  TITLE = {Automata-based stochastic analysis of modular hybrid
                  controllers},
  BOOKTITLE = {Conference on Probabilistic Analysis of Rare Events
                  (RARE)},
  NOTE = {ISBN 9984-668-08-8},
  YEAR = {1999}
}


@INPROCEEDINGS{uniform99,
  AUTHOR = {B. Krieg-Br\"uckner and J. Peleska and E.-R. Olderog and A.
Baer},
  TITLE = {{The UniForM Workbench, a Universal Development
                  Environment for Formal Methods}},
  EDITOR = {J.M. Wing and J. Woodcock and J. Davies},
  BOOKTITLE = {{FM'99 -- Formal Methods}},
  SERIES = {Lecture Notes in Computer Science},
  VOLUME = {1709},
  PUBLISHER = {Springer},
  YEAR = {1999},
  PAGES = {1186--1205}
}


@ARTICLE{ero99-login,
  AUTHOR = {E.-R.Olderog},
  TITLE = {Sichere {B}ahnsteuerungen},
  JOURNAL = {Log {IN}},
  PAGES = {64--65},
  NUMBER = {1},
  YEAR = {1999}
}


@INPROCEEDINGS{ero99,
  AUTHOR = {E.-R. Olderog},
  TITLE = {{Correct Real-Time Software for Programmable Logic
Controllers}},
  BOOKTITLE = {{Correct System Design - Recent Insights and Advances}},
  SERIES = {Lecture Notes in Computer Science},
  VOLUME = {1710},
  PUBLISHER = {Springer},
  YEAR = {1999},
  PAGES = {342--362}
}


@INPROCEEDINGS{ero99-gi/itg,
  AUTHOR = {E.-R. Olderog},
  TITLE = {Entwicklung korrekter zeitkritischer {Systeme}},
  BOOKTITLE = {{Formale} {Beschreibungstechniken} f\"ur verteilte
                  {Systeme}},
  EDITOR = {K. Spies and B. Sch\"atz },
  SERIES = {GI/ITG Fachgespr\"ach},
  VOLUME = {9},
  PUBLISHER = {Utz Verlag},
  YEAR = {1999},
  PAGES = {7--16}
}


@INPROCEEDINGS{bre:dagstuhl-se-requirements-noproc,
  AUTHOR = {Joanne Atlee and Wolfram Bartussek and Jan Bredereke and
                  Martin Glinz and Ridha Khedri and Lutz Prechelt and David
                  Weiss},
  TITLE = {Requirements},
  PAGES = {9--16},
  BOOKTITLE = {Software Engineering Research and Education: Seeking a new
                  Agenda},
  YEAR = {1999},
  MONTH = {Feb.},
  EDITOR = {Ernst Denert and Daniel Hoffman and Jochen Ludewig and
                  David Parnas},
  NUMBER = {230},
  KEY = {Dagstuhl},
  SERIES = {Dagstuhl-Seminar-Report, ISSN 0940-1121}
}


@INPROCEEDINGS{bre:dagstuhl-se-maintenance-noproc,
  AUTHOR = {Jan Bredereke and Karol Fr{\"u}hauf and Ridha Khedri and
                  Stefan Krau{\ss} and Andreas Zeller},
  TITLE = {Maintenance},
  PAGES = {41--43},
  BOOKTITLE = {Software Engineering Research and Education: Seeking a new
                  Agenda},
  YEAR = {1999},
  MONTH = {Feb.},
  EDITOR = {Ernst Denert and Daniel Hoffman and Jochen Ludewig and
                  David Parnas},
  NUMBER = {230},
  KEY = {Dagstuhl},
  SERIES = {Dagstuhl-Seminar-Report, ISSN 0940-1121}
}


@ARTICLE{bre:ieee-commag-maint-telsoft,
  AUTHOR = {Jan Bredereke},
  TITLE = {Maintaining Telephone Switching Software Requirements},
  JOURNAL = {IEEE Communications Magazine},
  YEAR = {1999},
  NOTE = {Submitted. An abstract is available
    {\url{http://csd.Informatik.Uni-Oldenburg.DE/~jan/abstracts/Bre99b.html}
      {here}}}
}


@ARTICLE{bre:change-tab-telsys,
  AUTHOR = {Jan Bredereke},
  TITLE = {Modular, Changeable Requirements in Functional
                  Documentation for Telephone Switching},
  JOURNAL = {Formal Methods in System Design},
  YEAR = {1999},
  NOTE = {Special issue on Tabular Notation. Submitted. 
    An extended abstract is available
   
{\url{http://csd.Informatik.Uni-Oldenburg.DE/~jan/abstracts/Bre99c.html}{here}}}
}


@INPROCEEDINGS{bre:dagstuhl-se-agenda,
  AUTHOR = {Jan Bredereke},
  TITLE = {Maintaining Telephone Switching System Requirements},
  BOOKTITLE = {Participants' notes of {Dagstuhl} seminar 99071 --
    software engineering research and education: seeking a new agenda},
  YEAR = {1999},
  MONTH = {15--19~Feb.}
}


@INPROCEEDINGS{cfhw99,
  AUTHOR = {Clemens Fischer and Heike Wehrheim},
  TITLE = {Model-Checking {CSP-OZ} Specifications with {FDR}},
  BOOKTITLE = {Proceedings of the 1st International Conference on
    Integrated Formal Methods (IFM)},
  EDITOR = {K. Araki and A. Galloway and K. Taguchi},
  YEAR = 1999,
  PAGES = {315--334},
  PUBLISHER = {Springer},
  ABSTRACT = {
    CSP-OZ is a formal method integrating two different specifications
    formalisms into one: the formalism Object-Z for the description of
    static aspects, and the process algebra CSP for the description of
    the dynamic behaviour of systems. The semantics of CSP-OZ is
    \emph{failure divergence} taken from the process algebra side. In
    this paper we propose a method for checking correctness of CSP-OZ
    specifications via a translation into the CSP dialect of the model
    checker FDR.
  },
  URL = {http://csd.informatik.uni-oldenburg.de/pub/Papers/cfhw99.ps.gz}
}


@INPROCEEDINGS{jt99,
  AUTHOR = {Josef Tapken},
  TITLE = {{Implementing Hierarchical Graph-Structures}},
  BOOKTITLE = {Proceedings of FASE'99},
  EDITOR = {J.-P. Finance},
  VOLUME = {1577},
  SERIES = {LNCS},
  PUBLISHER = {Springer-Verlag},
  YEAR = {1999},
  PAGES = {219--233},
  NOTE = {\copyright Springer-Verlag. This publication is available
    {\url{http://csd.informatik.uni-oldenburg.de/pub/Papers/jt99.ps.gz}{here}}
    and at
    {\url{http://www.springer.de/comp/lncs/index.html}{Springer}}}
}


@INPROCEEDINGS{fischer99:softwdevelobjeczcspjava,
  AUTHOR = {Clemens Fischer},
  TITLE = {Software Development with {Object-Z}, {CSP} and {Java}: A
                  Pragmatic Link from Formal Specifications to Programs},
  BOOKTITLE = {Formal Techniques for Java Programs},
  EDITOR = {B. Jacobs and B. Leavens and P. M\"uller and A.
                  Poetzsch-Heffter},
  VOLUME = 251,
  SERIES = {Technical Report},
  YEAR = 1999,
  PUBLISHER = {Fernuniversit{\"a}t Hagen},
  PAGES = {29--35},
  URL = {http://csd.informatik.uni-oldenburg.de/pub/Papers/cspoz2jass.ps.gz}
}


@ARTICLE{msero99,
  AUTHOR = {Michael Schenke and E.-R. Olderog},
  TITLE = {Transformational design of real-time systems -- Part 1:
                  from requirements to program specifications.},
  JOURNAL = {Acta Informatica 36},
  PAGES = {1-65},
  YEAR = {1999},
  URL = {http://csd.informatik.uni-oldenburg.de/pub/Papers/msero97_1.ps.gz}
}


@ARTICLE{ms99,
  AUTHOR = {Michael Schenke},
  TITLE = {Transformational design of real-time systems -- Part 2:
                  from program specifications to programs.},
  JOURNAL = {Acta Informatica 36},
  PAGES = {67-99},
  YEAR = {1999}
}


@ARTICLE{die99,
  AUTHOR = {H. Dierks},
  TITLE = {{Synthesizing Controllers from Real-Time Specifications}},
  JOURNAL = {IEEE Transactions on Computer-Aided Design of Integrated
                  Circu its and Systems},
  YEAR = {1999},
  VOLUME = {18},
  NUMBER = {1},
  PAGES = {33--43},
  URL = {http://csd.Informatik.Uni-Oldenburg.DE/~dierks/Berichte/TCAD.ps.gz}
}


@INPROCEEDINGS{bre:estelle98,
  AUTHOR = {Jan Bredereke},
  TITLE = {Specification Style and Efficiency in {E}stelle},
  PAGES = {165--186},
  BOOKTITLE = {Proc. of the 1st Int'l. Workshop on the Formal Description
    Technique {E}stelle -- {E}stelle'98},
  YEAR = {1998},
  EDITOR = {Stanislaw Budkowski and Stefan Fischer and Reinhard
Gotzhein},
  ADDRESS = {Evry, France},
  MONTH = {2~Nov.},
  ORGANIZATION = {Institut National des T{\'e}l{\'e}communications},
  URL = {http://csd.Informatik.Uni-Oldenburg.DE/~jan/papers/Bre98b.ps.gz}
}


@INPROCEEDINGS{ero98:formalmethodrealtimesystem,
  AUTHOR = {E.-R. Olderog},
  TITLE = {Formal Methods in Real-Time Systems},
  BOOKTITLE = {Proceedings of the 10th EuroMicro Workshop on Real Time
Systems},
  YEAR = 1998,
  ORGANIZATION = {IEEE Computer Society},
  MONTH = {June},
  PAGES = {254--263}
}


@INPROCEEDINGS{hd98c,
  AUTHOR = {H. Dierks and A. Fehnker and A. Mader and F.W. Vaandrager},
  TITLE = {{Operational and Logical Semantics for Polling Real-Time
Systems}},
  BOOKTITLE = {FTRTFT'98},
  SERIES = {Lecture Notes in Computer Science},
  YEAR = {1998},
  PUBLISHER = {Springer-Verlag},
  PAGES = {29--40},
  NOTE = {\copyright Springer-Verlag. This publication is available
   
{\url{http://csd.Informatik.Uni-Oldenburg.DE/~dierks/Berichte/FTRTFT98.ps.gz}{
here}}
    and at
    {\url{http://www.springer.de/comp/lncs/index.html}{Springer}}}
}


@INPROCEEDINGS{hd98a,
  AUTHOR = {H. Dierks},
  TITLE = {{Comparing Model-Checking and Logical Reasoning for
      Real-Time Systems}},
  BOOKTITLE = {ESSLLI'98},
  YEAR = {1998},
  MONTH = AUG,
  NOTE = {Workshop proceedings},
  URL = {http://csd.informatik.uni-oldenburg.de/pub/Papers/ESSLLI.ps.gz}
}


@PROCEEDINGS{all98,
  TITLE = {{Formal Techniques in Real-Time and Fault-Tolerant Systems}},
  YEAR = {1998},
  EDITOR = {A.P. Ravn and H. Rischel},
  VOLUME = {1486},
  SERIES = {Lecture Notes in Computer Science},
  PUBLISHER = {Springer-Verlag},
  ADDRESS = {Lyngby, Denmark},
  MONTH = SEP
}


@INPROCEEDINGS{jt98,
  AUTHOR = {J. Tapken},
  TITLE = {{Moby/PLC -- A Design Tool for Hierarchical Real-Time
Automata}},
  BOOKTITLE = {Proceedings of FASE'98},
  EDITOR = {E. Astesiano},
  VOLUME = {1382},
  SERIES = {LNCS},
  PUBLISHER = {Springer Verlag},
  YEAR = {1998},
  PAGES = {326-329},
}


@INPROCEEDINGS{jthd98,
  AUTHOR = {J. Tapken and H. Dierks},
  TITLE = {{Moby/PLC -- Graphical Development of PLC-Automata}},
  BOOKTITLE = {Proceedings of FTRTFT'98},
  EDITOR = {A.P. Ravn and H. Rischel},
  VOLUME = {1486},
  SERIES = {LNCS},
  PUBLISHER = {Springer Verlag},
  YEAR = {1998},
  PAGES = {311-314},
  NOTE = {\copyright Springer-Verlag. This publication is available
                 
{\url{http://csd.informatik.uni-oldenburg.de/pub/Papers/jthd98.ps.gz}{here}}
                  and at
                  {\url{http://www.springer.de/comp/lncs/index.html}{Springer}}},
}


@INPROCEEDINGS{fischer98:jawa,
  AUTHOR = {Clemens Fischer and D. Meemken},
  TITLE = {{JaWA}: {Java} with Assertions},
  BOOKTITLE = {Java-Informations-Tage},
  EDITOR = {C. H. Cap},
  SERIES = {Informatik aktuell},
  YEAR = 1998,
  PUBLISHER = {Springer},
  PAGES = {49-59},
  NOTE = {In german.},
  ABSTRACT = {
     Methoden zur Entwicklung von korrekter Software und deren
     Einf\"uhrung in die Praxis stellen heute immer noch ein
     schwieriges Problem dar.

     Bertrand Meyer hat unter dem Stichwort 'Programmieren mit
     Vertrag' einen Vorschlag gemacht und durch Eiffel implementiert,
     wie man formale Spezifikationsanteile mit Programmcode mischen
     und zur Laufzeit \"uberpr\"ufen kann.

     In diesem Paper geben wir einen \"Uberblick \"uber die Sprache
     JaWA, mit der dieses Konzept auf Java \"ubertragen wurde. 

     JaWA Programme bestehen aus herk\"ommlichem Java-Code, der
     Zusicherungen (Invarianten, Vor- und Nachbedingungen) in Form von
     Kommentaren enth\"alt. Der JaWA-Pr\"acompiler \"ubersetzt JaWA in
     Java. Er erzeugt zus\"atzliche Bedingungen, mit denen die
     spezifizierten Eigenschaften zur Laufzeit \"uberpr\"uft werden
     k\"onnen. Dabei wird die Java Ausnahmebehandlung ausgenutzt und
     um Eiffel \"ahnliche `rescue' und `retry' Anweisungen
     erg\"anzt. Die erzeugten Fehlermeldungen und Warnungen sind frei
     konfigurierbar.
  }
}


@INPROCEEDINGS{fischer98:howzprocesalgeb,
  AUTHOR = {Clemens Fischer},
  TITLE = {How to combine {Z} with a Process Algebra},
  BOOKTITLE = {{ZUM'98} The {Z} Formal Specification Notation},
  EDITOR = {J. Bowen and A. Fett and M. Hinchey},
  VOLUME = {1493 },
  PAGES = {5-23},
  SERIES = {LNCS},
  YEAR = 1998,
  PUBLISHER = {Springer},
  ABSTRACT = {
     The specification language Z has been designed to describe data
     and functional aspects of systems, but it does not define a
     semantics for specifications in a distributed setting. Process
     algebras, on the other hand, concentrate on the behaviour of
     communicating agents. For this reason the combination of Z with a
     process algebra recently got a lot of attention. In this paper we
     summarise and categorise the different approaches and identify
     pitfalls and shortcomings in existing combinations.  Thereby we
     give an overview over the many possible answers to the question:
     `What is the behavioural semantics of a Z specification?'
  }
}


@INPROCEEDINGS{sk98,
  AUTHOR = {S. Kleuker},
  TITLE = {Reengineering of Distributed Systems using Formal Methods},
  BOOKTITLE = {Proceedings of the Second Euromicro Conference on Software
    Maintenance and Reengineering},
  EDITOR = {P. Nesi and F. Lehner},
  PUBLISHER = {IEEE Computer Society},
  YEAR = 1998,
  PAGES = {189-192},
}


@INPROCEEDINGS{hdms98,
  AUTHOR = {H. Dierks and M. Schenke},
  TITLE = {{A Unifying Framework for Correct Program Construction}},
  BOOKTITLE = {Mathematics of Program Construction 98},
  EDITOR = {J. Jeuring},
  VOLUME = {1422},
  SERIES = {Lecture Notes in Computer Science},
  YEAR = {1998},
  PUBLISHER = {Springer-Verlag},
  MONTH = JUN,
  PAGES = {122--150},
  NOTE = {\copyright Springer-Verlag. This publication is available
    {\url{http://csd.informatik.uni-oldenburg.de/pub/Papers/MPC.ps.gz}{here}}
    and at
    {\url{http://www.springer.de/comp/lncs/index.html}{Springer}}}
}


@INPROCEEDINGS{hdjt98,
  AUTHOR = {H. Dierks and J. Tapken},
  TITLE = {{Tool-Supported Hierarchical Design of Distributed
                  Real-Time Systems}},
  BOOKTITLE = {Euromicro Workshop on Real Time Systems},
  PUBLISHER = {IEEE},
  YEAR = {1998},
  PAGES = {222-229},
  URL = {http://csd.informatik.uni-oldenburg.de/pub/Papers/hdjt98.ps.gz}
}


@INPROCEEDINGS{erohd98,
  AUTHOR = {E.-R. Olderog and H. Dierks},
  TITLE = {{Decomposing Real-Time Specifications}},
  BOOKTITLE = {{Compositionality: The Significant Difference}},
  EDITOR = {H. Langmaack and A. Pnueli and W.P. de Roever},
  VOLUME = {1536},
  SERIES = {Lecture Notes in Computer Science},
  YEAR = {1998},
  PUBLISHER = {Springer-Verlag},
  PAGES = {465--489},
  NOTE = {{\url{http://csd.informatik.uni-oldenburg.de/pub/Papers/erohd97.ps.gz}
      {An abstract is available on-line}}}
}