Publications 1995-1997

 

5 Publications 1995-1997 (BibTeX Source)

@MISC{msmd97,
  AUTHOR = {Michael Schenke and Michael Dossis},
  TITLE = {Provably Correct Hardware Compilation using Timing Diagrams},
  NOTE = {Submitted. This publication is available on-line in two
    parts.
\url{http://csd.informatik.uni-oldenburg.de/pub/Papers/msmd97-p1.ps.gz}{Part 1},
    \url{http://csd.informatik.uni-oldenburg.de/pub/Papers/msmd97-p2.ps.gz}{Part
2}.},
  YEAR = {1997}
}


@UNPUBLISHED{ms97-habil,
  AUTHOR = {Michael Schenke},
  TITLE = {Development of Correct Real-Time Systems by Refinement},
  NOTE = {Habilitationsschrift.},
  URL = {http://csd.informatik.uni-oldenburg.de/pub/Papers/ms97-habil.ps.gz},
  YEAR = {1997}
}


@INPROCEEDINGS{jt97-ess,
  AUTHOR = {Josef Tapken},
  TITLE = {{Interactive and Compilative Simulation of PLC-Automata}},
  BOOKTITLE = {Simulation in Industry, ESS'97},
  EDITOR = {Winfried Hahn and Axel Lehmann},
  PUBLISHER = {Society for Computer Simulation},
  YEAR = 1997,
  PAGES = {552--556},
  URL = {http://csd.informatik.uni-oldenburg.de/pub/Papers/jt97-ess.ps.gz}
}


@INPROCEEDINGS{sk97-fme,
  AUTHOR = {Stephan Kleuker},
  TITLE = {Formalizing Requirements for Distributed Systems with Trace
Diagrams},
  BOOKTITLE = {Formal Methods: Their Industrial Application and 
    Strengthened Foundations (FME'97)},
  EDITOR = {J. Fitzgerald and C.B. Jones and P. Lucas},
  PUBLISHER = {Springer-Verlag},
  SERIES = {Lecture Notes in Computer Science},
  VOLUME = 1313,
  YEAR = 1997,
  PAGES = {102--121},
  URL = {http://csd.informatik.uni-oldenburg.de/pub/Papers/sk97-fme.ps.gz},
}


@INPROCEEDINGS{cfgs97,
  AUTHOR = {Clemens Fischer and Graeme Smith},
  TITLE = {Combining {CSP} and {Object-Z}: Finite or Infinite
                  Trace-Semantics?},
  BOOKTITLE = {Proceedings of FORTE/PSTV'97},
  PUBLISHER = {Chapmann \& Hall},
  EDITOR = {T. Mizuno and N. Shiratori and T. Higashino and A.
                  Togashi},
  PAGES = {503 - 518},
  NOTE = {\url{http://csd.informatik.uni-oldenburg.de/pub/Papers/cfgs97-a.ps}
    {An abstract is available on-line}},
  YEAR = 1997
}


@INPROCEEDINGS{cd97,
  AUTHOR = {Cheryl Dietz},
  TITLE = {{Action Diagrams}},
  BOOKTITLE = {Proceedings of the IFAC/IFIP Workshop, Lyon, France, 15-17
                  September 1997},
  EDITOR = {Mathieu Maranzana},
  VOLUME = {Real-Time Programming 1997},
  PAGES = {},
  ADDRESS = {},
  SERIES = {},
  PUBLISHER = {Elsevier Science 1998},
  COMMENTS = {},
  MONTH = {},
  ORGANIZATION = {},
  YEAR = {1997},
  NOTE = {\url{http://csd.informatik.uni-oldenburg.de/pub/Papers/cd97-a.ps.gz}
    {An abstract is available on-line}}
}


@ARTICLE{cfskero97,
  AUTHOR = {C. Fischer and S. Kleuker and E.-R. Olderog},
  TITLE = {{B}eweisbar korrekte {T}elekommunikationssysteme},
  JOURNAL = {Informationstechnik und Technische Informatik},
  YEAR = 1997,
  VOLUME = 3,
  PAGES = {22--28},
  NOTE = {\url{http://csd.informatik.uni-oldenburg.de/pub/Papers/cfskero97-a.ps.gz}
    {An extended abstract is available on-line}},
}


@INPROCEEDINGS{cf97-gi,
  AUTHOR = {Clemens Fischer},
  TITLE = {Combining {Object-Z} and {CSP}},
  BOOKTITLE = {Formale Beschreibungstechniken f{\"u}r verteilte Systeme,
                  GI/ITG-Fachgespr\"ach, 19.-20. Juni 1997 in Berlin},
  EDITOR = {A. Wolisz and I. Schieferdecker and A. Rennoch},
  PUBLISHER = {GMD-Forschungszentrum Informationstechnik GMBH},
  SERIES = {GMD-Studien},
  NUMBER = 315,
  YEAR = 1997,
  PAGES = {119--128},
  NOTE = {\url{http://csd.informatik.uni-oldenburg.de/pub/Papers/cf97-gi-a.ps.gz}
    {An abstract is available on-line}}
}


@INPROCEEDINGS{sk97-gi,
  AUTHOR = {Stephan Kleuker},
  TITLE = {{A}nforderungsformalisierung f{\"u}r synchron
                  kommunizierende {P}rozesse mit {T}race-{D}iagrammen},
  BOOKTITLE = {Formale Beschreibungstechniken f{\"u}r verteilte Systeme,
                  GI/ITG-Fachgespr\"ach, 19.-20. Juni 1997 in Berlin},
  EDITOR = {A. Wolisz and I. Schieferdecker and A. Rennoch},
  PUBLISHER = {GMD-Forschungszentrum Informationstechnik GMBH},
  SERIES = {GMD-Studien},
  VOLUME = 315,
  YEAR = 1997,
  PAGES = {175--184},
  URL = {http://csd.informatik.uni-oldenburg.de/pub/Papers/sk97-gi.ps.gz},
}


@INPROCEEDINGS{hfjt97,
  AUTHOR = {Hans Fleischhack and Josef Tapken},
  TITLE = {An {M-Net} Semantics for a Real-Time Extension of
{$\mu$SDL}},
  BOOKTITLE = {Formal Methods: Their Industrial Application and
    Strengthened Foundations (FME'97)},
  PUBLISHER = {Springer-Verlag},
  SERIES = {Lecture Notes in Computer Science},
  VOLUME = 1313,
  YEAR = 1997,
  PAGES = {162--181},
  URL = {http://csd.informatik.uni-oldenburg.de/pub/Papers/hfjt97.ps.gz}
}


@INPROCEEDINGS{hdcd97,
  AUTHOR = {Henning Dierks and Cheryl Dietz},
  TITLE = {{Graphical Specification and Reasoning: Case Study
      "Generalized Railroad Crossing"}},
  BOOKTITLE = {FME'97},
  EDITOR = {J. Fitzgerald and C.B. Jones and P. Lucas},
  VOLUME = 1313,
  SERIES = {Lecture Notes in Computer Science},
  YEAR = 1997,
  PUBLISHER = {Springer-Verlag},
  PAGES = {20--39},
  URL = {http://csd.informatik.uni-oldenburg.de/pub/Papers/hdcd97-fme.ps.gz}
}


@INPROCEEDINGS{hd97-isss,
  AUTHOR = {Henning Dierks},
  TITLE = {{Synthesising Controllers from Real-Time Specifications}},
  BOOKTITLE = {{Tenth International Symposium on System Synthesis}},
  YEAR = {1997},
  PUBLISHER = {IEEE CS Press},
  OPTMONTH = SEP,
  PAGES = {126--133},
  URL = {http://csd.informatik.uni-oldenburg.de/pub/Papers/hd97-isss.ps.gz}
}


@INPROCEEDINGS{sk97-tacas,
  AUTHOR = {Stephan Kleuker},
  TITLE = {Incremental Development of Deadlock-Free Communicating
Systems},
  BOOKTITLE = {Proceedings of the Third International Workshop Tools and
    Algorithms for the Construction and Analysis of Systems (TACAS'97)},
  EDITOR = {E. Brinksma},
  PUBLISHER = {Springer-Verlag},
  SERIES = {Lecture Notes in Computer Science},
  VOLUME = {1217},
  YEAR = 1997,
  PAGES = {306--320},
  ABSTRACT = {
    A basic property which distributed communicating systems have to
    fulfill is deadlock-freedom. For systems consisting of the
    parallel composition of subsystems it is complex to check
    deadlock-freedom because the global state space of the composition
    has to be investigated.
    
    This paper presents an approach by which the absence of deadlocks
    is preserved during the development. Small initial deadlock-free
    systems are stepwise extended with new functionalities to large
    complex systems by transformation rules which preserve
    deadlock-freedom.  Systems are represented by finite automata
    extended with arbitrary local variables. A verification rule is
    presented which ensures that the parallel composition of such
    extended automata is deadlock-free. The advantage of this rule is
    that only information over pairs of connected subsystems is needed
    and not over the complete state space.
  },
  URL = {http://csd.informatik.uni-oldenburg.de/pub/Papers/sk97-tacas.ps.gz}
}


@INPROCEEDINGS{cf97,
  AUTHOR = {Clemens Fischer},
  TITLE = {{CSP-OZ}: A Combination of {Object-Z} and {CSP}},
  BOOKTITLE = {Formal Methods for Open Object-Based Distributed Systems
                  (FMOODS '97)},
  YEAR = 1997,
  VOLUME = 2,
  EDITOR = {H. Bowmann and J. Derrick},
  PUBLISHER = {Chapman \& Hall},
  PAGES = {423--438},
    {An abstract is available on-line}},
  ABSTRACT = {
    In this paper we define a combination of Object-Z and CSP called
    CSP-OZ. The basic idea is to define a CSP-semantics for every
    Object-Z class. Special care is taken to capture the
    characteristics of input and output parameters properly and to
    preserve the expected refinement rules. CSP-OZ is well suited for
    the specification and development of communicating distributed
    systems. It provides powerful techniques to model data- and
    control-aspects in a common framework. The language is easy to use
    for Z and Object-Z users.  
  }
}


@INPROCEEDINGS{hd97-arts,
  AUTHOR = {Henning Dierks},
  TITLE = {{PLC-Automata: A New Class of Implementable Real-Time
                  Automata}},
  BOOKTITLE = {Transformation-Based Reactive Systems Development
                  (ARTS'97)},
  EDITOR = {M. Bertran and T. Rus},
  SERIES = {Lecture Notes in Computer Science},
  VOLUME = {1231},
  YEAR = {1997},
  PUBLISHER = {Springer-Verlag},
  PAGES = {111--125},
  URL = {http://csd.informatik.uni-oldenburg.de/pub/Papers/hd97-arts.ps.gz}
}


@BOOK{ero97-verification,
  AUTHOR = {K.-R. Apt and E.-R. Olderog},
  TITLE = {Verification of Sequential and Concurrent Programs.},
  EDITION = {2nd},
  PUBLISHER = {Springer-Verlag},
  YEAR = 1997,
  NOTE = {ISBN 0-387-94896-1. 
    \url{http://www.springer-ny.com/catalog/np/mar97np/DATA/0-387-94896-1.html}
    {This book in the Springer catalogue}.
   
\url{
http://csd.informatik.uni-oldenburg.de/pub/Papers/ero97-verification-a.ps.gz}
    {More Information}.
  }
}


@INPROCEEDINGS{sk96-forte,
  AUTHOR = {Stephan Kleuker},
  TITLE = {Using Formal Methods in the Development of Protocols for
    Multi-User Multimedia Systems},
  BOOKTITLE = {Proceedings of the 9th international conference on Formal
    Description Techniques (FORTE'96) (Kaiserslautern, Germany)},
  EDITOR = {R. Gotzhein and J. Bredereke},
  YEAR = 1996,
  PUBLISHER = {Chapman \& Hall},
  PAGES = {113--128}
}


@INPROCEEDINGS{hd96,
  AUTHOR = {Henning Dierks},
  TITLE = {The Production Cell: A Verified Real-Time System},
  BOOKTITLE = {Formal Techniques in Real-Time and Fault-Tolerant Systems
    (FTRTFT'96) (Uppsala, Sweden)},
  EDITOR = {B. Jonsson and J. Parrow},
  VOLUME = {1135},
  SERIES = {Lecture Notes in Computer Science},
  PUBLISHER = {Springer-Verlag},
  YEAR = 1996,
  PAGES = {208--227},
  URL = {http://csd.informatik.uni-oldenburg.de/pub/Papers/FTRTFT96.ps.gz}
}


@INPROCEEDINGS{cd96,
  AUTHOR = {Cheryl Dietz},
  TITLE = {Graphical Formalization of Real-Time Requirements},
  BOOKTITLE = {Formal Techniques in Real-Time and Fault-Tolerant Systems
    (FTRTFT'96) (Uppsala, Sweden)},
  EDITOR = {B. Jonsson and J. Parrow},
  VOLUME = {1135},
  SERIES = {Lecture Notes in Computer Science},
  PUBLISHER = {Springer-Verlag},
  YEAR = 1996,
  PAGES = {366--385},
  NOTE = {\url{http://csd.informatik.uni-oldenburg.de/pub/Papers/cd96-ea.ps.gz}
    {An extended abstract is available on-line}}
}


@INPROCEEDINGS{cfwj96,
  AUTHOR = {Clemens Fischer and Wil Janssen},
  TITLE = {Synchronous Development of Asynchronous Systems},
  BOOKTITLE = {Proceedings of CONCUR'96},
  EDITOR = {Ugo Montanari and Vladimiro Sassone},
  VOLUME = {1119},
  SERIES = {Lecture Notes in Computer Science},
  PUBLISHER = {Springer-Verlag},
  YEAR = 1996,
  PAGES = {735--750},
  NOTE = {\url{http://csd.informatik.uni-oldenburg.de/pub/CoCoN/cfwj96-a.ps.gz}
    {An abstract is available on-line}}
}


@INCOLLECTION{ero96,
  AUTHOR = {E.-R. Olderog and A. P. Ravn and J. U. Skakkeb{\ae}k},
  TITLE = {Refining System Requirements to Program Specifications},
  EDITOR = {C. Heitmeyer and D. Mandrioli},
  BOOKTITLE = {Formal Methods for Real-Time Computing},
  CHAPTER = 5,
  PAGES = {107--134},
  PUBLISHER = {Wiley},
  SERIES = {Trends in Software},
  VOLUME = 5,
  YEAR = 1996,
  NOTE = {\url{http://csd.informatik.uni-oldenburg.de/pub/Papers/ero96.ps.gz}
    {An abstract is available on-line}}
}


@INPROCEEDINGS{jbwj96,
  AUTHOR = { J{\"u}rgen Bohn and Wil Janssen },
  TITLE = { A Strategic Approach to Transformational Design },
  BOOKTITLE = {Industrial Benefit and Advances in Formal Methods (FME'96)},
  VOLUME = 1051,
  PAGES = {609--628},
  SERIES = {Lecture Notes in Computer Science},
  PUBLISHER = {Springer-Verlag},
  YEAR = 1996,
  URL = {http://csd.informatik.uni-oldenburg.de/pub/Papers/jbwj96-fme.ps.gz}
}


@INPROCEEDINGS{sk96-ain,
  AUTHOR = {Stephan Kleuker},
  TITLE = {The Extension of Existing Telecommunication Software with
                  new Services Using Formal Methods},
  EDITOR = {T. Margaria},
  BOOKTITLE = {Proceedings of the International Workshop on Advanced
                  Intelligent Networks},
  PUBLISHER = {University of Passau},
  YEAR = 1996,
  PAGES = {91--106},
  URL = {http://csd.informatik.uni-oldenburg.de/pub/CoCoN/sk96-ain.ps.gz},
  ABSTRACT = {
    Software development based on formal methods is a rigorous
    approach to provably correct software. A problem is that for most
    industrial applications the system development never terminates
    because requirements change and new functionality has to be added
    to the system. One typical example are telecommunication systems
    with a permanently increasing number of new services that have to
    be supported. Therefore the formal development of extensible and
    correct specifications becomes more and more important.  But
    extensibility is not treated in formal methods so far.  This paper
    describes an approach for the development of extensible
    specifications in small intuitive steps for communication networks
    at different levels of abstraction.
  }
}


@INPROCEEDINGS{sk96-fme,
  AUTHOR = {S. Kleuker and H. Tjabben},
  TITLE = {The Incremental Development of Correct Specifications for
                  Distributed Systems},
  EDITOR = {M.-C. Gaudel and J. Woodcock},
  BOOKTITLE = {Industrial Benefit and Advances in Formal Methods
                  (FME'96)},
  PUBLISHER = {Springer-Verlag},
  SERIES = {Lecture Notes in Computer Science},
  VOLUME = 1051,
  YEAR = 1996,
  PAGES = {479--498},
  URL = {http://csd.informatik.uni-oldenburg.de/pub/CoCoN/sk96-fme.ps.gz},
  ABSTRACT = {
    Provably correct software can only be achieved by basing the
    development process on formal methods. For most industrial
    applications such a development never terminates because
    requirements change and new functionality has to be added to the
    system. Therefore a formal method that supports an incremental
    development of complex systems is required. The project CoCoN
    (Provably Correct Communication Networks) that is carried out
    jointly between Philips Research Laboratories Aachen and the
    University of Oldenburg takes results from the ESPRIT Basic
    Research Action ProCoS to show the applicability of a more formal
    approach to the development of correct telecommunications
    software. These ProCoS-methods have been adapted to support the
    development of extensible specifications for distributed systems.
    Throughout this paper our approach is exemplified by a case study
    how call handling software for telecommunication switching systems
    should be developed.
  }
}


@INPROCEEDINGS{ms96,
  AUTHOR = {Michael Schenke and A. P. Ravn},
  TITLE = {Refinement from a control problem to programs},
  BOOKTITLE = {Formal methods for industrial applications: specifying and
    programming the steam boiler control},
  EDITOR = {Jean-Raymond Abrial and Egon Borger and Hans Langmaack},
  VOLUME = 1165,
  SERIES = {Lecture Notes in Computer Science},
  YEAR = 1996,
  PUBLISHER = {Springer-Verlag},
  PAGES = {403--427},
  URL = {http://csd.informatik.uni-oldenburg.de/pub/Papers/ms96.ps.gz}
}


@INPROCEEDINGS{ebhf95-lncs,
  EDITOR = {Giorgio De Michelis and Michel Diaz},
  BOOKTITLE = {Proceedings of the 16th Internationcal Conference on
  Application and Theory of Petri nets (Turin, Italy, June 26--30, 1995)},
  AUTHOR = {E. Best and Hans Fleischack and W. Fraczak and R. P.
Hopkins},
  TITLE = {A Class of Composable High Level {Petri} Nets with an
    Application to the Semantics of {B(PN)$^2$}},
  SERIES = {Lecture Notes in Computer Science},
  VOLUME = {935},
  PUBLISHER = {Springer-Verlag},
  PAGES = {103--118},
  YEAR = {1995}
}


@INPROCEEDINGS{aghf95,
  EDITOR = {Horst Reichel},
  BOOKTITLE = {Proceedings on the 10th International Conference on
    Fundamentals of computation theory ({FCT}'95) (Dresden,
    Germany, August 1995)},
  AUTHOR = {A. Gronewold and Hans Fleischhack},
  TITLE = {Computing {Petri} Net Languages by Reductions},
  SERIES = {Lecture Notes in Computer Science},
  VOLUME = {965},
  PAGES = {253--???{}},
  YEAR = {1995},
  PUBLISHER = {Springer-Verlag}
}


@INPROCEEDINGS{ebhf95-wics,
  AUTHOR = {Eike Best and Hans Fleischhack and W. Fraczak and R. P.
    Hopkins and H. Klaudel and E. Pelz},
  TITLE = {An {M-Net} semantics of {B(PN)$^2$}.},
  EDITOR = {J. Desel},
  BOOKTITLE = {Structures in Concurrency Theory},
  PUBLISHER = {Springer-Verlag},
  SERIES = {Workshops in Computing},
  YEAR = 1995
}


@INPROCEEDINGS{hfjt95,
  AUTHOR = {Hans Fleischhack and Josef Tapken},
  TITLE = {Eine kompositionelle {P}etrinetz-{S}emantik f\"ur
    {SDL}-{S}pezifikationen},
  BOOKTITLE = {2. Workshop Algorithmen und Werkzeuge f\"ur Petrinetze},
  EDITOR = {J. Desel and Hans Fleischhack and A. Oberweis and Michael
    Sonnenschein},
  NUMBER = {22},
  SERIES = {AIS reports},
  YEAR = 1995,
  ORGANIZATION = {Fachbereich Informatik},
  PUBLISHER = {Universit\"at Oldenburg}
}


@INPROCEEDINGS{eroms95,
  AUTHOR = {E.-R. Olderog and M. Schenke},
  TITLE = {Design of Real-Time Systems: The Interface between
    Duration Calculus and Program Specifications},
  EDITOR = {J. Desel},
  BOOKTITLE = {Structures in Concurrency Theory},
  PUBLISHER = {Springer-Verlag},
  SERIES = {Workshops in Computing},
  YEAR = 1995,
  PAGES = {32--54},
  URL = {http://csd.informatik.uni-oldenburg.de/pub/Papers/eroms95.ps.gz}
}


@ARTICLE{jbhh95,
  AUTHOR = { J{\"u}rgen Bohn and Hardi Hungar },
  TITLE = { Traverdi -- Transformation and Verification of Distributed
Systems },
  JOURNAL = {Lecture Notes in Computer Science},
  PAGES = {317--???{}},
  EDITOR = { M. Broy and S. J\"anichen },
  PUBLISHER = {Springer-Verlag},
  VOLUME = 1009,
  YEAR = 1995
}


@INPROCEEDINGS{jbsr95-tacas,
  AUTHOR = {J{\"u}rgen Bohn and Stephan R{\"o}ssig},
  TITLE = {On Automatic and Interactive Design of Communicating
Systems},
  EDITOR = {E. Brinksma and W. R. Cleaveland and K. G. Larsen and T.
    Margaria and B. Steffen},
  BOOKTITLE = {Proceedings of the 1st International Workshop on Tools and
    Algorithms for the Construction and Analysis of Systems (TACAS'95) (Aarhus,
Denmark)},
  SERIES = {Lecture Notes in Computer Science},
  VOLUME = 1019,
  PAGES = {216--237},
  PUBLISHER = {Springer-Verlag},
  YEAR = 1995,
  ABSTRACT = {
    The design of provable correct software requires formal methods
    whose usage should be assisted by suitable tools.  Following a
    transformational approach the design needs interactive user help
    when important design decisions have to be made. Nevertheless
    simple parts should be automated as far as possible. Ideally the
    user only guides the design process by indicating the design ideas
    which are then carried out automatically. Typically sequential
    implementations are more appropriate for automation while
    parallelization needs interaction to determine the intended
    program architecture.\bibpar This paper presents a
    transformational approach to the design of distributed systems
    where environment and concurrently running components communicate
    via synchronous message passing along directed channels. System
    specifications that combine trace-based with state-based reasoning
    are gradually modified by application of transfromation rules
    until Occam-like programs are achieved finally. We consider
    interactive and automatic aspects of such a design process and
    illustrate our approach by sketching the development of a shared
    register implementation.
  }
}


@INPROCEEDINGS{sk95-gi,
  AUTHOR = {S. Kleuker and H. Tjabben},
  TITLE = {A Formal Approach to the Development of Reliable
    Multi-User Multimedia Applications },
  EDITOR = {R. Gotzhein and J. Bredereke },
  BOOKTITLE = {Proceedings of the 5th GI/ITG-Fachgespr\"ach ``Formale
    Beschreibungs\-techniken f\"ur verteilte Systeme'' },
  PUBLISHER = {University of Kaiserslautern, Department of Computer
Science},
  YEAR = 1995,
  PAGES = {1--10},
  URL = {http://csd.informatik.uni-oldenburg.de/pub/CoCoN/sk95-gi.ps.gz},
  ABSTRACT = {
    Multi-user multimedia communication systems allow users at
    different sides to exchange any kind of information (video, audio
    and data) in a multipoint call. We expect that these systems will
    at first be used in professional areas like hospitals. The medical
    area poses strong requirements on the reliability and security of
    the application software.  This paper presents an approach how
    formal methods can help to meet these requirements.
  },
}


@INPROCEEDINGS{sk95-ieee,
  AUTHOR = {H. Tjabben and S. Kleuker and A. Kehne},
  TITLE = {Provably Correct Intelligent Networks},
  BOOKTITLE = {Proceedings of the IEEE Intelligent Network '95 Workshop,
    May 9-11, 1995, Ottawa, Canada },
  YEAR = 1995,
  URL = {http://csd.informatik.uni-oldenburg.de/pub/CoCoN/sk95-ieee.ps.gz}
}


@INPROCEEDINGS{sk95-tapsoft,
  AUTHOR = {S. Kleuker},
  TITLE = {A Gentle Introduction to Specification Engineering using a
                  Case Study in Telecommunications},
  EDITOR = {P. D. Mosses and M. Nielsen and M. I. Schwartzbach},
  BOOKTITLE = {International Joint Conference on Theory and Practice of
                  Software Development (TAPSOFT'95)},
  PUBLISHER = {Springer-Verlag},
  SERIES = {Lecture Notes in Computer Science},
  VOLUME = 915,
  YEAR = 1995,
  PAGES = {636--650},
  URL = {http://csd.informatik.uni-oldenburg.de/pub/CoCoN/sk95-tapsoft.ps.gz},
  ABSTRACT = {
    Software development based on formal methods is the only way to
    provably correct software. Therefore a method for the development
    of complex systems in intuitive steps is needed. A suitable
    solution is the transformational approach where verified
    semantics-preserving transformation rules are used to come from a
    first verified specification to the desired system. A problem is
    that for most industrial applications the system development never
    terminates because requirements change and new functionalities
    have to be added to the system.
    
    This paper describes a new approach for the development of
    extensible specifications in small intuitive steps. New
    transformation rules are introduced that guarantee that
    intermediate results of development can be used for further
    steps.
  }
}


@MASTERSTHESIS{rm95,
  AUTHOR = {R. M\"uller},
  TITLE = {{A}n\-forderungs\-ger\-echte {S}pez\-ifika\-tion eines
    zeit\-ab\-h\"an\-gigen {G}eb\"uh\-renab\-rech\-nungs\-systems},
  SCHOOL = {University of Oldenburg, Department of Computer Science, Oldenburg, Germany},
  MONTH = APR,
  YEAR = 1995
}