Dr. Clemens Fischer

 

1 Publications (with abstracts)

[FW04]

C. Fischer and H. Wehrheim. Failure-Divergence Semantics as a Formal Basis for an Object-Oriented Integrated Formal Method. In G. Paun, G. Rozenberg, and A. Salomaa, editors, Current Trends in Theoretical Computer Science: The Challenge of the New Century, Vol 2: Formal Models and Semantics. World Scientific, 2004.
[ bib ]

[BFMW01]

D. Bartetzko, C. Fischer, M. Möller, and H. Wehrheim. Jass - Java with Assertions. In Klaus Havelund and Grigore Rosu, editors, Proceedings of the First Workshop on Runtime Verification (RV'01), Paris, France, July 2001, volume 55 of Electronic Notes in Theoretical Computer Science. Elsevier Science, 2001. This publication is available at ENTCS.
[ bib | .pdf ]

Design by Contract, proposed by Meyer for the programming language Eiffel, is a technique that allows run-time checks of specification violation and their treatment during program execution. , Java with assertions, is a Design by Contract extension for Java allowing to annotate Java programs with specifications in the form of assertions. The tool is a pre-compiler that translates annotated into pure Java programs in which compliance with the specification is dynamically tested. Besides the standard Design by Contract features known from classical program verification (e.g. pre- and postconditions, invariants), additionally supports refinement, i.e. subtyping, checks and the novel concept of trace assertions. Trace assertions are used to monitor the dynamic behaviour of objects in time.

[FOW01]

C. Fischer, E.-R. Olderog, and H. Wehrheim. A CSP view on UML-RT structure diagrams. In H. Husmann, editor, Fundamental Approaches to Software Engineering, volume 2029 of Lecture Notes in Computer Science, pages 91-108. Springer-Verlag, 2001.
[ bib | .ps ]

UML-RT is an extension of UML for modelling embedded reactive and real-time software systems. Its particular focus lies on system descriptions on the architectural level, defining the overall system structure. In this paper we propose to use UML-RT structure diagrams together with the formal method CSP-OZ combining CSP and Object-Z. While CSP-OZ is used for specifying the system components themselves (by CSP-OZ classes), UML-RT diagrams provide the architecture description. Thus the usual architecture specification in terms of the CSP operators parallel composition, renaming and hiding is replaced by a graphical description. To preserve the formal semantics of CSP-OZ specifications, we develop a translation from UML-RT structure diagrams to CSP. Besides achieving a more easily accessible, graphical architecture modelling for CSP-OZ, we thus also give a semantics to UML-RT structure diagrams.

[FW00a]

Clemens Fischer and Heike Wehrheim. Behavioural Subtyping Relations for Object-Oriented Formalisms. In T. Rus, editor, Algebraic Methodology and Software Technology, volume 1816 of LNCS, pages 469-483. Springer, 2000.
[ bib | .ps ]

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.

[FW00b]

Clemens Fischer and Heike Wehrheim. Failure-divergence semantics as a formal basis for an object-oriented integrated formal method. Bulletin of the EATCS (European Association of Theoretical Computer Science), 71:92 - 101, 2000.
[ bib | .ps ]

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.

[FW99]

Clemens Fischer and Heike Wehrheim. Model-checking CSP-OZ specifications with FDR. In K. Araki, A. Galloway, and K. Taguchi, editors, Proceedings of the 1st International Conference on Integrated Formal Methods (IFM), pages 315-334. Springer, 1999.
[ bib | .ps.gz ]

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

[Fis99]

Clemens Fischer. Software development with Object-Z, CSP and Java: A pragmatic link from formal specifications to programs. In B. Jacobs, B. Leavens, P. Müller, and A. Poetzsch-Heffter, editors, Formal Techniques for Java Programs, volume 251 of Technical Report, pages 29-35. Fernuniversität Hagen, 1999.
[ bib | .ps.gz ]

[FM98]

Clemens Fischer and D. Meemken. JaWA: Java with assertions. In C. H. Cap, editor, Java-Informations-Tage, Informatik aktuell, pages 49-59. Springer, 1998. In german.
[ bib ]

Methoden zur Entwicklung von korrekter Software und deren Einführung 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 überprüfen kann.

In diesem Paper geben wir einen Überblick über die Sprache JaWA, mit der dieses Konzept auf Java übertragen wurde.

JaWA Programme bestehen aus herkömmlichem Java-Code, der Zusicherungen (Invarianten, Vor- und Nachbedingungen) in Form von Kommentaren enthält. Der JaWA-Präcompiler übersetzt JaWA in Java. Er erzeugt zusätzliche Bedingungen, mit denen die spezifizierten Eigenschaften zur Laufzeit überprüft werden können. Dabei wird die Java Ausnahmebehandlung ausgenutzt und um Eiffel ähnliche `rescue' und `retry' Anweisungen ergänzt. Die erzeugten Fehlermeldungen und Warnungen sind frei konfigurierbar.

[Fis98]

Clemens Fischer. How to combine Z with a process algebra. In J. Bowen, A. Fett, and M. Hinchey, editors, ZUM'98 The Z Formal Specification Notation, volume 1493 of LNCS, pages 5-23. Springer, 1998.
[ bib ]

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?'

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

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

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

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

[Fis95]

Clemens Fischer. Semantics and compositional verification of muSDL. Labornotiz 1/95, Philips Research Laboratories Aachen, Germany, 1995.
[ bib | .ps.gz ]

[Fis93]

Clemens Fischer. Fehleranalyse bei der Spezifikationsentwicklung von intelligenten Telefonnetzen. University of Oldenburg, Department of Computer Science, Oldenburg, Germany, November 1993.
[ bib ]