Publications 2004-2006

 

2 Publications 2004-2006 (BibTeX Source)

@INPROCEEDINGS{QS06,
  AUTHOR = {J.-D. Quesel and A. Sch\"afer},
  TITLE = {Spatio-Temporal Model Checking for Mobile Real-Time  Systems},
  BOOKTITLE = {3rd International Colloquium on Theoretical Aspects 
               of Computing, ICTAC},
  YEAR = {2006},
  EDITOR = {K. Barkaoui and A. Cavalcanti and A. Cerone},
  SERIES = {LNCS},
  PAGES = {347--361},
  ABSTRACT = {
    This paper presents an automatic verification method for combined
    temporal and spatial properties of mobile real-time systems. To
    this end, we provide a translation of the Shape Calculus (SC), a
    spatio-temporal extension of Duration Calculus, into weak second
    order logic of one successor (WS1S).  A prototypical
    implementation facilitates successful verification of
    spatio-temporal properties by translating SC specifications into
    the syntax of the WS1S checker MONA.  For demonstrating the
    formalism and tool usage, we apply it to the benchmark case study
    ``generalised railroad crossing'' (GRC) enriched by requirements
    inexpressible in non-spatial formalisms.
  }
}


@ARTICLE{BMW06,
  AUTHOR = {I. Br\"uckner and B. Metzler and H. Wehrheim},
  TITLE = {Optimizing Slicing of Formal Specifications by Deductive
Verification},
  JOURNAL = {Nordic Journal of Computing},
  YEAR = {2006},
  VOLUME = {13},
  NUMBER = {1--2},
  MONTH = {August},
  PAGES = {22--45},
  ABSTRACT = {
    Slicing is a technique for extracting parts of programs or
    specifications with respect to certain criteria of interest.  The
    extraction is carried out in such a way that properties as
    described by the slicing criterion are preserved, i.e., they hold
    in the complete program if and only if they hold in the sliced
    program.  During verification, slicing is often employed to reduce
    the state space of specifications to a size tractable by a model
    checker.

    The computation of specification slices relies on the construction
    of dependence graphs, reflecting (at least) control and data
    dependencies in specifications.  The more dependencies the graph
    has, the less removal of parts is possible.  In this paper we
    present a technique for optimizing the construction of the
    dependence graph by using deductive verification techniques.  More
    precisely, we propose a technique for showing that certain control
    dependencies in the graph can be eliminated.  The technique
    employs small {\em deductive} proofs of the enabledness of certain
    transitions.  Thereby we obtain dependence graphs with less
    control dependencies and as a consequence smaller specification
    slices which are an easier target for model checking.
  },
  URL = {http://csd.informatik.uni-oldenburg.de/pub/Papers/ib06njc.pdf}
}


@INPROCEEDINGS{MFR2006,
  AUTHOR = {Roland Meyer and Johannes Faber and Andrey Rybalchenko},
  TITLE = {Model Checking Duration Calculus: A Practical Approach},
  BOOKTITLE = {Theoretical Aspects of Computing - ICTAC 2006},
  YEAR = {2006},
  EDITOR = {K. Barkaoui and A. Cavalcanti and A. Cerone},
  SERIES = {LNCS},
  VOLUME = {4281},
  PAGES = {332--346},
  URL = {http://csd.informatik.uni-oldenburg.de/~jfaber/dl/MeyerFaberRybalchenko2006.pdf
},
  NOTE = {This publication is available at
   
\url{
http://www.springerlink.com/openurl.asp?genre=article&id=doi:10.1007/11921240_23
}
    {SpringerLink}},
  ABSTRACT = {
    Model checking of real-time systems with respect to Duration
    Calculus (DC) specifications requires the translation of DC
    formulae into automata-based semantics. This task is difficult to
    automate.  The existing algorithms provide a limited DC coverage
    and do not support compositional verification. We propose a
    translation algorithm that advances the applicability of model
    checking tools to real world applications.  Our algorithm
    significantly extends the subset of DC that can be handled. It
    decomposes DC specifications into sub-properties that can be
    verified independently. The decomposition bases on a novel
    distributive law for DC. We implemented the algorithm as part of
    our tool chain for the automated verification of systems
    comprising data, communication, and real-time aspects. Our
    translation facilitated a successful application of the tool chain
    on an industrial case study from the European Train Control System
    (ETCS).
  }
}


@INPROCEEDINGS{Meyer2006Dagstuhl,
  AUTHOR = {R. Meyer},
  TITLE = {Model Checking the $\pi$-Calculus},
  BOOKTITLE = {Proceedings of the International Research Training Groups
Workshop},
  PAGES = {15},
  YEAR = {2006},
  VOLUME = {3},
  SERIES = {Trustworthy Software Systems},
  PUBLISHER = {GITO},
}


@INPROCEEDINGS{FR06,
  AUTHOR = {Johannes Faber and Roland Meyer},
  TITLE = {Model Checking Data-Dependent Real-Time Properties
                 of the European Train Control System},
  BOOKTITLE = {Formal Methods in Computer Aided Design, 2006. FMCAD '06},
  YEAR = {2006},
  MONTH = NOV,
  PAGES = {76--77},
  PUBLISHER = {IEEE Computer Society Press},
  NOTE = {This publication is available free of charge at
    \url{http://doi.ieeecomputersociety.org/10.1109/FMCAD.2006.21}
    {IEEE Digital Library}},
  ABSTRACT = {
    The behavior of embedded hardware and software systems is
    determined by at least three dimensions: control flow, data
    aspects, and real-time requirements. To specify the different
    dimensions of a system with the best-suited techniques, the formal
    language CSP-OZ-DC integrates Communicating Sequential Processes
    (CSP), Object-Z (OZ), and Duration Calculus (DC) into a
    declarative formalism equipped with a unified and compositional
    semantics. In this paper, we provide evidence that CSP-OZ-DC is a
    convenient language for modeling systems of industrial
    relevance. To this end, we examine the emergency message handling
    in the European Train Control System (ETCS) as a case study with
    uninterpreted constants and infinite data domains. We
    automatically verify that our model ensures real-time safety
    properties, which crucially depend on the system?s data handling.
  }
}


@INPROCEEDINGS{SS06,
  AUTHOR = {Tim Strazny and Christian Stehno},
  TITLE = {{E}in {S}imulator {f}\"{u}r {m}ehrfach {e}rweiterte
{h}\"{o}here {P}etrinetze},
  BOOKTITLE = {19. Symposium Simulationstechnik (ASIM 2006)},
  EDITOR = {Matthias Becker and Helena Szczerbicka},
  YEAR = {2006},
  MONTH = SEP,
  PAGES = {171--176},
  PUBLISHER = {SCS Publishing House e.V.},
}


@INPROCEEDINGS{erobs06,
  AUTHOR = {E.-R. Olderog and B. Steffen},
  TITLE = {{F}ormale {S}emantik und {P}rogrammverifikation},
  BOOKTITLE = {Informatik-Handbuch, 4. Auflage},
  EDITOR = {P. Rechenberg and G. Pomberger},
  YEAR = 2006,
  PUBLISHER = {Hanser Verlag},
  PAGES = {145--166}
}


@INPROCEEDINGS{SBO06,
  AUTHOR = {P. E. Sevin\c{c} and D. Basin and E.-R. Olderog},
  BOOKTITLE = {ETRICS 2006},
  EDITOR = {G\"unter M\"uller},
  MONTH = {June},
  PAGES = {352--367},
  PUBLISHER = {Springer-Verlag},
  SERIES = {LNCS},
  TITLE = {Controlling Access to Documents: A Formal Access Control Model},
  VOLUME = 3995,
  YEAR = 2006,
  ABSTRACT = {
    Current access-control systems for documents suffer from one or
    more of the following limitations: they are coarse-grained,
    limited to XML documents, ot unable to maintain control over
    copies of documents once they are released by the system.  We
    present a formal model of a system that overcomes all of these
    restrictions. It is very fine-grained, supporst a general class of
    documents, and provides a foundation for usage control.
  }
}


@INPROCEEDINGS{DBLP:conf/cade/BeckertP06,
  AUTHOR = {Bernhard Beckert and Andr{\'e} Platzer},
  TITLE = {Dynamic Logic with Non-rigid Functions: A Basis for 
           Object-oriented Program Verification},
  BOOKTITLE = {Automated Reasoning, Third International Joint Conference,
               IJCAR 2006, Seattle, WA, USA, August 17-20, 2006, Proceedings},
  YEAR = {2006},
  EDITOR = {U. Furbach and N. Shankar},
  VOLUME = {4130},
  SERIES = {LNCS},
  SUBSERIES = {LNAI},
  PAGES = {266--280},
  DOI = {10.1007/11814771_23},
  ISSN = {0302-9743},
  ISBN = {3-540-37187-7},
  PUBLISHER = {Springer-Verlag},
  KEYWORDS = {dynamic logic, sequent calculus, program logic, software 
              verification, logical foundations of programming languages, 
              object-orientation},
  NOTE = {\url{http://dx.doi.org/10.1007/11814771_23}{(c)
Springer-Verlag}},
  URL = {http://www.functologic.com/pub/odl.pdf},
  ABSTRACT = { 
    We introduce a dynamic logic that is enriched by non-rigid
    functions, i.e., functions that may change their value from state
    to state (during program execution), and we present a (relatively)
    complete sequent calculus for this logic.  In conjunction with
    dynamically typed object enumerators, non-rigid functions allow to
    embed notions of object-orientation in dynamic logic, thereby
    forming a basis for verification of object-oriented programs.  A
    semantical generalisation of substitutions, called state update,
    which we add to the logic, constitutes the central technical
    device for dealing with object aliasing during function
    modification.  With these few extensions, our dynamic logic
    captures the essential aspects of the complex verification system
    KeY and, hence, constitutes a foundation for object-oriented
    verification with the principles of reasoning that underly the
    successful KeY case studies.
  }
}


@ARTICLE{DHO06,
  AUTHOR = {W. Damm and H. Hungar and E.-R. Olderog},
  TITLE = {Verification of cooperating traffic agents},
  JOURNAL = {International Journal of Control},
  YEAR = {2006},
  VOLUME = {79},
  NUMBER = {5},
  MONTH = {May},
  PAGES = {395--421},
  ABSTRACT = {
    This paper exploits design patterns employed in coordinating
    autonomous transport vehicles so as to ease the burden in
    verifying cooperating hybrid systems. The presented verification
    methodology is equally applicable for avionics applications (such
    as TCAS, the Traffic Alert and Collision Avoidance System), train
    applications (such as ETCS, the European Train Control System), or
    automotive applications (such as platooning).  We present a
    verification rule explicating the essence of employed design
    patters, guaranteeing global safety properties of the kind ``a
    collision will never occur'', and whose premises can either be
    established by off-line analysis of the worst-case behavior of the
    involved traffic agents, or by purely local proofs, involving only
    a single traffic agent. A companion paper will show how such local
    proof obligations can be discharged automatically.
  }
}


@INCOLLECTION{Meyer2006,
  AUTHOR = {R. Meyer},
  TITLE = {Model Checking Using Testing},
  BOOKTITLE = {Dependability Engineering},
  PAGES = {147--171},
  PUBLISHER = {GITO},
  YEAR = {2006},
  EDITOR = {W. Hasselbring and S. Giesecke},
  VOLUME = {2},
  SERIES = {Trustworthy Software Systems},
}


@INPROCEEDINGS{ibnwpt05,
  AUTHOR = {I. Br{\"u}ckner and B. Metzler},
  TITLE = {{Deductive Verification for Improving Slicing of Integrated
Formal 
      Specifications}},
  BOOKTITLE = {Proceedings of the 17th Nordic Workshop on Programming Theory},
  PUBLISHER = {University of Copenhagen, Denmark},
  PAGES = {39--41},
  YEAR = {2005},
  MONTH = {October},
  URL = {http://csd.informatik.uni-oldenburg.de/pub/Papers/ib05-nwpt.pdf}
}


@INPROCEEDINGS{nwpt05,
  AUTHOR = {Johannes Faber},
  TITLE = {Verifying Real-Time aspects of the {European Train Control
System}},
  BOOKTITLE = {Proceedings of the 17th Nordic Workshop on Programming Theory},
  PUBLISHER = {University of Copenhagen, Denmark},
  PAGES = {67--70},
  YEAR = {2005},
  MONTH = {October},
  URL = {http://csd.informatik.uni-oldenburg.de/pub/Papers/jf05-nwpt.pdf}
}


@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{Die05b,
  AUTHOR = {H. Dierks},
  TITLE = {{Finding Optimal Plans for Domains with Continuous
      Effects with UPPAAL CORA}},
  BOOKTITLE = {{Proceedings of the ICAPS'05 Workshop on Verification
      and Validation of Model-Based Planning and Scheduling Systems}},
  MONTH = {June},
  YEAR = {2005}
}


@INPROCEEDINGS{BS05,
  AUTHOR = {R. Boute and A. Sch\"afer},
  TITLE = {The Timer Cascade: Functional Modelling and Real Time Calculi},
  BOOKTITLE = {Theoretical Aspects of Computing, ICTAC 2005},
  PAGES = {242 - 256},
  YEAR = {2005},
  EDITOR = {D.V. Hung and M. Wirsing},
  VOLUME = {3722},
  SERIES = {LNCS},
  PUBLISHER = {Springer},
  URL = {http://csd.Informatik.Uni-Oldenburg.DE/~skript/pub/Papers/bs05.pdf},
  NOTE = {This publication is available at
   
\url{
http://www.springerlink.com/openurl.asp?genre=article&id=doi:10.1007/11560647_16
}
    {SpringerLink}
  },
  ABSTRACT = {
    Case studies can significantly contribute towards improving the
    understanding of formalisms and thereby to their applicability in
    practice. One such case, namely a cascade of the familiar 24-hour
    timers (in suitably generalized form) provides interesting
    gedanken experiments and illustrations for presenting,
    illustrating and comparing various formalisms for modelling
    real-time behaviour of systems.
    
    The timer cascade is first modelled in a general-purpose
    functional formalism (Funmath) and various properties are derived,
    including an interesting algebraic monoid structure of timer
    programs. Then it is described and analyzed in duration calculus,
    thereby highlighting, similarities and differences in the approach
    to modelling and reasoning, and also the link between the
    formalisms.
    
    Future work consists in using this case as a running example for
    exploring the same issues for other formalisms intended for real
    time and hybrid systems.  The underlying idea is that other
    authors join this effort and contribute towards extending it,
    finally arriving at a broad comparative survey of such formalisms.
  }
}


@INPROCEEDINGS{BW05b,
  AUTHOR = {Ingo Br\"uckner and Heike Wehrheim},
  TITLE = {{Slicing an Integrated Formal Method for Verification}},
  BOOKTITLE = {ICFEM 2005: Seventh International Conference on Formal 
    Engineering Methods},
  SERIES = {Lecture Notes in Computer Science},
  VOLUME = {3785},
  PUBLISHER = {Springer},
  ISSN = {0302-9743},
  ISBN = {3-540-29797-9},
  EDITOR = {Kung-Kiu Lau and Richard Banach},
  PAGES = {360--374},
  MONTH = {November},
  YEAR = {2005},
  ABSTRACT = {
    Model checking specifications with complex data and behaviour
    descriptions often fails due to the large state space to be
    processed. In this paper we propose a technique for {\em reducing}
    such specifications (with respect to certain properties under
    interest) before verification. The method is an adaption of the
    {\em slicing technique} from program analysis to the area of
    integrated formal notations and temporal logic properties. It
    solely operates on the syntactic structure of the specification
    which is usually significantly smaller than its state space.  We
    show how to build a reduced specification via the construction of
    a so called program dependence graph, and prove correctness of the
    technique with respect to a projection relationship between full
    and reduced specification.  The reduction thus preserves all
    properties formulated in temporal logics which are invariant under
    stuttering, as for instance LTL$_{-X}$.
},
  NOTE = { This publication is available at
   
\url{
http://springerlink.metapress.com/openurl.asp?genre=article&issn=0302-9743&volum
e=3785&spage=360}
    {SpringerLink}
  },
  URL = {http://csd.informatik.uni-oldenburg.de/pub/Papers/ib05icfem.pdf}
}


@INPROCEEDINGS{HoenickeMaierFM2005,
  AUTHOR = {Jochen Hoenicke and Patrick Maier},
  TITLE = {Model-Checking of Specifications Integrating Processes, Data and
Time},
  BOOKTITLE = {FM 2005},
  EDITOR = {J.S. Fitzgerald and I.J. Hayes and A. Tarlecki},
  SERIES = {LNCS},
  VOLUME = {3582},
  PUBLISHER = {Springer},
  YEAR = {2005},
  PAGES = {465--480},
  URL = {http://csd.Informatik.Uni-Oldenburg.DE/~skript/pub/Papers/hm05-fm.pdf},
  ABSTRACT = {
  We present a new model-checking technique for CSP-OZ-DC, a
  combination of CSP, Object-Z and Duration Calculus, that allows
  reasoning about systems exhibiting communication, data and real-time
  aspects. As intermediate layer we will use a new kind of timed
  automata that preserve events and data variables of the
  specification. These automata have a simple operational semantics
  that is amenable to verification by a constraint-based
  abstraction-refinement model checker. By means of a case study, a
  simple elevator parameterised by the number of floors, we show that
  this approach admits model-checking parameterised and infinite state
  real-time systems.
}
}


@INPROCEEDINGS{EichnerFleischhackMeyerSchrimpfStehno2005,
  AUTHOR = {C. Eichner and H. Fleischhack and R. Meyer and U. Schrimpf and C.
Stehno},
  TITLE = {Compositional Semantics for UML 2.0 Sequence Diagrams Using
               Petri Nets},
  BOOKTITLE = {{SDL} 2005: Model Driven},
  YEAR = {2005},
  PAGES = {133--148},
  SERIES = {LNCS},
  VOLUME = {3530},
  PUBLISHER = {Springer-Verlag},
}


@INPROCEEDINGS{sch05b,
  AUTHOR = {A. Sch\"afer},
  TITLE = {{Axiomatisation and Decidability of Multi-Dimensional Duration
Calculus}},
  BOOKTITLE = {Proceedings of the 12th International Symposium on Temporal 
    Representation and Reasoning, {TIME} 2005},
  PAGES = {122-130},
  MONTH = {June},
  YEAR = {2005},
  EDITOR = {J. Chomicki and D. Toman},
  VOLUME = {},
  SERIES = {},
  URL = {http://csd.Informatik.Uni-Oldenburg.DE/pub/Papers/as05.pdf},
  PUBLISHER = {IEEE Computer Society},
  NOTE = {This publication is available at
    \url{http://doi.ieeecomputersociety.org/10.1109/TIME.2005.15}
    {IEEE Digital Library}
  },
  ABSTRACT = {
    We investigate properties of a spatio-temporal logic based on an
    n-dimensional Duration Calculus tailored for the specification and
    verification of mobile real-time systems. After showing
    non-axiomatisability, we give a complete embedding in
    n-dimensional interval temporal logic and present two different
    decidable subsets, which are important for tool support and
    practical use.
  }
}


@ARTICLE{OW05,
  AUTHOR = {E.-R. Olderog and H. Wehrheim},
  TITLE = {{Specification and (property) inheritance in CSP-OZ}},
  JOURNAL = {Science of Computer Programming},
  YEAR = {2005},
  VOLUME = {55},
  PAGES = {227--257},
  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 failure
    divergence model of CSP. In this paper we explain CSP-OZ and
    investigate the notion of inheritance. Furthermore, we study the
    issue of property inheritance among classes. We prove in a uniform
    way that behavioural subtyping relations between classes
    introduced in [Weh02] guarantee the inheritance of safety and
    ``liveness'' properties.
    
    \emph{Key words}: CSP, Object-Z, failures divergence semantics,
    inheritance, safety and ``liveness'' properties, model-checking,
    FDR

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


@MISC{ib05zb,
  AUTHOR = {I. Br{\"u}ckner},
  TITLE = {{Slicing CSP-OZ Specifications for Verification}},
  HOWPUBLISHED = {Poster Session, 4th International Conference
                   of B and Z Users (ZB '05)},
  MONTH = {April},
  YEAR = {2005},
}


@INPROCEEDINGS{BW05a,
  AUTHOR = {I. Br\"uckner and H. Wehrheim},
  TITLE = {{Slicing Object-Z Specifications for Verification}},
  BOOKTITLE = {ZB 2005: Formal Specification and Development in Z and B},
  SERIES = {LNCS},
  VOLUME = {3455},
  PUBLISHER = {Springer},
  ISSN = {0302-9743},
  ISBN = {3-540-25559-1},
  EDITOR = {H. Treharne and S. King and M. Henson and S. Schneider},
  PAGES = {414--433},
  MONTH = {April},
  YEAR = {2005},
  ABSTRACT = {
    Slicing is the activity of reducing a program or a specification
    with respect to a given condition (the slicing criterion) such
    that the condition holds on the full program if and only if it
    holds on the reduced program. Originating from program analysis
    the entity to be sliced is usually a program and the slicing
    criterion a value of a variable at a certain program point. In
    this paper we present an approach to slicing Object-Z
    specifications with temporal logic formulae as slicing criteria
    and show the correctness of our approach. The underlying
    motivation is the goal to substantially reduce the size of the
    specification and subsequently facilitate verification of temporal
    logic properties.
  },
  NOTE = {This publication is available at
   
\url{
http://springerlink.metapress.com/openurl.asp?genre=article&issn=0302-9743&volum
e=3455&spage=414}
    {SpringerLink}
  },
  URL = {http://csd.informatik.uni-oldenburg.de/pub/Papers/ib05zb.pdf}
}


@INPROCEEDINGS{sch05,
  AUTHOR = {A. Sch\"afer},
  TITLE = {A calculus for shapes in time and space},
  BOOKTITLE = {Theoretical Aspects of Computing, ICTAC 2004},
  PAGES = {463-478},
  YEAR = {2005},
  EDITOR = {Z. Liu and K. Araki},
  VOLUME = {3407},
  SERIES = {LNCS},
  URL = {http://csd.Informatik.Uni-Oldenburg.DE/pub/Papers/as05a.pdf},
  PUBLISHER = {Springer},
  NOTE = {This publication is available at
   
\url{
http://springerlink.metapress.com/openurl.asp?genre=article&issn=0302-9743&volum
e=3407&spage=463}
    {SpringerLink}
  },
  ABSTRACT = {
    We present a spatial and temporal logic based on Duration Calculus
    for the specification and verification of mobile real-time
    systems.  We demonstrate the use of the formalism and apply it to
    a case study. We extend a pure Duration Calculus specification for
    the controller by spatial assumptions to reason about spatial
    system properties. We prove that the formalism is undecidable in
    general for discrete and continuous domains and present a
    decidable fragment.
  }
}


@INPROCEEDINGS{nwpt04,
  AUTHOR = {I. Br{\"u}ckner},
  TITLE = {{Slicing CSP-OZ Specifications}},
  EDITOR = {P. Pettersson and W. Yi},
  BOOKTITLE = {Proceedings of the 16th Nordic Workshop on Programming Theory},
  SERIES = {Technical Reports of the Department of Information Technology},
  NUMBER = {2004-041},
  PUBLISHER = {Uppsala University, Sweden},
  ISSN = {1404-3203},
  PAGES = {71--73},
  YEAR = {2004},
  MONTH = {October},
  URL = {http://csd.informatik.uni-oldenburg.de/pub/Papers/ib04nwpt.pdf}
}


@INPROCEEDINGS{Die04b,
  AUTHOR = {H. Dierks},
  TITLE = {Heuristic Guided Model-Checking of Real-Time Systems},
  EDITOR = {P. Pettersson and Wang Yi},
  BOOKTITLE = {{Proceedings of the 16th Nordic Workshop on Programming Theory}},
  PAGES = {14--16},
  SERIES = {Technical Reports of the Department of Information Technology},
  NUMBER = {2004-041},
  PUBLISHER = {Uppsala University, Sweden},
  ISSN = {1404-3203},
  YEAR = {2004},
  MONTH = {October}
}


@INPROCEEDINGS{incose04,
  AUTHOR = {M. Bretschneider and H.-J. Holberg and E. B\"ode and I.
Br\"uckner 
    and T. Peikenkamp and H. Spenke},
  TITLE = {{Model-based Safety Analysis of a Flap Control System}},
  BOOKTITLE = {Proceedings of the 14th Annual International INCOSE Symposium
2004, Toulouse},
  EDITOR = {T. Fossnes and M. Galinier},
  MONTH = {June},
  YEAR = {2004},
  ABSTRACT = {
    Fault tree analysis is a widely adopted technique to
    systematically analyze causes for a given failure of a complex
    system. Traditionally, a fault tree is constructed top-down based
    on knowledge about the structure of the system and the interaction
    of subsystems. With the increasing system complexity and the
    accompanying introduction of model-based development techniques in
    the industrial process, a substantial amount of this knowledge is
    laid down in the system models. The main focus of the presented
    techniques and tools is to automatically exploit this knowledge by
    extracting a fault tree suitable for FaulTree+ directly from a
    given design modeled in Statemate. The resulting fault tree is
    complete wrt. the specified failure, i.e. the analysis considers
    every possible causal failure combination which is guaranteed by
    applying model checking techniques. Using an aircraft Flap control
    system this paper shows how to smoothly integrate the technique
    into an existing model-based process.
},
  URL = {http://csd.informatik.uni-oldenburg.de/pub/Papers/ib04ft.pdf}
}


@INPROCEEDINGS{DaHuOl04,
  AUTHOR = {W. Damm and H. Hungar and E.-R. Olderog},
  TITLE = {On the Verification of Cooperating Traffic Agents},
  BOOKTITLE = {FMCO 2003: Formal Methods for Components and Objects},
  YEAR = {2004},
  EDITOR = {F.S. de Boer and M.M. Bonsangue and S. Graf and W.-P. de Roever},
  VOLUME = {3188},
  PAGES = {77--110},
  SERIES = {LNCS},
  ABSTRACT = {
    This paper exploits design patterns employed in coordinating
    autonomous transport vehicles so as to ease the burden in
    verifying cooperating hybrid systems. The presented veri cation
    methodology is equally applicable for avionics applications (such
    as TCAS), train applications (such as ETCS), or automotive
    applications (such as platooning). We present a veri cation rule
    explicating the essence of employed design patters, guaranteeing
    global safety properties of the kind ``a collision will never
    occur'', and whose premises can either be established by o -line
    analysis of the worst-case behavior of the involved tra c agents,
    or by purely local proofs, involving only a single tra c agent. In
    a companion paper we will show, how such local proof obligations
    can be discharged automatically.
  }
}


@INPROCEEDINGS{Weh04,
  AUTHOR = {H. Wehrheim},
  TITLE = {Preserving properties under change},
  BOOKTITLE = {FMCO 2003: Formal Methods for Components and Objects},
  YEAR = {2004},
  EDITOR = {F.S. de Boer and M.M. Bonsangue and S. Graf and W.-P. de
Roever},
  VOLUME = {3188},
  PAGES = {330--343},
  SERIES = {LNCS}
}


@INCOLLECTION{FiWe04,
  AUTHOR = {C. Fischer and H. Wehrheim},
  EDITOR = {G. Paun and G. Rozenberg and A. Salomaa},
  TITLE = {{Failure-Divergence Semantics
  as a Formal Basis for an Object-Oriented Integrated Formal Method}},
  PUBLISHER = {World Scientific},
  YEAR = {2004},
  BOOKTITLE = {Current Trends in Theoretical Computer Science:  
  The Challenge of the New Century, Vol 2: Formal Models and
  Semantics}
}


@ARTICLE{mcp04,
  AUTHOR = {R. Buscherm\"ohle and M. Br\"orkens and I. Br\"uckner and 
W. Damm and W. Hasselbring and B. Josko and C. Schulte and T. Wolf},
  TITLE = {{Model Checking -- Grundlagen und Praxiserfahrungen}},
  JOURNAL = {Informatik Spektrum},
  EDITOR = {A. Bode},
  ISSN = {0170-6012},
  PUBLISHER = {Springer Verlag},
  VOLUME = {27},
  NUMBER = {2},
  PAGES = {146--158},
  MONTH = {April},
  YEAR = {2004},
  ABSTRACT = {
    The correct functioning of hard- and software components is often
    a crucial factor in computer-based system engineering.
    Particularly, this is the case in the area of 'safety critical'
    systems, where a system failure can endanger human life. But also
    in less critical areas the correctness of provided functionality
    becomes more and more important.  Furthermore the complexity of
    system functionality increases steadily.  Therefore manual test
    and simulation methods can detect many errors only with
    inaccaptable high effort concerning time and resources.  Starting
    from this background, this article presents the basics of 'model
    checking', an automatic and complete verification method.  Based
    on this introduction, experience gained with the application of
    model checking tools in industrial contexts is presented and
    discussed.
},
  URL = {http://csd.informatik.uni-oldenburg.de/pub/Papers/ib04mc.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},
}