Dipl.-Inform. Michael Möller

 

1 Publications (BibTeX Source)

@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{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{mbmm02,
  AUTHOR = {M. Br\"orkens and M. M\"oller},
  TITLE = {{jassda Trace Assertions}},
  BOOKTITLE = {Trends in Testing Communicating Systems},
  PAGES = {39--48},
  YEAR = {2002},
  EDITOR = {Ina Schieferdecker and Hartmut K\"onig and Adam Wolisz},
  SERIES = {International Confernece on Testing Communicating Systems
                  (TestCom)},
  ADDRESS = {Berlin, Germany},
  MONTH = {March},
  OPTNOTE = {to be published as Technical Report by Frauenhofer
                  Gesellschaft},
  URL = {http://csd.Informatik.Uni-Oldenburg.DE/pub/Papers/mbmm02.pdf}
}


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