Correct System Design

Dr. Clemens Fischer

email: Clemens.Fischer

In April 2000 Clemens Fischer completed his PhD with the dissertation ``Combination and Implementation of Processes and Data: from CSP-OZ to Java'', which is available as Technical Report No. 2/00 of the Department of Computer Science at the University of Oldenburg.
Foto

 


top of page

Tools

Jass-Precompiler
top of page

Publications (technical reports at the bottom)

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

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

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

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

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

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

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

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

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

top of page go back

Technical Reports of Clemens Fischer

TRCF-97-1
Combining CSP and Z
A preliminary work on the combination of CSP and Z.
(Available on request)
TRCF-97-2
CSP-OZ: A Combination of CSP and Object-Z
A long version of [cf97].
This paper is available on line
TRCF-97-3
Data-Refinement in CSP-OZ, joint work with Stefan Hallerstede
Rules for the refinement of the Object-Z part of an CSP-OZ class. Standard data-refinement and weak data-refinement rules (data-refinement + Introduction of local channels) are investigated.
An abstract is available on line

Last Modified: November 12, 1997

For comments and requests, please contact me.
top of page

Theses

[Fis00]
Clemens Fischer. Combination and Implementation of Processes and Data: from CSP-OZ to Java. PhD thesis, University of Oldenburg, January 2000.
[ bib | .ps.gz ]

[Fis95]
Clemens Fischer. Transformation von synchronen SL-Spezifikationen von Telekommunikationssystemen in asynchrone SL-Spezifikationen. Master's thesis, 1995. This publication is available on-line in two parts. Part 1, Part 2.
[ bib ]