Prof. Dr. Stephan Kleuker

 

1 Publications (with abstracts)

[Kle98]

S. Kleuker. Reengineering of distributed systems using formal methods. In P. Nesi and F. Lehner, editors, Proceedings of the Second Euromicro Conference on Software Maintenance and Reengineering, pages 189-192. IEEE Computer Society, 1998.
[ bib ]

[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 ]

[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 ]

[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 ]

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

[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 ]

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

[KT96b]

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.

[KT96a]

S. Kleuker and H. Tjabben. A formal approach to the development of reliable multi-user multimedia communication systems. Technical Report 1168/96, Philips Research Laboratories Aachen, Germany, 1996.
[ bib | .ps.gz ]

Multi-user multimedia communication systems allow users at different sites to exchange any kind of information (video, audio and data) in a multipoint call. A typical application area for such systems can be hospitals. Especially the medical area poses strong requirements on the reliability and security of the communication systems and of the application software. This paper presents an approach how formal methods can help to meet these requirements. The first part of this paper gives a short introduction to a set of standards for multipoint communications recently proposed by the ITU-T (International Telecommunications Union - Telecommunications Standardization Sector). Only parts of these standards contain formal specifications while others contain only informal textual descriptions. The second part begins with the development of a simple formal specification of a multi-user multimedia communication system based on these standards. We start by collecting informal requirements for conference handling as the basic functionality of the system aimed at. These requirements are formalized and a specification is developed for which we prove that it is in accordance with the requirements. It is then explained how new functionality can be added with an incremental development technique. This technique supports that unchanged requirements remain valid in the new system. Stepwise employing of this technique leads from our initial specification to more enhanced and complete formal specifications. In the end we sketch how the final specification can be used for the development of new applications for multi-user multimedia communication systems. These applications are realized on top of a system with proven properties and therefore we can guarantee their correctness. Work presented in this paper is done as part of the project CoCoN (Provably Correct Communication Networks) that is carried out in cooperation between the Philips Research Laboratories in Aachen and the University of Oldenburg.

[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 ]

[KKT95]

S. Kleuker, A. Kehne, and H. Tjabben. Provably correct communication networks (CoCoN). Technical Report 1123/95, Philips Research Laboratories Aachen, Germany, 1995.
[ bib | .ps.gz ]

During the last few years there has been an ever increasing demand for the fast and flexible introduction of value-added services and new features into private as well as into public telecommunications networks. Intelligent networks (IN), personal communications, computer-supported telecommunications applications (CSTA) are just a few areas from which these services are emerging. Adding more and more services to the telecommunications network leads to a situation where not only the software part of the separate network components but also the structure of the network is becoming increasingly complex. Today, it is already difficult to maintain and to extend the systems. It becomes more and more harder to understand and to predict the behaviour of the system, e.g. in situations when interactions between services occur. Therefore it becomes a key issue to design communications system software that provably not only arguably meets its requirements. Aim of our project is to support a stepwise and verified development of communications systems from the requirement phase over the specification phase to an implementation. The vision that we have in mind is an engineering approach for the development of correct communications networks. Meanwhile theoretical work has reached a point where formal methods seem to be applicable to industrial-size applications. Here we would especially like to mention the ESPRIT Basic Research Project ProCoS (= Provably Correct Systems). This project was started in 1989 and finished in 1992, a follow-up project ProCoS II was initiated 1993. ProCoS is dedicated to cover the entire development process from the capture of the requirements down to the computer programs. ProCoS offers a constructive approach to correctness, that is based on a common mathematical model. Our project CoCoN is closely related to the ProCoS project. The formal methods that have been developed within the ProCoS framework establish the foundation of our approach. In particular, distributed embedded real-time systems are in the scope of ProCoS. Therefore the ProCoS- methods are considered to be directly applicable to problems from the communications area. Call handling for the originating and terminating side in a plain network configuration is used as a consistent example throughout the whole report to describe the principles of our approach. We proceed in the following way: Informal requirements for basic call handling are first identified and then captured in a formal language. In a next step from these formal requirements a specification is developed and it is proved that the resulting specification is correct with respect to the requirements. It is then shown how it is possible to decompose the resulting small switching system specification in order to come to more realistic network configurations. New transformation rules are introduced. These rules enable the stepwise extension of the starting system into a complex but still verified system.

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

[Kle94]

S. Kleuker. Case study: Stepwise refinement of a communication processor using trace logic. In D. J. Andrews, J. F. Groote, and C. A. Middelburg, editors, Semantics of Specification Languages, Workshops in Computing, pages 252-269. Springer-Verlag, 1994.
[ bib ]

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.