Prof. Dr. Stephan Kleuker
On this page:
back to the mainpage.
1
Publications (BibTeX Source)
@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{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},
}
@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{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{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{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{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.
}
}
@TECHREPORT{sk96-philips,
AUTHOR = {S. Kleuker and H. Tjabben },
TITLE = {A Formal Approach to the Development of Reliable
Multi-User Multimedia Communication Systems },
TYPE = {Technical Report},
NUMBER = {1168/96},
INSTITUTION = {Philips Research Laboratories Aachen },
ADDRESS = {Germany},
YEAR = 1996,
URL = {http://csd.informatik.uni-oldenburg.de/pub/CoCoN/sk96-philips.ps.gz},
ABSTRACT = {
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.
}
}
@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}
}
@TECHREPORT{sk95-philips,
AUTHOR = {S. Kleuker and A. Kehne and H. Tjabben },
TITLE = {Provably Correct Communication Networks ({CoCoN}) },
TYPE = {Technical Report},
NUMBER = {1123/95 },
INSTITUTION = {Philips Research Laboratories Aachen },
ADDRESS = {Germany},
YEAR = 1995,
URL = {http://csd.informatik.uni-oldenburg.de/pub/CoCoN/sk95-philips.ps.gz},
ABSTRACT = {
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.
}
}
@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.
}
}
@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.
}
}
