tr.bib

@TECHREPORT{lukoschus:comp-veri-ces,
  AUTHOR = {Ben Lukoschus},
  TITLE = {Composition and Verification of Condition/Event Systems},
  INSTITUTION = {Lehrstuhl f{\"ur} Software-Technologie,
                    Institut f{\"u}r Informatik und Praktische Mathematik,
                    Christian-Albrechts-Universit{\"a}t zu Kiel},
  YEAR = 1999,
  TYPE = {Technical Report},
  NUMBER = {TR-ST-99-1},
  MONTH = MAY,
  URL = {http://www.informatik.uni-kiel.de/inf/deRoever/techreports/99/tr-st-99-1.ps.gz},
  ABSTRACT = {We consider different ways of combining discrete and
                  timed condition/event systems (CESs) in a modular,
                  compositional way. In addition to the
                  interconnection operators for CESs found in the
                  literature, we introduce a new, powerful operator,
                  called parallel interconnection operator, which
                  allows arbitrary connections among a set of CESs. An
                  extensive example shows various possibilities how to
                  verify properties of a system consisting of some
                  interconnected CESs. We conclude this work by
                  showing how a set of interconnected discrete CESs
                  can be transformed into the input language of the
                  model checking tool SMV. This offers another
                  possibility to apply formal verification to
                  condition/event systems.}
}

@TECHREPORT{lukoschus:abstract-model-cs1,
  AUTHOR = {Ben Lukoschus},
  TITLE = {An Abstract Model of {VHS} Case Study 1
                  (Experimental Batch Plant)},
  INSTITUTION = {Lehrstuhl f{\"ur} Software-Technologie,
                    Institut f{\"u}r Informatik und Praktische Mathematik,
                    Christian-Albrechts-Universit{\"a}t zu Kiel},
  YEAR = 1999,
  TYPE = {Technical Report},
  NUMBER = {TR-ST-99-2},
  MONTH = MAY,
  URL = {http://www.informatik.uni-kiel.de/inf/deRoever/techreports/99/tr-st-99-2.ps.gz},
  ABSTRACT = {In this work we describe the verification of safety
                  properties for the experimental batch plant of case
                  study 1 using the model checker SMV. Discrete
                  condition/event systems are used to describe the
                  physical parts of the plant and the control
                  programs. This model is transformed into SMV code,
                  and the properties are checked.}
}