Prof. Dr. habil. Heike Wehrheim
On this page:
back to the mainpage.
1
Publications (BibTeX Source)
@ARTICLE{MORW08,
AUTHOR = {M. M{\"o}ller and E.-R. Olderog and H. Rasch and H.
Wehrheim},
TITLE = {Integrating a Formal Method into a Software
Engineering Process with {UML} and {Java}},
JOURNAL = {Formal Apsects of Computing},
YEAR = {2008},
VOLUME = {20},
PAGES = {161--204},
ABSTRACT = {We describe how CSP-OZ, a formal method combining the
process algebra CSP with the specification language
Object-Z, can be integrated into an object-oriented
software engineering process employing the UML as a
modelling and Java as an implementation language. The
benefit of this integration lies in the rigour of the
formal method, which improves the precision of the
constructed models and opens up the possibility of (1)
verifying properties of models in the early design
phases, and (2) checking adherence of implementations
to models. The envisaged application area of our
approach is the design of distributed {\em reactive
systems}. To this end, we propose a specific UML {\em
profile} for reactive systems. The profile contains
facilities for modelling components, their interfaces
and interconnections via synchronous/broadcast
communication, and the overall architecture of a
system. The integration with the formal method proceeds
by generating a significant part of the CSP-OZ
specification from the initially developed UML model.
The formal specification is on the one hand the
starting point for {\em verifying} properties of the
model, for instance by using the FDR model checker. On
the other hand, it is the basis for generating {\em
contracts} for the final implementation. Contracts are
written in the Java Modeling Language (JML)
complemented by \CSPjassda{}, an assertion language for
specifying orderings between method invocations. A set
of tools for runtime checking can be used to supervise
the adherence of the final Java implementation to the
generated contracts.}
}
@INPROCEEDINGS{BDFW07,
AUTHOR = {I. Br\"uckner and K. Dr\"ager and B. Finkbeiner and H. Wehrheim},
TITLE = {{Slicing Abstractions}},
BOOKTITLE = {FSEN 2007: IPM International Symposium on Fundamentals of
Software Engineering},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {4767},
PUBLISHER = {Springer},
ISSN = {},
ISBN = {978-3-540-75697-2},
EDITOR = {F. Arbab and M. Sirjani},
PAGES = {17--32},
MONTH = {April},
YEAR = {2007},
ABSTRACT = {
Abstraction and slicing are both techniques for reducing the size
of the state space to be inspected during verification. In this
paper, we present a new model checking procedure for
infinite-state concurrent systems that interleaves automatic
abstraction refinement, which splits states according to new
predicates obtained by Craig interpolation, with slicing, which
removes irrelevant states and transitions from the
abstraction. The effects of abstraction and slicing complement
each other. As the refinement progresses, the increasing accuracy
of the abstract model allows for a more precise slice; the
resulting smaller representation gives room for additional
predicates in the abstraction. The procedure terminates when an
error path in the abstraction can be concretized, which proves
that the system is erroneous, or when the slice becomes empty,
which proves that the system is correct.
},
URL = {http://csd.informatik.uni-oldenburg.de/pub/Papers/ib07fsen.pdf}
}
@ARTICLE{BMW06,
AUTHOR = {I. Br\"uckner and B. Metzler and H. Wehrheim},
TITLE = {Optimizing Slicing of Formal Specifications by Deductive
Verification},
JOURNAL = {Nordic Journal of Computing},
YEAR = {2006},
VOLUME = {13},
NUMBER = {1--2},
MONTH = {August},
PAGES = {22--45},
ABSTRACT = {
Slicing is a technique for extracting parts of programs or
specifications with respect to certain criteria of interest. The
extraction is carried out in such a way that properties as
described by the slicing criterion are preserved, i.e., they hold
in the complete program if and only if they hold in the sliced
program. During verification, slicing is often employed to reduce
the state space of specifications to a size tractable by a model
checker.
The computation of specification slices relies on the construction
of dependence graphs, reflecting (at least) control and data
dependencies in specifications. The more dependencies the graph
has, the less removal of parts is possible. In this paper we
present a technique for optimizing the construction of the
dependence graph by using deductive verification techniques. More
precisely, we propose a technique for showing that certain control
dependencies in the graph can be eliminated. The technique
employs small {\em deductive} proofs of the enabledness of certain
transitions. Thereby we obtain dependence graphs with less
control dependencies and as a consequence smaller specification
slices which are an easier target for model checking.
},
URL = {http://csd.informatik.uni-oldenburg.de/pub/Papers/ib06njc.pdf}
}
@INPROCEEDINGS{BW05b,
AUTHOR = {Ingo Br\"uckner and Heike Wehrheim},
TITLE = {{Slicing an Integrated Formal Method for Verification}},
BOOKTITLE = {ICFEM 2005: Seventh International Conference on Formal
Engineering Methods},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {3785},
PUBLISHER = {Springer},
ISSN = {0302-9743},
ISBN = {3-540-29797-9},
EDITOR = {Kung-Kiu Lau and Richard Banach},
PAGES = {360--374},
MONTH = {November},
YEAR = {2005},
ABSTRACT = {
Model checking specifications with complex data and behaviour
descriptions often fails due to the large state space to be
processed. In this paper we propose a technique for {\em reducing}
such specifications (with respect to certain properties under
interest) before verification. The method is an adaption of the
{\em slicing technique} from program analysis to the area of
integrated formal notations and temporal logic properties. It
solely operates on the syntactic structure of the specification
which is usually significantly smaller than its state space. We
show how to build a reduced specification via the construction of
a so called program dependence graph, and prove correctness of the
technique with respect to a projection relationship between full
and reduced specification. The reduction thus preserves all
properties formulated in temporal logics which are invariant under
stuttering, as for instance LTL$_{-X}$.
},
NOTE = { This publication is available at
\url{
http://springerlink.metapress.com/openurl.asp?genre=article&issn=0302-9743&volum
e=3785&spage=360}
{SpringerLink}
},
URL = {http://csd.informatik.uni-oldenburg.de/pub/Papers/ib05icfem.pdf}
}
@TECHREPORT{BW05bTR,
AUTHOR = {I. Br\"uckner and H. Wehrheim},
TITLE = {{Slicing CSP-OZ Specifications for Verification}},
NUMBER = {7},
INSTITUTION = {{SFB/TR 14 AVACS}},
ADDRESS = {http://www.avacs.org/},
URL = {http://www.avacs.org/Publikationen/Open/avacs_technical_report_007.pdf},
YEAR = {2005},
}
@ARTICLE{OW05,
AUTHOR = {E.-R. Olderog and H. Wehrheim},
TITLE = {{Specification and (property) inheritance in CSP-OZ}},
JOURNAL = {Science of Computer Programming},
YEAR = {2005},
VOLUME = {55},
PAGES = {227--257},
ABSTRACT = {
CSP-OZ [Fis97, Fis00] is a combination of Communicating Sequential
Processes (CSP) and Object-Z (OZ). It enables the specification of
systems having both a state-based and a behaviour-oriented view
using the object-oriented concepts of classes, instantiation and
inheritance. CSP-OZ has a process semantics in the failure
divergence model of CSP. In this paper we explain CSP-OZ and
investigate the notion of inheritance. Furthermore, we study the
issue of property inheritance among classes. We prove in a uniform
way that behavioural subtyping relations between classes
introduced in [Weh02] guarantee the inheritance of safety and
``liveness'' properties.
\emph{Key words}: CSP, Object-Z, failures divergence semantics,
inheritance, safety and ``liveness'' properties, model-checking,
FDR
\begin{thebibliography}
\bibitem{Fis97}
C.~Fischer.
\newblock {CSP-OZ}: A combination of {Object-Z} and {CSP}.
\newblock In H.~Bowman and J.~Derrick, editors, {\em Formal Methods for Open
Object-Based Distributed Systems (FMOODS'97)}, volume~2, pages 423--438.
Chapman \& Hall, 1997.
\bibitem{Fis00}
C.~Fischer.
\newblock {\em Combination and Implementation of Processes and Data: From
{CSP-OZ} to {Java}}.
\newblock PhD thesis, Bericht Nr. 2/2000, University of Oldenburg, April 2000.
\bibitem{Weh02}
H.~Wehrheim.
\newblock Behavioural subtyping in object-oriented specification formalisms.
\newblock University of Oldenburg, Habilitation Thesis, 2002.
\end{thebibliography}
}
}
@INPROCEEDINGS{BW05a,
AUTHOR = {I. Br\"uckner and H. Wehrheim},
TITLE = {{Slicing Object-Z Specifications for Verification}},
BOOKTITLE = {ZB 2005: Formal Specification and Development in Z and B},
SERIES = {LNCS},
VOLUME = {3455},
PUBLISHER = {Springer},
ISSN = {0302-9743},
ISBN = {3-540-25559-1},
EDITOR = {H. Treharne and S. King and M. Henson and S. Schneider},
PAGES = {414--433},
MONTH = {April},
YEAR = {2005},
ABSTRACT = {
Slicing is the activity of reducing a program or a specification
with respect to a given condition (the slicing criterion) such
that the condition holds on the full program if and only if it
holds on the reduced program. Originating from program analysis
the entity to be sliced is usually a program and the slicing
criterion a value of a variable at a certain program point. In
this paper we present an approach to slicing Object-Z
specifications with temporal logic formulae as slicing criteria
and show the correctness of our approach. The underlying
motivation is the goal to substantially reduce the size of the
specification and subsequently facilitate verification of temporal
logic properties.
},
NOTE = {This publication is available at
\url{
http://springerlink.metapress.com/openurl.asp?genre=article&issn=0302-9743&volum
e=3455&spage=414}
{SpringerLink}
},
URL = {http://csd.informatik.uni-oldenburg.de/pub/Papers/ib05zb.pdf}
}
@TECHREPORT{BW05aTR,
AUTHOR = {I. Br\"uckner and H. Wehrheim},
TITLE = {{Slicing Object-Z Specifications for Verification}},
NUMBER = {3},
INSTITUTION = {{SFB/TR 14 AVACS}},
ADDRESS = {http://www.avacs.org/},
URL = {http://www.avacs.org/Publikationen/Open/avacs_technical_report_003.pdf},
YEAR = {2005},
}
@INPROCEEDINGS{Weh04,
AUTHOR = {H. Wehrheim},
TITLE = {Preserving properties under change},
BOOKTITLE = {FMCO 2003: Formal Methods for Components and Objects},
YEAR = {2004},
EDITOR = {F.S. de Boer and M.M. Bonsangue and S. Graf and W.-P. de
Roever},
VOLUME = {3188},
PAGES = {330--343},
SERIES = {LNCS}
}
@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{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{We03,
AUTHOR = {H. Wehrheim},
TITLE = {{Inheritance of Temporal Logic Properties}},
EDITOR = {E. Najm and U. Nestmann and P. Stevens},
BOOKTITLE = {Formal Methods for Open Object-based Distributed Systems},
VOLUME = {2884},
SERIES = {LNCS},
PAGES = {79--93},
PUBLISHER = {Springer},
URL = {http://csd.informatik.uni-oldenburg.de/~wehrheim/Fmoods03.ps},
YEAR = {2003}
}
@INPROCEEDINGS{OlWe02,
AUTHOR = {E.-R. Olderog and H. Wehrheim},
TITLE = {{Specification and Inheritance in CSP-OZ}},
EDITOR = {F. de Boer and M. Bosangue and S. Graf and W.-P. de Roever},
BOOKTITLE = {Formal Methods for Components and Objects},
VOLUME = {2852},
SERIES = {LNCS},
PAGES = {361--379},
PUBLISHER = {Springer},
YEAR = {2003},
ABSTRACT = {
CSP-OZ [Fis97,Fis00] is a combination of Communicating Sequential
Processes (CSP) and Object-Z (OZ). It enables the specification
of systems having both a state-based and a behaviour-oriented view
using the object-oriented concepts of classes, instantiation and
inheritance. CSP-OZ has a process semantics in the failures
divergence model of CSP. In this paper we explain CSP-OZ and
investigate the notion of inheritance. Behavioural subtyping
relations between classes introduced in [Weh02] guarantee the
inheritance of safety and ``liveness'' properties.
\begin{thebibliography}
\bibitem{Fis97}
C.~Fischer.
\newblock {CSP-OZ}: A combination of {Object-Z} and {CSP}.
\newblock In H.~Bowman and J.~Derrick, editors, {\em Formal Methods for Open
Object-Based Distributed Systems (FMOODS'97)}, volume~2, pages 423--438.
Chapman \& Hall, 1997.
\bibitem{Fis00}
C.~Fischer.
\newblock {\em Combination and Implementation of Processes and Data: From
{CSP-OZ} to {Java}}.
\newblock PhD thesis, Bericht Nr. 2/2000, University of Oldenburg, April 2000.
\bibitem{Weh02}
H.~Wehrheim.
\newblock Behavioural subtyping in object-oriented specification formalisms.
\newblock University of Oldenburg, Habilitation Thesis, 2002.
\end{thebibliography}
}
}
@ARTICLE{Weh03b,
AUTHOR = {H. Wehrheim},
TITLE = {{Behavioral Subtyping Relations for Active Objects}},
JOURNAL = {Formal Methods in System Design},
VOLUME = {23},
NUMBER = {2},
PAGES = {143--170},
YEAR = {2003}
}
@INPROCEEDINGS{DeWe03,
TITLE = {Using coupled simulations in non-atomic refinement},
AUTHOR = {J. Derrick and H. Wehrheim},
EDITOR = {D. Bert and J. Bowen and S. King and M. Walden},
BOOKTITLE = {ZB 2003: Formal Specification and Development in Z and B},
VOLUME = {2651},
SERIES = {LNCS},
PAGES = {127--147},
PUBLISHER = {Springer},
URL = {http://csd.informatik.uni-oldenburg.de/~wehrheim/ZB2003.ps},
YEAR = {2003}
}
@ARTICLE{weh03,
AUTHOR = {H. Wehrheim},
TITLE = {Relating State-based and Behaviour-oriented Subtyping},
JOURNAL = {Nordic Journal of Computing},
YEAR = {2002},
VOLUME = {9},
NUMBER = {4},
PAGES = {405--435},
NOTE = {appeared March 2003},
ABSTRACT = {
Subtyping relations for object-oriented formalisms describe
relationships between classes which satisfy the substitutability
requirement imposed on types and their subtypes. Subtyping
relations have been proposed both for state-based and for
behaviour-oriented specification formalisms. In this paper we
state and proof correspondence results between these two forms of
subtyping: starting from a state-based specification language we
show that via a behaviour-oriented semantics state-based
subtyping induces behaviour-oriented subtyping. In the comparison
we study three different kinds of subtyping achieving
substitutivity to a different degree. For all three kinds of
definitions a correspondence result can be shown.
}
}
@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{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}
}
@ARTICLE{rewe01,
AUTHOR = {A. Rensink and H. Wehrheim},
TITLE = {Process algebra with action dependencies},
JOURNAL = {Acta Informatica},
NUMBER = {38},
PAGES = {155--234},
YEAR = {2001}
}
@INPROCEEDINGS{weh01,
AUTHOR = {Heike Wehrheim},
TITLE = {{Patterns and Rules for Behavioural Subtyping}},
BOOKTITLE = {FORTE 2001},
EDITOR = {M. Kim and B. Chin and S. Kang and D. Lee},
PAGES = {335 - 352},
PUBLISHER = {Kluwer},
ABSTRACT = {
Subtyping relations for object-oriented formalisms describe
relationships between super- and subclasses which satisfy the
substitutability requirement imposed on types and their subtypes.
Behavioural subtyping is concerned with subtypes for active
classes with an explicit dynamic behaviour, specifiable for
instance by object-oriented formal methods combining state-based
with behavioural formalisms. Such specification languages often
have a formal semantics that composes behavioural semantics for
both the behaviour and the state-based part.
In this paper we develop syntactic patterns and semantic rules for
the state-based part of a subclass which guarantee that the
subclass is a behavioural subtype of its superclass. This allows
to check for subtypes without computing the behavioural semantics
of the class at all. Our results are similar to the ones linking
data refinement in state-based methods with failure-divergence
refinement in CSP. In contrast to classical data refinement,
subtyping (and the simulation relations used for showing the
soundness of the patterns) have to cope with additional new
operations in the subclass.
},
URL = {http://csd.informatik.uni-oldenburg.de/~wehrheim/forte01.ps},
YEAR = {2001}
}
@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}
}
@ARTICLE{weh00d,
AUTHOR = {H. Wehrheim},
TITLE = {{Data Abstraction Techniques in the Validation of CSP-OZ
Specifications}},
JOURNAL = {Formal Aspects of Computing},
YEAR = {2000},
VOLUME = {12},
PAGE = {147--164}
}
@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}
}
@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}
}
@INPROCEEDINGS{weh00b,
AUTHOR = {Heike Wehrheim},
TITLE = {Behavioural Subtyping and Property Preservation},
BOOKTITLE = {FMOODS'00: Formal Methods for Open Object-Based
Distributed Systems},
EDITOR = {S. Smith and C. Talcott},
PUBLISHER = {Kluwer},
ABSTRACT = {
Inheritance is one of the key features in object-oriented design
and analysis. It especially supports an incremental development by
allowing to stepwise add new functionality to an existing system
design. When using a subclass which is a specialisation of a
certain superclass, the question arises which of the superclass'
properties still hold for the subclass. We investigate this topic
for three behavioural subtyping relations, which formalise the
subtype - supertype relationship among classes on the basis of
process algebra correctness relations. According to the degree of
change allowed by the subtyping relations, safety and liveness
properties of the superclass are preserved up to different
extents.
},
URL = {http://csd.informatik.uni-oldenburg.de/~wehrheim/fmoods00.ps},
YEAR = {2000}
}
@INPROCEEDINGS{weh00c,
AUTHOR = {Heike Wehrheim},
TITLE = {Subtyping patterns for active objects},
EDITOR = {H. Giese and S. Philippi},
BOOKTITLE = {Proceedings 8ter Workshop des GI-Arbeitskreises GROOM:
Visuelle Verhaltensmodellierung verteilter und nebenl\"aufiger
Software-Systeme},
PUBLISHER = {Universit\"at M\"unster},
NOTE = {No. 24/00-I},
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{rewe94,
AUTHOR = {Arend Rensink and Heike Wehrheim},
PAGES = {226--241},
TITLE = {{Weak Sequential Composition in Process Algebras}},
EDITOR = {B.~Jonsson and J.~Parrow},
PUBLISHER = {Springer},
SERIES = {LNCS},
BOOKTITLE = {{Concur '94: Concurrency Theory}},
VOLUME = {836},
URL = {http://csd.informatik.uni-oldenburg.de/~wehrheim/Concur94.ps},
YEAR = {1994}
}
@INPROCEEDINGS{hunw98,
AUTHOR = {Michaela Huhn and Peter Niebert and Heike Wehrheim},
BOOKTITLE = {FST\&TCS},
TITLE = {Partial order reductions for bisimulation checking},
YEAR = {1998},
EDITOR = {V. Arvind and R. Ramanujam},
SERIES = {Lecture Notes in Computer Science},
URL = {http://csd.informatik.uni-oldenburg.de/~wehrheim/Fsttcs98.ps},
VOLUME = {1530}
}
@INPROCEEDINGS{ghrw98,
AUTHOR = {T. Gehrke and M. Huhn and A. Rensink and H. Wehrheim},
TITLE = {An algebraic semantics for Message Sequence Chart
Documents},
EDITOR = {S. Budkowski and A. Cavalle and E. Najm},
BOOKTITLE = {FORTE/PSTV'98: Formal Description Techniques \& Protocol
Specification, Testing and Verification},
PAGES = {3--18},
PUBLISHER = {Kluwer Academic Publishers},
URL = {http://csd.informatik.uni-oldenburg.de/~wehrheim/Forte98.ps},
YEAR = {1998}
}
@INPROCEEDINGS{ghnrw98,
AUTHOR = {Thomas Gehrke and Michaela Huhn and Peter Niebert and
Arend Rensink and Heike Wehrheim},
BOOKTITLE = {8.GI/ITG Fachgespr\"ach Formale Beschreibungstechniken
f\"ur verteilte Systeme},
TITLE = {A process algebra semantics for Message Sequence Charts
including conditions},
YEAR = {1998}
}
@INPROCEEDINGS{rw97,
AUTHOR = {Arend Rensink and Heike Wehrheim},
BOOKTITLE = {MFCS'97 Mathematical Foundations of Computer Science},
EDITOR = {P. Ruzicka},
NUMBER = {1295},
PUBLISHER = {Springer},
SERIES = {Lecture Notes in Computer Science},
TITLE = {Dependency-based action refinement},
URL = {http://csd.informatik.uni-oldenburg.de/~wehrheim/mfcs97.ps.gz},
YEAR = {1997}
}
@INPROCEEDINGS{huwd96,
AUTHOR = {M. Huhn and H. Wehrheim and G. Denker},
BOOKTITLE = {6. GI/ITG-Fachgespr\"ach ''Formale Beschreibungstechniken
f\"ur verteilte Systeme''},
INSTITUTION = {University of Hildesheim},
MONTH = JUN,
SERIES = {Arbeitsbericht des IMMD 1996},
TITLE = {Action Refinement --- An application of process theory on
object-oriented specification},
YEAR = {1996}
}
@PHDTHESIS{weh96,
AUTHOR = {Heike Wehrheim},
SCHOOL = {University of Hildesheim},
TITLE = {Specifying Reactive Systems with Action Dependencies:
Modelling and Hierarchical Design},
YEAR = {1996}
}
@INPROCEEDINGS{gowe96c,
AUTHOR = {Ursula Goltz and Heike Wehrheim},
BOOKTITLE = {MFCS '96},
EDITOR = {W. Penczek and A. Szalas},
NUMBER = {1113},
PAGES = {394-406},
SERIES = {Lecture Notes in Computer Science},
TITLE = {Causal testing},
URL = {http://csd.informatik.uni-oldenburg.de/~wehrheim/MFCS96.ps.gz},
YEAR = {1996}
}
@ARTICLE{gowe96b,
AUTHOR = {Ursula Goltz and Heike Wehrheim},
JOURNAL = {Information Processing Letters},
MONTH = AUG,
PAGES = {179-184},
TITLE = {Modelling Causality by Dependency of Actions in Branching
Time Semantics},
VOLUME = {59(4)},
YEAR = {1996}
}
@INPROCEEDINGS{weh94,
AUTHOR = {Heike Wehrheim},
BOOKTITLE = {IFIP Transactions: Programming Concepts, Methods and
Calculi},
EDITOR = {E.R. Olderog},
PAGES = {247-266},
PUBLISHER = {Elsevier},
TITLE = {Parametric Action Refinement},
URL = {http://csd.informatik.uni-oldenburg.de/~wehrheim/Procomet94.ps.gz},
YEAR = {1994}
}
