Dipl. Inform. Holger Rasch

 

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{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},
}