ForMooS - Selected Publications
(BibTeX Source)
back to the mainpage.
@INPROCEEDINGS{mm05-nwpt,
AUTHOR = {M. M\"oller},
TITLE = {Mapping Formal Specifications to Java Contracts},
BOOKTITLE = {Proceedings of the 17th Nordic Workshop on Programming Theory},
PUBLISHER = {University of Copenhagen, Denmark},
PAGES = {100--102},
YEAR = {2005},
MONTH = {October},
URL = {http://csd.informatik.uni-oldenburg.de/pub/Papers/mm05-nwpt.pdf}
}
@INPROCEEDINGS{MORW04,
AUTHOR = {M. M\"oller and E.-R. Olderog and H. Rasch and H. Wehrheim},
TITLE = {{Linking CSP-OZ with UML and Java: A Case Study}},
EDITOR = {E. Boiten and J. Derrick and G. Smith},
BOOKTITLE = {Integrated Formal Methods},
SERIES = {Lecture Notes in Computer Science},
NUMBER = {2999},
PUBLISHER = {Springer-Verlag},
ISSN = {0302-9743},
PAGES = {267--286},
YEAR = {2004},
MONTH = {March},
ABSTRACT = {
We describe how CSP-OZ, an integrated formal method combining the
process algebra CSP with the specification language Object-Z, can
be linked to standard software engineering languages, viz.\ UML
and Java. Our aim is to generate a significant part of the CSP-OZ
specification from an initially developed UML model using a UML
profile for CSP-OZ, and afterwards transform the formal
specification into assertions written in the Java Modelling
Language JML complemented by CSP$_{jassda}$. The intermediate
CSP-OZ specification serves to verify correctness of the UML
model, and the assertions control at runtime the adherence of a
Java implementation to these formal requirements. We explain this
approach using the case study of a ``holonic manufacturing
system'' in which coordination of transportation and processing is
distributed among stores, machine tools and agents without central
control.
},
URL = {http://csd.informatik.uni-oldenburg.de/pub/Papers/morw04.pdf},
}
@INPROCEEDINGS{RaWe03,
AUTHOR = {H. Rasch and H. Wehrheim},
TITLE = {{Checking Consistency in UML Diagrams: Classes and State Machines}},
EDITOR = {E. Najm and U. Nestmann and P. Stevens},
BOOKTITLE = {Formal Methods for Open Object-based Distributed Systems},
VOLUME = {2884},
SERIES = {LNCS},
PAGES = {229--243},
PUBLISHER = {Springer},
YEAR = {2003},
URL = {http://csd.informatik.uni-oldenburg.de/~wehrheim/RaWe03.ps},
}
@INPROCEEDINGS{rawe02,
AUTHOR = {H. Rasch and H. Wehrheim},
TITLE = {Consistency between {UML} Classes
and Associated State Machines},
BOOKTITLE = {{UML} 2002 -- Workshop on Consistency Problems
in {UML}-based Software Development},
PAGES = {46--60},
YEAR = {2002},
EDITOR = {L. Kuzniarz and G. Reggio and J. L. Sourrouille and Z. Huzar},
VOLUME = {06},
}
@INPROCEEDINGS{mbmm02b,
AUTHOR = {M. Br\"orkens and M. M\"oller},
TITLE = {{Dynamic Event Generation for Runtime Checking using the
JDI}},
BOOKTITLE = {Proceedings of the Second Workshop on Runtime Verification
(RV'02), Copenhagen, Denmark, July 2002},
PUBLISHER = {Elsevier Science},
EDITOR = {Klaus Havelund and Grigore Rosu},
VOLUME = 70,
NUMBER = 4,
SERIES = {Electronic Notes in Theoretical Computer Science},
YEAR = 2002,
MONTH = {July},
NOTE = {This publication is available at
\url{http://www.elsevier.nl/locate/entcs/volume70.html}{ENTCS}},
URL = {http://csd.Informatik.Uni-Oldenburg.DE/pub/Papers/jassda-events.pdf},
ABSTRACT = {
Approaches to runtime checking have to track the execution of a
software system and therefore have to deal with generating and
processing execution events. Often these techniques are applied at
the code level -- either by inserting new source code prior to the
compilation or by modifying the target code, e.g. Java byte code,
before running the program.
The \textsf{jassda} framework and tool enable runtime checking of
Java programs against a CSP-like specification. For generating
events it uses the Java Debug Interface (JDI) and thus no
modifications to the code are necessary. Another advantage is that
events are generated on demand, i.e. dynamically at runtime it is
determined which events to generate for the current debug run
without modifying the program itself. This paper shows how this
event generation is done by the \textsf{jassda} framework.
}
}
@INPROCEEDINGS{mm02,
AUTHOR = {Michael M\"oller},
TITLE = {{Specifying and Checking Java using CSP}},
BOOKTITLE = {Workshop on Formal Techniques for Java-like Programs -
FTfJP'2002},
YEAR = {2002},
MONTH = {June},
ORGANIZATION = {Computing Science Department, University of Nijmegen},
NOTE = {Technical Report NIII-R0204},
URL = {http://csd.Informatik.Uni-Oldenburg.DE/pub/Papers/csp4j.pdf},
ABSTRACT = {
Currently several approaches are done in applying formal
techniques to the Java programming language. A new trend is to
take dynamic behaviour into account when designing such
techniques. To bring formal techniques to practical applications
one often has to reduce the goal coming down from full
verification to runtime checking.
\textsf{jassda} is a framework for performing such runtime checks
at the byte-code level of Java. The Trace-Checker module of
\textsf{jassda} allows one to test the dynamic behaviour of
multiple Java virtual machines by monitoring whether the trace of
all relevant events is a member of the trace semantics of a given
CSP process or not.
In this paper we present the CSP dialect that is used to specify a
set of allowed traces for Java programs. The underlying semantics
allows partial specifications of distributed Java programs and to
recombine them while preserving properties.
}
}
@INPROCEEDINGS{weh02,
AUTHOR = {H. Wehrheim},
TITLE = {Checking Behavioural Subtypes via Refinement},
BOOKTITLE = {FMOODS 2002: Formal Methods for Open Object-Based
Distributed Systems},
EDITOR = {B. Jacobs and A. Rensink},
YEAR = {2002},
MONTH = {May},
PAGES = {79--93},
PUBLISHER = {Kluwer},
ABSTRACT = {
Behavioural subtyping is concerned with the question of whether
one class is behaviourally consistent with another class. The
word ``behaviour'' in this context usually refers to the semantics
of methods, typically given by pre- and postconditions. In this
paper, we will use this term in a more specific way, referring to
the dynamic behaviour of objects in time. Behaviour descriptions
of classes give sequencing constraints on method invocations, in
this paper formulated using the process algebra CSP.
Behavioural subtyping can be seen as a mixture of refinement and
inheritance: we expect the subtype to be substitutable for the
supertype while at the same moment allowing extension of
functionality. Since refinement itself does not allow extension of
functionality, a subtyping definition must therefore extend
standard refinement concepts to cope with additional methods in
the subtype. In this paper, we show for three such subtyping
relations how they can, despite these extensions, be checked via
refinement. This gives us the possibility of employing standard
refinement checkers for CSP (viz. the FDR modelchecker) for
subtype checks.
},
URL = {http://csd.informatik.uni-oldenburg.de/~wehrheim/fmoods02.ps}
}
@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{weh2000,
AUTHOR = {Heike Wehrheim},
TITLE = {Specification of an Automatic Manufacturing System -- A
case study in using integrated formal methods},
EDITOR = {},
BOOKTITLE = {FASE 2000, Fundamental Approaches to Software
Engineering},
SERIES = {LNCS},
VOLUME = {1783},
NOTE = {},
ABSTRACT = {
An automatic manufacturing system serves as a case study for the
applicability of an integrated formal method to the specification
of software systems. The formal method chosen is CSP-OZ, an
integration of the state-oriented formalism Object-Z with the
process algebra CSP. The practicability as well as limitations of
CSP-OZ are studied. We furthermore employ a graphical notation
(class diagrams) from the Unified Modelling Language to describe
the architectural view of the system. The correctness of the
obtained specification is checked by a translation into the input
language of the CSP model checker FDR and a following property
check.
},
URL = {http://csd.informatik.uni-oldenburg.de/~wehrheim/fase00.ps},
YEAR = {2000}
}
