Publications 1995-1997

 

5 Publications 1995-1997 (with Abstracts)

[SD97]

Michael Schenke and Michael Dossis. Provably correct hardware compilation using timing diagrams, 1997. Submitted. This publication is available on-line in two parts. Part 1, Part 2.
[ bib ]

[Sch97]

Michael Schenke. Development of correct real-time systems by refinement. Habilitationsschrift., 1997.
[ bib | .ps.gz ]

[Tap97]

Josef Tapken. Interactive and Compilative Simulation of PLC-Automata. In Winfried Hahn and Axel Lehmann, editors, Simulation in Industry, ESS'97, pages 552-556. Society for Computer Simulation, 1997.
[ bib | .ps.gz ]

[Kle97b]

Stephan Kleuker. Formalizing requirements for distributed systems with trace diagrams. In J. Fitzgerald, C.B. Jones, and P. Lucas, editors, Formal Methods: Their Industrial Application and Strengthened Foundations (FME'97), volume 1313 of Lecture Notes in Computer Science, pages 102-121. Springer-Verlag, 1997.
[ bib | .ps.gz ]

[FS97]

Clemens Fischer and Graeme Smith. Combining CSP and Object-Z: Finite or infinite trace-semantics? In T. Mizuno, N. Shiratori, T. Higashino, and A. Togashi, editors, Proceedings of FORTE/PSTV'97, pages 503 - 518. Chapmann & Hall, 1997. An abstract is available on-line.
[ bib ]

[Die97c]

Cheryl Dietz. Action Diagrams. In Mathieu Maranzana, editor, Proceedings of the IFAC/IFIP Workshop, Lyon, France, 15-17 September 1997, volume Real-Time Programming 1997. Elsevier Science 1998, 1997. An abstract is available on-line.
[ bib ]

[FKO97]

C. Fischer, S. Kleuker, and E.-R. Olderog. Beweisbar korrekte Telekommunikationssysteme. Informationstechnik und Technische Informatik, 3:22-28, 1997. An extended abstract is available on-line.
[ bib ]

[Fis97a]

Clemens Fischer. Combining Object-Z and CSP. In A. Wolisz, I. Schieferdecker, and A. Rennoch, editors, Formale Beschreibungstechniken für verteilte Systeme, GI/ITG-Fachgespräch, 19.-20. Juni 1997 in Berlin, number 315 in GMD-Studien, pages 119-128. GMD-Forschungszentrum Informationstechnik GMBH, 1997. An abstract is available on-line.
[ bib ]

[Kle97a]

Stephan Kleuker. Anforderungsformalisierung für synchron kommunizierende Prozesse mit Trace-Diagrammen. In A. Wolisz, I. Schieferdecker, and A. Rennoch, editors, Formale Beschreibungstechniken für verteilte Systeme, GI/ITG-Fachgespräch, 19.-20. Juni 1997 in Berlin, volume 315 of GMD-Studien, pages 175-184. GMD-Forschungszentrum Informationstechnik GMBH, 1997.
[ bib | .ps.gz ]

[FT97]

Hans Fleischhack and Josef Tapken. An M-Net semantics for a real-time extension of muSDL. In Formal Methods: Their Industrial Application and Strengthened Foundations (FME'97), volume 1313 of Lecture Notes in Computer Science, pages 162-181. Springer-Verlag, 1997.
[ bib | .ps.gz ]

[DD97]

Henning Dierks and Cheryl Dietz. Graphical Specification and Reasoning: Case Study Generalized Railroad Crossing. In J. Fitzgerald, C.B. Jones, and P. Lucas, editors, FME'97, volume 1313 of Lecture Notes in Computer Science, pages 20-39. Springer-Verlag, 1997.
[ bib | .ps.gz ]

[Die97b]

Henning Dierks. Synthesising Controllers from Real-Time Specifications. In Tenth International Symposium on System Synthesis, pages 126-133. IEEE CS Press, 1997.
[ bib | .ps.gz ]

[Kle97c]

Stephan Kleuker. Incremental development of deadlock-free communicating systems. In E. Brinksma, editor, Proceedings of the Third International Workshop Tools and Algorithms for the Construction and Analysis of Systems (TACAS'97), volume 1217 of Lecture Notes in Computer Science, pages 306-320. Springer-Verlag, 1997.
[ bib | .ps.gz ]

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.

[Fis97b]

Clemens Fischer. CSP-OZ: A combination of Object-Z and CSP. In H. Bowmann and J. Derrick, editors, Formal Methods for Open Object-Based Distributed Systems (FMOODS '97), volume 2, pages 423-438. Chapman & Hall, 1997.
[ bib ]

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.

[Die97a]

Henning Dierks. PLC-Automata: A New Class of Implementable Real-Time Automata. In M. Bertran and T. Rus, editors, Transformation-Based Reactive Systems Development (ARTS'97), volume 1231 of Lecture Notes in Computer Science, pages 111-125. Springer-Verlag, 1997.
[ bib | .ps.gz ]

[AO97]

K.-R. Apt and E.-R. Olderog. Verification of Sequential and Concurrent Programs. Springer-Verlag, 2nd edition, 1997. ISBN 0-387-94896-1. This book in the Springer catalogue. More Information.
[ bib ]

[Kle96b]

Stephan Kleuker. Using formal methods in the development of protocols for multi-user multimedia systems. In R. Gotzhein and J. Bredereke, editors, Proceedings of the 9th international conference on Formal Description Techniques (FORTE'96) (Kaiserslautern, Germany), pages 113-128. Chapman & Hall, 1996.
[ bib ]

[Die96a]

Henning Dierks. The production cell: A verified real-time system. In B. Jonsson and J. Parrow, editors, Formal Techniques in Real-Time and Fault-Tolerant Systems (FTRTFT'96) (Uppsala, Sweden), volume 1135 of Lecture Notes in Computer Science, pages 208-227. Springer-Verlag, 1996.
[ bib | .ps.gz ]

[Die96b]

Cheryl Dietz. Graphical formalization of real-time requirements. In B. Jonsson and J. Parrow, editors, Formal Techniques in Real-Time and Fault-Tolerant Systems (FTRTFT'96) (Uppsala, Sweden), volume 1135 of Lecture Notes in Computer Science, pages 366-385. Springer-Verlag, 1996. An extended abstract is available on-line.
[ bib ]

[FJ96]

Clemens Fischer and Wil Janssen. Synchronous development of asynchronous systems. In Ugo Montanari and Vladimiro Sassone, editors, Proceedings of CONCUR'96, volume 1119 of Lecture Notes in Computer Science, pages 735-750. Springer-Verlag, 1996. An abstract is available on-line.
[ bib ]

[ORS96]

E.-R. Olderog, A. P. Ravn, and J. U. Skakkebæk. Refining system requirements to program specifications. In C. Heitmeyer and D. Mandrioli, editors, Formal Methods for Real-Time Computing, volume 5 of Trends in Software, chapter 5, pages 107-134. Wiley, 1996. An abstract is available on-line.
[ bib ]

[BJ96]

Jürgen Bohn and Wil Janssen. A strategic approach to transformational design. In Industrial Benefit and Advances in Formal Methods (FME'96), volume 1051 of Lecture Notes in Computer Science, pages 609-628. Springer-Verlag, 1996.
[ bib | .ps.gz ]

[Kle96a]

Stephan Kleuker. The extension of existing telecommunication software with new services using formal methods. In T. Margaria, editor, Proceedings of the International Workshop on Advanced Intelligent Networks, pages 91-106. University of Passau, 1996.
[ bib | .ps.gz ]

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.

[KT96]

S. Kleuker and H. Tjabben. The incremental development of correct specifications for distributed systems. In M.-C. Gaudel and J. Woodcock, editors, Industrial Benefit and Advances in Formal Methods (FME'96), volume 1051 of Lecture Notes in Computer Science, pages 479-498. Springer-Verlag, 1996.
[ bib | .ps.gz ]

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.

[SR96]

Michael Schenke and A. P. Ravn. Refinement from a control problem to programs. In Jean-Raymond Abrial, Egon Borger, and Hans Langmaack, editors, Formal methods for industrial applications: specifying and programming the steam boiler control, volume 1165 of Lecture Notes in Computer Science, pages 403-427. Springer-Verlag, 1996.
[ bib | .ps.gz ]

[BFFH95]

E. Best, Hans Fleischack, W. Fraczak, and R. P. Hopkins. A class of composable high level Petri nets with an application to the semantics of B(PN)². In Giorgio De Michelis and Michel Diaz, editors, Proceedings of the 16th Internationcal Conference on Application and Theory of Petri nets (Turin, Italy, June 26-30, 1995), volume 935 of Lecture Notes in Computer Science, pages 103-118. Springer-Verlag, 1995.
[ bib ]

[GF95]

A. Gronewold and Hans Fleischhack. Computing Petri net languages by reductions. In Horst Reichel, editor, Proceedings on the 10th International Conference on Fundamentals of computation theory (FCT'95) (Dresden, Germany, August 1995), volume 965 of Lecture Notes in Computer Science, pages 253-???. Springer-Verlag, 1995.
[ bib ]

[BFF⁺95]

Eike Best, Hans Fleischhack, W. Fraczak, R. P. Hopkins, H. Klaudel, and E. Pelz. An M-Net semantics of B(PN)². In J. Desel, editor, Structures in Concurrency Theory, Workshops in Computing. Springer-Verlag, 1995.
[ bib ]

[FT95]

Hans Fleischhack and Josef Tapken. Eine kompositionelle Petrinetz-Semantik für SDL-Spezifikationen. In J. Desel, Hans Fleischhack, A. Oberweis, and Michael Sonnenschein, editors, 2. Workshop Algorithmen und Werkzeuge für Petrinetze, number 22 in AIS reports. Fachbereich Informatik, Universität Oldenburg, 1995.
[ bib ]

[OS95]

E.-R. Olderog and M. Schenke. Design of real-time systems: The interface between duration calculus and program specifications. In J. Desel, editor, Structures in Concurrency Theory, Workshops in Computing, pages 32-54. Springer-Verlag, 1995.
[ bib | .ps.gz ]

[BH95]

Jürgen Bohn and Hardi Hungar. Traverdi - transformation and verification of distributed systems. Lecture Notes in Computer Science, 1009:317-???, 1995.
[ bib ]

[BR95]

Jürgen Bohn and Stephan Rössig. On automatic and interactive design of communicating systems. In E. Brinksma, W. R. Cleaveland, K. G. Larsen, T. Margaria, and B. Steffen, editors, Proceedings of the 1st International Workshop on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'95) (Aarhus, Denmark), volume 1019 of Lecture Notes in Computer Science, pages 216-237. Springer-Verlag, 1995.
[ bib ]

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

[KT95]

S. Kleuker and H. Tjabben. A formal approach to the development of reliable multi-user multimedia applications. In R. Gotzhein and J. Bredereke, editors, Proceedings of the 5th GI/ITG-Fachgespräch ``Formale Beschreibungstechniken für verteilte Systeme'', pages 1-10. University of Kaiserslautern, Department of Computer Science, 1995.
[ bib | .ps.gz ]

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.

[TKK95]

H. Tjabben, S. Kleuker, and A. Kehne. Provably correct intelligent networks. In Proceedings of the IEEE Intelligent Network '95 Workshop, May 9-11, 1995, Ottawa, Canada, 1995.
[ bib | .ps.gz ]

[Kle95]

S. Kleuker. A gentle introduction to specification engineering using a case study in telecommunications. In P. D. Mosses, M. Nielsen, and M. I. Schwartzbach, editors, International Joint Conference on Theory and Practice of Software Development (TAPSOFT'95), volume 915 of Lecture Notes in Computer Science, pages 636-650. Springer-Verlag, 1995.
[ bib | .ps.gz ]

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.

[M95]

R. Müller. Anforderungsgerechte Spezifikation eines zeitabhängigen Gebührenabrechnungssystems. Master's thesis, University of Oldenburg, Department of Computer Science, Oldenburg, Germany, April 1995.
[ bib ]