Prof. Dr. habil. Heike Wehrheim

 

1 Publications (with abstracts)

[MORW07]

M. Möller, E.-R. Olderog, H. Rasch, and H. Wehrheim. Integrating a formal method into a software engineering process with UML and Java. Formal Apsects of Computing, 2007. To appear.
[ bib ]

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 reactive systems. To this end, we propose a specific UML 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 verifying properties of the model, for instance by using the FDR model checker. On the other hand, it is the basis for generating contracts for the final implementation. Contracts are written in the Java Modeling Language (JML) complemented by , 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.

[BDFW07]

I. Brückner, K. Dräger, B. Finkbeiner, and H. Wehrheim. Slicing Abstractions. In F. Arbab and M. Sirjani, editors, FSEN 2007: IPM International Symposium on Fundamentals of Software Engineering, volume 4767 of Lecture Notes in Computer Science, pages 17-32. Springer, April 2007.
[ bib | .pdf ]

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.

[BMW06]

I. Brückner, B. Metzler, and H. Wehrheim. Optimizing slicing of formal specifications by deductive verification. Nordic Journal of Computing, 13(1-2):22-45, August 2006.
[ bib | .pdf ]

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

[BW05d]

Ingo Brückner and Heike Wehrheim. Slicing an Integrated Formal Method for Verification. In Kung-Kiu Lau and Richard Banach, editors, ICFEM 2005: Seventh International Conference on Formal Engineering Methods, volume 3785 of Lecture Notes in Computer Science, pages 360-374. Springer, November 2005. This publication is available at SpringerLink.
[ bib | .pdf ]

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 reducing such specifications (with respect to certain properties under interest) before verification. The method is an adaption of the 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.

[BW05a]

I. Brückner and H. Wehrheim. Slicing CSP-OZ Specifications for Verification. Technical Report 7, SFB/TR 14 AVACS, http://www.avacs.org/, 2005.
[ bib | .pdf ]

[OW05]

E.-R. Olderog and H. Wehrheim. Specification and (property) inheritance in CSP-OZ. Science of Computer Programming, 55:227-257, 2005.
[ bib ]

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. Key words: CSP, Object-Z, failures divergence semantics, inheritance, safety and ``liveness'' properties, model-checking, FDR

References

[Fis97]

C. Fischer. CSP-OZ: A combination of Object-Z and CSP. In H. Bowman and J. Derrick, editors, Formal Methods for Open Object-Based Distributed Systems (FMOODS'97), volume 2, pages 423-438. Chapman & Hall, 1997.

[Fis00]

C. Fischer. Combination and Implementation of Processes and Data: From CSP-OZ to Java. PhD thesis, Bericht Nr. 2/2000, University of Oldenburg, April 2000.

[Weh02]

H. Wehrheim. Behavioural subtyping in object-oriented specification formalisms. University of Oldenburg, Habilitation Thesis, 2002.

[BW05b]

I. Brückner and H. Wehrheim. Slicing Object-Z Specifications for Verification. In H. Treharne, S. King, M. Henson, and S. Schneider, editors, ZB 2005: Formal Specification and Development in Z and B, volume 3455 of LNCS, pages 414-433. Springer, April 2005. This publication is available at SpringerLink.
[ bib | .pdf ]

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.

[BW05c]

I. Brückner and H. Wehrheim. Slicing Object-Z Specifications for Verification. Technical Report 3, SFB/TR 14 AVACS, http://www.avacs.org/, 2005.
[ bib | .pdf ]

[Weh04]

H. Wehrheim. Preserving properties under change. In F.S. de Boer, M.M. Bonsangue, S. Graf, and W.-P. de Roever, editors, FMCO 2003: Formal Methods for Components and Objects, volume 3188 of LNCS, pages 330-343, 2004.
[ bib ]

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

[MORW04]

M. Möller, E.-R. Olderog, H. Rasch, and H. Wehrheim. Linking CSP-OZ with UML and Java: A Case Study. In E. Boiten, J. Derrick, and G. Smith, editors, Integrated Formal Methods, number 2999 in Lecture Notes in Computer Science, pages 267-286. Springer-Verlag, March 2004.
[ bib | .pdf ]

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.

[RW03]

H. Rasch and H. Wehrheim. Checking Consistency in UML Diagrams: Classes and State Machines. In E. Najm, U. Nestmann, and P. Stevens, editors, Formal Methods for Open Object-based Distributed Systems, volume 2884 of LNCS, pages 229-243. Springer, 2003.
[ bib | .ps ]

[Weh03b]

H. Wehrheim. Inheritance of Temporal Logic Properties. In E. Najm, U. Nestmann, and P. Stevens, editors, Formal Methods for Open Object-based Distributed Systems, volume 2884 of LNCS, pages 79-93. Springer, 2003.
[ bib | .ps ]

[OW03]

E.-R. Olderog and H. Wehrheim. Specification and Inheritance in CSP-OZ. In F. de Boer, M. Bosangue, S. Graf, and W.-P. de Roever, editors, Formal Methods for Components and Objects, volume 2852 of LNCS, pages 361-379. Springer, 2003.
[ bib ]

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.

References

[Fis97]

C. Fischer. CSP-OZ: A combination of Object-Z and CSP. In H. Bowman and J. Derrick, editors, Formal Methods for Open Object-Based Distributed Systems (FMOODS'97), volume 2, pages 423-438. Chapman & Hall, 1997.

[Fis00]

C. Fischer. Combination and Implementation of Processes and Data: From CSP-OZ to Java. PhD thesis, Bericht Nr. 2/2000, University of Oldenburg, April 2000.

[Weh02]

H. Wehrheim. Behavioural subtyping in object-oriented specification formalisms. University of Oldenburg, Habilitation Thesis, 2002.

[Weh03a]

H. Wehrheim. Behavioral Subtyping Relations for Active Objects. Formal Methods in System Design, 23(2):143-170, 2003.
[ bib ]

[DW03]

J. Derrick and H. Wehrheim. Using coupled simulations in non-atomic refinement. In D. Bert, J. Bowen, S. King, and M. Walden, editors, ZB 2003: Formal Specification and Development in Z and B, volume 2651 of LNCS, pages 127-147. Springer, 2003.
[ bib | .ps ]

[Weh02b]

H. Wehrheim. Relating state-based and behaviour-oriented subtyping. Nordic Journal of Computing, 9(4):405-435, 2002. appeared March 2003.
[ bib ]

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.

[RW02]

H. Rasch and H. Wehrheim. Consistency between UML classes and associated state machines. In L. Kuzniarz, G. Reggio, J. L. Sourrouille, and Z. Huzar, editors, UML 2002 - Workshop on Consistency Problems in UML-based Software Development, volume 06, pages 46-60, 2002.
[ bib ]

[Weh02a]

H. Wehrheim. Checking behavioural subtypes via refinement. In B. Jacobs and A. Rensink, editors, FMOODS 2002: Formal Methods for Open Object-Based Distributed Systems, pages 79-93. Kluwer, May 2002.
[ bib | .ps ]

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.

[RW01]

A. Rensink and H. Wehrheim. Process algebra with action dependencies. Acta Informatica, (38):155-234, 2001.
[ bib ]

[Weh01]

Heike Wehrheim. Patterns and Rules for Behavioural Subtyping. In M. Kim, B. Chin, S. Kang, and D. Lee, editors, FORTE 2001, pages 335 - 352. Kluwer, 2001.
[ bib | .ps ]

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.

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

[Weh00a]

H. Wehrheim. Data Abstraction Techniques in the Validation of CSP-OZ Specifications. Formal Aspects of Computing, 12, 2000.
[ bib ]

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

[Weh00c]

Heike Wehrheim. Specification of an automatic manufacturing system - a case study in using integrated formal methods. In FASE 2000, Fundamental Approaches to Software Engineering, volume 1783 of LNCS, 2000.
[ bib | .ps ]

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.

[Weh00b]

Heike Wehrheim. Behavioural subtyping and property preservation. In S. Smith and C. Talcott, editors, FMOODS'00: Formal Methods for Open Object-Based Distributed Systems. Kluwer, 2000.
[ bib | .ps ]

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.

[Weh00d]

Heike Wehrheim. Subtyping patterns for active objects. In H. Giese and S. Philippi, editors, Proceedings 8ter Workshop des GI-Arbeitskreises GROOM: Visuelle Verhaltensmodellierung verteilter und nebenläufiger Software-Systeme. Universität Münster, 2000. No. 24/00-I.
[ bib ]

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

[RW94]

Arend Rensink and Heike Wehrheim. Weak Sequential Composition in Process Algebras. In B. Jonsson and J. Parrow, editors, Concur '94: Concurrency Theory, volume 836 of LNCS, pages 226-241. Springer, 1994.
[ bib | .ps ]

[HNW98]

Michaela Huhn, Peter Niebert, and Heike Wehrheim. Partial order reductions for bisimulation checking. In V. Arvind and R. Ramanujam, editors, FST&TCS, volume 1530 of Lecture Notes in Computer Science, 1998.
[ bib | .ps ]

[GHRW98]

T. Gehrke, M. Huhn, A. Rensink, and H. Wehrheim. An algebraic semantics for message sequence chart documents. In S. Budkowski, A. Cavalle, and E. Najm, editors, FORTE/PSTV'98: Formal Description Techniques & Protocol Specification, Testing and Verification, pages 3-18. Kluwer Academic Publishers, 1998.
[ bib | .ps ]

[GHN⁺98]

Thomas Gehrke, Michaela Huhn, Peter Niebert, Arend Rensink, and Heike Wehrheim. A process algebra semantics for message sequence charts including conditions. In 8.GI/ITG Fachgespräch Formale Beschreibungstechniken für verteilte Systeme, 1998.
[ bib ]

[RW97]

Arend Rensink and Heike Wehrheim. Dependency-based action refinement. In P. Ruzicka, editor, MFCS'97 Mathematical Foundations of Computer Science, number 1295 in Lecture Notes in Computer Science. Springer, 1997.
[ bib | .ps.gz ]

[HWD96]

M. Huhn, H. Wehrheim, and G. Denker. Action refinement - an application of process theory on object-oriented specification. In 6. GI/ITG-Fachgespräch ''Formale Beschreibungstechniken für verteilte Systeme'', Arbeitsbericht des IMMD 1996, June 1996.
[ bib ]

[Weh96]

Heike Wehrheim. Specifying Reactive Systems with Action Dependencies: Modelling and Hierarchical Design. PhD thesis, University of Hildesheim, 1996.
[ bib ]

[GW96a]

Ursula Goltz and Heike Wehrheim. Causal testing. In W. Penczek and A. Szalas, editors, MFCS '96, number 1113 in Lecture Notes in Computer Science, pages 394-406, 1996.
[ bib | .ps.gz ]

[GW96b]

Ursula Goltz and Heike Wehrheim. Modelling causality by dependency of actions in branching time semantics. Information Processing Letters, 59(4):179-184, August 1996.
[ bib ]

[Weh94]

Heike Wehrheim. Parametric action refinement. In E.R. Olderog, editor, IFIP Transactions: Programming Concepts, Methods and Calculi, pages 247-266. Elsevier, 1994.
[ bib | .ps.gz ]