ForMooS - Selected Publications

(with abstracts)

[M05]

M. Möller. Mapping formal specifications to java contracts. In Proceedings of the 17th Nordic Workshop on Programming Theory, pages 100-102. University of Copenhagen, Denmark, October 2005.
[ bib | .pdf ]

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

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

[BM02]

M. Brörkens and M. Möller. Dynamic Event Generation for Runtime Checking using the JDI. In Klaus Havelund and Grigore Rosu, editors, Proceedings of the Second Workshop on Runtime Verification (RV'02), Copenhagen, Denmark, July 2002, volume 70 of Electronic Notes in Theoretical Computer Science. Elsevier Science, July 2002. This publication is available at ENTCS.
[ bib | .pdf ]

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

[M02]

Michael Möller. Specifying and Checking Java using CSP. In Workshop on Formal Techniques for Java-like Programs - FTfJP'2002. Computing Science Department, University of Nijmegen, June 2002. Technical Report NIII-R0204.
[ bib | .pdf ]

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. jassda is a framework for performing such runtime checks at the byte-code level of Java. The Trace-Checker module of 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.

[Weh02]

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.

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

[Weh00]

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.