Dr. Clemens Fischer
On this page:
back to the mainpage.
1
Publications (BibTeX Source)
@INCOLLECTION{FiWe04,
AUTHOR = {C. Fischer and H. Wehrheim},
EDITOR = {G. Paun and G. Rozenberg and A. Salomaa},
TITLE = {{Failure-Divergence Semantics
as a Formal Basis for an Object-Oriented Integrated Formal Method}},
PUBLISHER = {World Scientific},
YEAR = {2004},
BOOKTITLE = {Current Trends in Theoretical Computer Science:
The Challenge of the New Century, Vol 2: Formal Models and
Semantics}
}
@INPROCEEDINGS{bfmw01,
AUTHOR = {D. Bartetzko and C. Fischer and M. M\"oller and H. Wehrheim},
TITLE = {{Jass -- Java with Assertions}},
BOOKTITLE = {Proceedings of the First Workshop on Runtime Verification
(RV'01), Paris, France, July 2001},
PUBLISHER = {Elsevier Science},
EDITOR = {Klaus Havelund and Grigore Rosu},
VOLUME = 55,
NUMBER = 2,
SERIES = {Electronic Notes in Theoretical Computer Science},
YEAR = 2001,
NOTE = {This publication is available at
\url{http://www.elsevier.nl/locate/entcs/volume55.html}
{ENTCS}
},
URL = {http://csd.Informatik.Uni-Oldenburg.DE/pub/Papers/jass.pdf},
ABSTRACT = {
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. \jass, {\bf J}ava with {\bf ass}ertions, is a Design
by Contract extension for Java allowing to annotate Java programs
with specifications in the form of assertions. The \jass{} 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), \jass{} additionally supports \emph{refinement}, i.e.
subtyping, \emph{checks} and the novel concept of \emph{trace
assertions}. Trace assertions are used to monitor the dynamic
behaviour of objects in time.
}
}
@INPROCEEDINGS{fow01,
AUTHOR = {C. Fischer and E.-R. Olderog and H. Wehrheim},
TITLE = {{A CSP view on UML-RT structure diagrams}},
BOOKTITLE = {{Fundamental Approaches to Software Engineering}},
PAGES = {91-108},
YEAR = {2001},
EDITOR = {H. Husmann},
VOLUME = {2029},
SERIES = {Lecture Notes in Computer Science},
PUBLISHER = {Springer-Verlag},
ABSTRACT = {
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.
},
URL = {http://csd.informatik.uni-oldenburg.de/~wehrheim/fase01.ps}
}
@INPROCEEDINGS{cfhw2000,
AUTHOR = {Clemens Fischer and Heike Wehrheim},
TITLE = {{Behavioural Subtyping Relations for Object-Oriented
Formalisms}},
EDITOR = {T. Rus},
BOOKTITLE = {{Algebraic Methodology and Software Technology}},
SERIES = {LNCS},
VOLUME = {1816},
PUBLISHER = {Springer},
PAGES = {469--483},
NOTE = {},
ABSTRACT = {
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.
},
URL = {http://csd.informatik.uni-oldenburg.de/~wehrheim/amast00.ps},
YEAR = {2000}
}
@ARTICLE{fiwe00b,
AUTHOR = {Clemens Fischer and Heike Wehrheim},
TITLE = {Failure-Divergence Semantics as a Formal Basis for an
Object-Oriented Integrated Formal Method},
JOURNAL = {Bulletin of the EATCS (European Association of Theoretical
Computer Science)},
VOLUME = {71},
PAGES = {92 -- 101},
URL = {http://csd.informatik.uni-oldenburg.de/~wehrheim/Eatcs.ps},
ABSTRACT = {
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.
},
YEAR = {2000}
}
@INPROCEEDINGS{cfhw99,
AUTHOR = {Clemens Fischer and Heike Wehrheim},
TITLE = {Model-Checking {CSP-OZ} Specifications with {FDR}},
BOOKTITLE = {Proceedings of the 1st International Conference on
Integrated Formal Methods (IFM)},
EDITOR = {K. Araki and A. Galloway and K. Taguchi},
YEAR = 1999,
PAGES = {315--334},
PUBLISHER = {Springer},
ABSTRACT = {
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
\emph{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.
},
URL = {http://csd.informatik.uni-oldenburg.de/pub/Papers/cfhw99.ps.gz}
}
@INPROCEEDINGS{fischer99:softwdevelobjeczcspjava,
AUTHOR = {Clemens Fischer},
TITLE = {Software Development with {Object-Z}, {CSP} and {Java}: A
Pragmatic Link from Formal Specifications to Programs},
BOOKTITLE = {Formal Techniques for Java Programs},
EDITOR = {B. Jacobs and B. Leavens and P. M\"uller and A.
Poetzsch-Heffter},
VOLUME = 251,
SERIES = {Technical Report},
YEAR = 1999,
PUBLISHER = {Fernuniversit{\"a}t Hagen},
PAGES = {29--35},
URL = {http://csd.informatik.uni-oldenburg.de/pub/Papers/cspoz2jass.ps.gz}
}
@INPROCEEDINGS{fischer98:jawa,
AUTHOR = {Clemens Fischer and D. Meemken},
TITLE = {{JaWA}: {Java} with Assertions},
BOOKTITLE = {Java-Informations-Tage},
EDITOR = {C. H. Cap},
SERIES = {Informatik aktuell},
YEAR = 1998,
PUBLISHER = {Springer},
PAGES = {49-59},
NOTE = {In german.},
ABSTRACT = {
Methoden zur Entwicklung von korrekter Software und deren
Einf\"uhrung 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 \"uberpr\"ufen kann.
In diesem Paper geben wir einen \"Uberblick \"uber die Sprache
JaWA, mit der dieses Konzept auf Java \"ubertragen wurde.
JaWA Programme bestehen aus herk\"ommlichem Java-Code, der
Zusicherungen (Invarianten, Vor- und Nachbedingungen) in Form von
Kommentaren enth\"alt. Der JaWA-Pr\"acompiler \"ubersetzt JaWA in
Java. Er erzeugt zus\"atzliche Bedingungen, mit denen die
spezifizierten Eigenschaften zur Laufzeit \"uberpr\"uft werden
k\"onnen. Dabei wird die Java Ausnahmebehandlung ausgenutzt und
um Eiffel \"ahnliche `rescue' und `retry' Anweisungen
erg\"anzt. Die erzeugten Fehlermeldungen und Warnungen sind frei
konfigurierbar.
}
}
@INPROCEEDINGS{fischer98:howzprocesalgeb,
AUTHOR = {Clemens Fischer},
TITLE = {How to combine {Z} with a Process Algebra},
BOOKTITLE = {{ZUM'98} The {Z} Formal Specification Notation},
EDITOR = {J. Bowen and A. Fett and M. Hinchey},
VOLUME = {1493 },
PAGES = {5-23},
SERIES = {LNCS},
YEAR = 1998,
PUBLISHER = {Springer},
ABSTRACT = {
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?'
}
}
@INPROCEEDINGS{cfgs97,
AUTHOR = {Clemens Fischer and Graeme Smith},
TITLE = {Combining {CSP} and {Object-Z}: Finite or Infinite
Trace-Semantics?},
BOOKTITLE = {Proceedings of FORTE/PSTV'97},
PUBLISHER = {Chapmann \& Hall},
EDITOR = {T. Mizuno and N. Shiratori and T. Higashino and A.
Togashi},
PAGES = {503 - 518},
NOTE = {\url{http://csd.informatik.uni-oldenburg.de/pub/Papers/cfgs97-a.ps}
{An abstract is available on-line}},
YEAR = 1997
}
@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{cf97-gi,
AUTHOR = {Clemens Fischer},
TITLE = {Combining {Object-Z} and {CSP}},
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},
NUMBER = 315,
YEAR = 1997,
PAGES = {119--128},
NOTE = {\url{http://csd.informatik.uni-oldenburg.de/pub/Papers/cf97-gi-a.ps.gz}
{An abstract is available on-line}}
}
@INPROCEEDINGS{cf97,
AUTHOR = {Clemens Fischer},
TITLE = {{CSP-OZ}: A Combination of {Object-Z} and {CSP}},
BOOKTITLE = {Formal Methods for Open Object-Based Distributed Systems
(FMOODS '97)},
YEAR = 1997,
VOLUME = 2,
EDITOR = {H. Bowmann and J. Derrick},
PUBLISHER = {Chapman \& Hall},
PAGES = {423--438},
{An abstract is available on-line}},
ABSTRACT = {
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.
}
}
@INPROCEEDINGS{cfwj96,
AUTHOR = {Clemens Fischer and Wil Janssen},
TITLE = {Synchronous Development of Asynchronous Systems},
BOOKTITLE = {Proceedings of CONCUR'96},
EDITOR = {Ugo Montanari and Vladimiro Sassone},
VOLUME = {1119},
SERIES = {Lecture Notes in Computer Science},
PUBLISHER = {Springer-Verlag},
YEAR = 1996,
PAGES = {735--750},
NOTE = {\url{http://csd.informatik.uni-oldenburg.de/pub/CoCoN/cfwj96-a.ps.gz}
{An abstract is available on-line}}
}
@TECHREPORT{cf95-philips,
AUTHOR = {Clemens Fischer},
TITLE = {Semantics and Compositional Verification of {$\mu$SDL}},
INSTITUTION = {Philips Research Laboratories Aachen },
ADDRESS = {Germany},
YEAR = 1995,
TYPE = {Labornotiz},
NUMBER = {1/95},
URL = {http://csd.informatik.uni-oldenburg.de/pub/CoCoN/cf95-philips.ps.gz}
}
@UNPUBLISHED{cf93,
AUTHOR = {Clemens Fischer},
TITLE = {{Fehleranalyse bei der Spezifikationsentwicklung von
intelligenten Telefonnetzen}},
YEAR = 1993,
MONTH = NOV,
TYPE = {Studienarbeit},
NOTE = {University of Oldenburg, Department of Computer Science, Oldenburg, Germany}
}
