Publications 2001-2003

 

3 Publications 2001-2003 (BibTeX Source)

@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{We03,
  AUTHOR = {H. Wehrheim},
  TITLE = {{Inheritance of Temporal Logic Properties}},
  EDITOR = {E. Najm and U. Nestmann and P. Stevens},
  BOOKTITLE = {Formal Methods for Open Object-based Distributed Systems},
  VOLUME = {2884},
  SERIES = {LNCS},
  PAGES = {79--93},
  PUBLISHER = {Springer},
  URL = {http://csd.informatik.uni-oldenburg.de/~wehrheim/Fmoods03.ps},
  YEAR = {2003}
}


@INPROCEEDINGS{OlWe02,
  AUTHOR = {E.-R. Olderog and H. Wehrheim},
  TITLE = {{Specification and Inheritance in CSP-OZ}},
  EDITOR = {F. de Boer and M. Bosangue and S. Graf and W.-P. de Roever},
  BOOKTITLE = {Formal Methods for Components and Objects},
  VOLUME = {2852},
  SERIES = {LNCS},
  PAGES = {361--379},
  PUBLISHER = {Springer},
  YEAR = {2003},
  ABSTRACT = {
    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.

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

\bibitem{Fis00}
C.~Fischer.
\newblock {\em Combination and Implementation of Processes and Data: From
  {CSP-OZ} to {Java}}.
\newblock PhD thesis, Bericht Nr. 2/2000, University of Oldenburg, April 2000.

\bibitem{Weh02}
H.~Wehrheim.
\newblock Behavioural subtyping in object-oriented specification formalisms.
\newblock University of Oldenburg, Habilitation Thesis, 2002.
\end{thebibliography}
}
}


@ARTICLE{mcpees03,
  AUTHOR = {C. Schulte and M. Br\"orkens and I. Br\"uckner and 
R. Buscherm\"ohle and T. Wolf},
  TITLE = {{Sicherheit f\"ur sicherheitskritische Systeme}},
  JOURNAL = {Electronic Embedded Systeme},
  ISSN = {0943-4941},
  PUBLISHER = {AWi Verlag},
  MONTH = {September},
  PAGES = {19-21},
  YEAR = {2003},
  ABSTRACT = {
    Mikroprozessoren werden immer h\"aufiger auch in technischen
    Ger\"aten und vielerlei allt\"aglichen Konsumg\"utern eingesetzt.
    Letzere werden auch als eingebettete Systeme bezeichnet, das
    hei\ss{}t in umgebende technische Systeme wechselseitig
    integrierte Computersysteme. Die Entwicklung solcher eingebetteter
    Systeme wird unter anderem aufgrund immer h\"oherer Anforderungen
    an die Funktionalit\"at und einer wachsenden Anzahl von
    interagierenden Komponenten immer komplexer. Um diesem Umstand
    Rechnung zu tragen, werden in Prozessmodellen und Standards, die
    insbesondere im Bereich sicherheitskritischer Systeme angewendet
    werden, bereits seit geraumer Zeit vollst\"andige
    Korrektheitsnachweise gefordert. Ein aussichtsreicher Kandidat in
    diesem Kontext ist das Model-Checking.
  },
  URL = {http://csd.informatik.uni-oldenburg.de/pub/Papers/ib03.pdf}
}


@ARTICLE{Weh03b,
  AUTHOR = {H. Wehrheim},
  TITLE = {{Behavioral Subtyping Relations for Active Objects}},
  JOURNAL = {Formal Methods in System Design},
  VOLUME = {23},
  NUMBER = {2},
  PAGES = {143--170},
  YEAR = {2003}
}


@INPROCEEDINGS{DeWe03,
  TITLE = {Using coupled simulations in non-atomic refinement},
  AUTHOR = {J. Derrick and H. Wehrheim},
  EDITOR = {D. Bert and J. Bowen and S. King and M. Walden},
  BOOKTITLE = {ZB 2003: Formal Specification and Development in Z and B},
  VOLUME = {2651},
  SERIES = {LNCS},
  PAGES = {127--147},
  PUBLISHER = {Springer},
  URL = {http://csd.informatik.uni-oldenburg.de/~wehrheim/ZB2003.ps},
  YEAR = {2003}
}


@INPROCEEDINGS{sch03,
  AUTHOR = {A. Sch\"afer},
  TITLE = {Combining Real-Time Model-Checking and Fault Tree Analysis},
  BOOKTITLE = {FM 2003: the 12th International FME Symposium },
  YEAR = {2003},
  EDITOR = {D. Mandrioli and K. Araki and S. Gnesi},
  VOLUME = {2805},
  SERIES = {LNCS},
  PAGES = {522-541},
  PUBLISHER = {Springer},
  URL = {http://csd.Informatik.Uni-Oldenburg.DE/pub/Papers/as03.pdf},
  NOTE = {This publication is available at
   
\url{
http://www.springerlink.com/openurl.asp?genre=article&issn=0302-9743&volume=2805
&spage=522}
    {SpringerLink}
  },
  ABSTRACT = {
    We present a semantics for fault tree analysis, a technique used
    for the analysis of safety critical systems, in the real-time
    interval logic Duration Calculus with Liveness and show how
    properties of fault trees can be checked automatically. We apply
    this technique in two examples and show how it can be connected to
    other verification techniques.
  }
}


@INPROCEEDINGS{DT03,
  AUTHOR = {H. Dierks and J. Tapken},
  TITLE = {{\sc Moby/DC} -- {A} Tool for Model-Checking 
                   Parametric Real-Time Specifications},
  BOOKTITLE = {Tools and Algorithms for the Construction and
                  Analysis of Systems (TACAS 2003)},
  EDITOR = {H. Garavel and J. Hatcliff},
  YEAR = {2003},
  PAGES = {271--277},
  SERIES = {LNCS},
  VOLUME = 2619,
  PUBLISHER = {Springer},
  ABSTRACT = {
    We define an operational subset of Duration Calculus, called phase
    automata, which serves as an intermediate language for the
    analysis and verification of real-time system descriptions that
    contain timing parameters.  We introduce the tool Moby/DC which
    implements a model-checking algorithm for phase automata.  The
    algorithm applies compositional model-checking techniques and
    handles parameters by built-in procedures or by a link to CLP(R).
    Due to the parameters the model-checking problem is undecidable in
    general. Hence, we have to accept that the results are
    overapproximations only in order to guarantee termination.  The
    overapproximation together with the compositional technique makes
    the model-checker especially well suited for proving the absence
    of error traces instead of finding them.
  },
  URL = {http://csd.informatik.uni-oldenburg.de/~dierks/Berichte/TACAS03.ps.gz}
}


@ARTICLE{OD03,
  AUTHOR = {E.-R. Olderog and H. Dierks},
  TITLE = {{Moby/RT: A Tool for Specification and Verification of
Real-Time Systems}},
  JOURNAL = {Journal of Universal Computer Science},
  YEAR = {2003},
  VOLUME = {9},
  PAGES = {88--105},
  ABSTRACT = {
    The tool Moby/RT supports the design of real-time systems at the
    levels of requirements, design specifications and programs.
    Requirements are expressed by constraint diagrams [Kle00], design
    specifications by PLC-Automata [Die00], and programs by Structured
    Text, a programming language dedicated for programmable logic
    controllers (PLCs), or by programs for LEGO Mindstorm robots. In
    this paper we outline the theoretical background of Moby-RT by
    discussing its semantic basis and its use for automatic
    verification by utilising the model-checker UPPAAL.

\begin{thebibliography}
\bibitem{Kle00}
Kleuker, C. (2000).
\newblock {\em {Constraint Diagrams}}.
\newblock PhD thesis, University of Oldenburg.

\bibitem[Dierks, 2000]{Die00}
Dierks, H. (2000).
\newblock {PLC-Automata: A New Class of Implementable Real-Time Automata}.
\newblock {\em TCS}, 253(1):61--93.
\end{thebibliography}
  }
}


@ARTICLE{DO03,
  AUTHOR = {H. Dierks and E.-R. Olderog},
  TITLE = {{Temporale Spezifikationslogiken}},
  JOURNAL = {at-Automatisierungstechnik},
  YEAR = {2003},
  VOLUME = {51},
  NUMBER = {2},
  PAGES = {A1--A4},
  ABSTRACT = {
     Logiken sind in der Informatik ein weitverbreitetes Mittel zur
     Spezifikation. Dazu werden Logiken verschiedener Auspr{\"a}gung
     benutzt, z.B.  temporale Logiken f{\"u}r reaktive Systeme, zu
     denen die Systeme der Automatisierungstechnik z{\"a}hlen.  Dieser
     Beitrag enth{\"a}lt eine Einf{\"u}hrung in die wichtigsten
     temporalen Logiken und Literaturverweise.

     \textbf{English}\\
     Logics are often used in computer science as specification
     languages.  There is a rich variety of logics to choose from
     depending on the problem. Systems in automation technology are
     typically reactive systems for which temporal logics are
     adequate.  We introduce the most important temporal logics and
     give reference for further reading.
   }
}


@ARTICLE{weh03,
  AUTHOR = {H. Wehrheim},
  TITLE = {Relating State-based and Behaviour-oriented Subtyping},
  JOURNAL = {Nordic Journal of Computing},
  YEAR = {2002},
  VOLUME = {9},
  NUMBER = {4},
  PAGES = {405--435},
  NOTE = {appeared March 2003},
  ABSTRACT = {
     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.
   }
}


@ARTICLE{HO02b,
  AUTHOR = {J. Hoenicke and E.-R. Olderog},
  TITLE = {{CSP-OZ-DC}: A Combination of Specification Techniques for
Processes, 
    Data and Time},
  JOURNAL = {Nordic Journal of Computing},
  YEAR = {2002},
  VOLUME = {9},
  NUMBER = {4},
  PAGES = {301--334},
  NOTE = {appeared March 2003},
  ABSTRACT = {
    CSP-OZ-DC is a new combination of three well researched formal
    techniques for the specification of processes, data and time: CSP
    [Hoa85], Object-Z [Smi00], and Duration Calculus [ZHR91]. This
    combination is illustrated by specifying the train controller of a
    case study on radio controlled railway crossings. The technical
    contribution of the paper is a smooth integration of the
    underlying semantic models and its use for verifying timing
    properties of CSP-OZ-DC specifications. This is done by combining
    the model-checkers FDR [Ros94] for CSP and UPPAAL [BLL97] for
    timed automata with a new tool \emph{f2u} that transforms FDR
    transition systems and certain patterns of Duration Calculus
    formulae into timed automata. This approach is illustrated by the
    example of a vending machine.

 \begin{thebibliography}
\bibitem{BLL97}
J.~Bengtsson, K.G. Larsen, F.~Larsson, P.~Pettersson, and Wang Yi.
\newblock Uppaal -- a tool suite for automatic verification of real-time
  systems.
\newblock In R.~Alur, T.A. Henzinger, and E.D. Sonntag, editors, {\em Hybrid
  Systems III -- Verification and Control}, volume 1066 of {\em LNCS}, pages
  232--243. Springer, 1997.

\bibitem{Hoa85}
C.A.R. Hoare.
\newblock {\em Communicating Sequential Processes}.
\newblock Prentice Hall, 1985.

\bibitem{Ros94}
A.W. Roscoe.
\newblock Model-checking {CSP}.
\newblock In A.W. Roscoe, editor, {\em A Classical Mind --- Essays in Honour of
  C.A.R.Hoare}, pages 353--378. Prentice-Hall, 1994.

\bibitem{Smi00}
G.~Smith.
\newblock {\em The Object-Z Specification Language}.
\newblock Kluwer Academic Publisher, 2000.

\bibitem{ZHR91}
C.~Zhou, C.A.R. Hoare, and A.P. Ravn.
\newblock A calculus of durations.
\newblock {\em Information Processing Letters}, 40(5):269--276, 1991.
 \end{thebibliography}
 
}
}


@INPROCEEDINGS{DBL02,
  AUTHOR = {H. Dierks and G. Behrmann and K.G. Larsen},
  TITLE = {{Solving Planning Problems Using Real-Time Model-Checking 
(Translating PDDL3 into Timed Automata)}},
  BOOKTITLE = {{AIPS-Workshop Planning via Model-Checking}},
  PAGES = {30--39},
  YEAR = {2002},
  EDITOR = {F. Kabanza and S. Thiebaux},
  MONTH = APR,
  URL = {http://csd.Informatik.Uni-Oldenburg.DE/~dierks/Berichte/AIPS.ps.gz}
}


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


@INPROCEEDINGS{DL02,
  AUTHOR = {H. Dierks and M. Lettrari},
  TITLE = {{Constructing Test Automata from Graphical Real-Time 
Requirements}},
  BOOKTITLE = {FTRTFT 2002},
  PAGES = {433--453},
  YEAR = {2002},
  SERIES = {Lecture Notes in Computer Science},
  MONTH = SEP,
  PUBLISHER = {Springer-Verlag},
  URL = {http://csd.Informatik.Uni-Oldenburg.DE/~dierks/Berichte/FTRTFT02.ps.gz}
}


@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{ho02,
  AUTHOR = {J. Hoenicke and E.-R. Olderog},
  TITLE = {{Combining Specification Techniques for Processes Data and
Time}},
  EDITOR = {M. Butler and L. Petre and K. Sere},
  BOOKTITLE = {Integrated Formal Methods},
  SERIES = {Lecture Notes in Computer Science},
  VOLUME = {2335},
  PUBLISHER = {Springer-Verlag},
  URL = {http://csd.Informatik.Uni-Oldenburg.DE/~skript/pub/Papers/ho02-ifm.pdf},
  YEAR = {2002},
  MONTH = {May},
  PAGES = {245--266},
  ABSTRACT = {
    We present a new combination CSP-OZ-DC of three well researched
    formal techniques for the specification of processes, data and
    time: CSP [Hoa85], Object-Z [Smi00], and Duration Calculus
    [ZHR91]. The emphasis is on a smooth integration of the underlying
    semantic models and its use for verifying properties of CSP-OZ-DC
    specifications by a combined application of the model-checkers FDR
    [Ros94] for CSP and UPPAAL [BLL97] for Timed Automata.  This
    approach is applied to part of a case study on radio controlled
    railway crossings.
  }
}


@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{weh02,
  AUTHOR = {H. Wehrheim},
  TITLE = {Checking Behavioural Subtypes via Refinement},
  BOOKTITLE = {FMOODS 2002: Formal Methods for Open Object-Based
    Distributed Systems},
  EDITOR = {B. Jacobs and A. Rensink},
  YEAR = {2002},
  MONTH = {May},
  PAGES = {79--93},
  PUBLISHER = {Kluwer},
  ABSTRACT = {
    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.
  },
  URL = {http://csd.informatik.uni-oldenburg.de/~wehrheim/fmoods02.ps}
}


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


@ARTICLE{rewe01,
  AUTHOR = {A. Rensink and H. Wehrheim},
  TITLE = {Process algebra with action dependencies},
  JOURNAL = {Acta Informatica},
  NUMBER = {38},
  PAGES = {155--234},
  YEAR = {2001}
}


@INPROCEEDINGS{weh01,
  AUTHOR = {Heike Wehrheim},
  TITLE = {{Patterns and Rules for Behavioural Subtyping}},
  BOOKTITLE = {FORTE 2001},
  EDITOR = {M. Kim and B. Chin and S. Kang and D. Lee},
  PAGES = {335 - 352},
  PUBLISHER = {Kluwer},
  ABSTRACT = {
    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.
  },
  URL = {http://csd.informatik.uni-oldenburg.de/~wehrheim/forte01.ps},
  YEAR = {2001}
}


@MISC{hoe01,
  AUTHOR = {J. Hoenicke},
  TITLE = {{Specification of Radio Based Railway Crossings with the
                  Combination of CSP, OZ, and DC}},
  MONTH = JUN,
  YEAR = 2001,
  HOWPUBLISHED = {FBT 2001},
  URL = {http://www.i-u.de/fbt2001/fbt2001_docs/hoenicke.ps}
}


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


@INPROCEEDINGS{fow01,
  AUTHOR = {C. Fischer and E.-R. Olderog and H. Wehrheim},
  TITLE = {{A CSP view on UML-RT structure diagrams}},
  BOOKTITLE = {{Fundamental Approaches to Software Engineering}},
  PAGES = {91-108},
  YEAR = {2001},
  EDITOR = {H. Husmann},
  VOLUME = {2029},
  SERIES = {Lecture Notes in Computer Science},
  PUBLISHER = {Springer-Verlag},
  ABSTRACT = {
    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.
  },
  URL = {http://csd.informatik.uni-oldenburg.de/~wehrheim/fase01.ps}
}


@INPROCEEDINGS{bo01,
  AUTHOR = {M. Broy and E.-R. Olderog},
  TITLE = {{Trace-Oriented Models of Concurrency}},
  BOOKTITLE = {Handbook of Process Algebra},
  PAGES = {101-195},
  YEAR = {2001},
  EDITOR = {J.A. Bergstra and A. Ponse and S.A. Scott},
  PUBLISHER = {Elsevier Science B.V.},
  ABSTRACT = {
    This chapter provides an in-depth presentation of trace-oriented
    models of concurrent processes.  We begin by introducing and
    investigating finite traces as a simple abstraction of the
    transition behaviour of automata.  Using finite traces safety
    properties of processes can be modelled.  Later infinite traces or
    {\it streams} together with stream processing functions are
    studied.  Using infinite traces more advanced phenomena like
    fairness and liveness properties can be modelled.  We discuss and
    relate operational, denotational, algebraic and logical approaches
    to trace-oriented models and explain methods for the specification
    and verification of process behaviour based on these models.
  }
}


@ARTICLE{dt01,
  AUTHOR = {H. Dierks and J. Tapken},
  TITLE = {{Moby/PLC: Eine graphische Entwicklungsumgebung f{\"u}r
      SPS-Programme}},
  JOURNAL = {at-Automatisierungstechnik},
  YEAR = {2001},
  VOLUME = {1},
  PAGES = {38--44},
}