Dipl. Inform. Holger Rasch

 

1 Publications (BibTeX Source)

@ARTICLE{MORW07,
  AUTHOR = {M. M\"oller 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 = {2007},
  VOLUME = {},
  NUMBER = {},
  NOTE = {To appear.},
  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},
}