tr.bib

@TECHREPORT{sidorova.steffen:mascaracontrol,
  AUTHOR = {Natalia Sidova and Martin Steffen},
  TITLE = {Verifying {M}ascara {C}ontrol},
  INSTITUTION = {Lehrstuhl f{\"ur} Software-Technologie,
                    Institut f{\"u}r Informatik und praktische Mathematik,
                    Christian-Albrechts-Universit{\"a}t Kiel},
  YEAR = 2000,
  TYPE = {Technical Report},
  NUMBER = {TR-ST-00-1},
  MONTH = MAY,
  URL = {http://www.informatik.uni-kiel.de/inf/deRoever/techreports/00/tr-st-00-1.ps.gz},
  ABSTRACT = {This  document reports on a series of verification experiments on the
                  control-part of Mascara, a medium-access protocol for
                  wireless ATM-networks.}
}

@TECHREPORT{dams.lakhnech.steffen:accelerating,
  AUTHOR = {Dennis Dams and Yassine Lakhnech and Martin Steffen},
  TITLE = {Iterating Transducers for Safety of Abstraction},
  INSTITUTION = {Christian-Albrechts-Universit{\"a}t, Lehrstuhl
                  Softwaretechnologie},
  YEAR = 2000,
  TYPE = {Technical Report},
  NUMBER = {TR-ST-00-2},
  MONTH = MAY,
  URL = {http://www.informatik.uni-kiel.de/inf/deRoever/techreports/00/tr-st-00-2.ps.gz},
  ABSTRACT = {  Regular languages have proved useful for the symbolic
                  state exploration of infinite state systems. Regular
                  languages can be used to represent infinite sets of
                  system configurations, the transitional semantics of the
                  system consequently can be modeled by finite-state
                  transducers.  A standard problem encountered when doing
                  symbolic state exploration for infinite state systems is,
                  how to explore all states in a finite amount of time. 
  
                  When representing the one-step transition relation of a
                  system by a finite-state transducer $\mathcal{T}$, this problem
                  boils down to finding a finite-state representation for
                  $\mathcal{T}^*$, capturing the transitive closure of the
                  one-step reduction relation.  
  
                  In this paper we give a semi-algorithm to compute
                  $\mathcal{T}^*$.  The construction is based on building a
                  quotient of an infinite-state representation, where the
                  quotienting uses \emph{past} and \emph{future}
                  bisimulations computed on finite approximations of
                  $\mathcal{T}^*$.  As in general, $\mathcal{T}^*$ is not representable
                  by a finite-state transducer, the construction may not terminate.}
}

@TECHREPORT{sidorova.steffen:atm-verification-report,
  AUTHOR = {Natalia Sidorova and Martin Steffen},
  TITLE = {Verification of a Wireless {ATM} Medium-Access Protocol},
  INSTITUTION = {Lehrstuhl f{\"ur} Software-Technologie,
                    Institut f{\"u}r Informatik und praktische Mathematik,
                    Christian-Albrechts-Universit{\"a}t Kiel},
  YEAR = 2000,
  TYPE = {Technical Report},
  NUMBER = {TR-ST-00-3},
  MONTH = MAY,
  URL = {http://www.informatik.uni-kiel.de/inf/deRoever/techreports/00/tr-st-00-3.ps.gz},
  ABSTRACT = {In this paper we report on a model-checking case study of
                  an industrial medium-access protocol for wireless ATM.
                  Since the protocol is too large to be verified by any of
                  existing checkers as a whole, the verification exploits
                  the layered and modular structure of the protocol's
                  SDL specification and proceeds in a bottom-up,
                  compositional way. The compositional arguments are used
                  in combination with abstraction techniques to further
                  reduce the state space of the system. The verification is
                  primarily aimed at debugging the system.  After
                  correcting the specification step by step and validating
                  various untimed and time-dependent properties, a model of
                  the whole control component of the medium-access protocol
                  is built and verified. The significance of the case study
                  is in demonstrating that verification tools can handle
                  complex properties of a model as large as shown.}
}

@TECHREPORT{baukus.lakhnech.stahl:universal-report,
  AUTHOR = {Kai Baukus and Yassine Lakhnech and Karsten Stahl},
  TITLE = {Verifying Universal Properties of Parameterized Networks
                  (full paper)},
  INSTITUTION = {Lehrstuhl f{\"ur} Software-Technologie,
                    Institut f{\"u}r Informatik und praktische Mathematik,
                    Christian-Albrechts-Universit{\"a}t Kiel},
  YEAR = {2000},
  TYPE = {Technical Report},
  NUMBER = {TR-ST-00-4},
  MONTH = JUL,
  URL = {http://www.informatik.uni-kiel.de/inf/deRoever/techreports/00/tr-st-00-4.ps.gz},
  ABSTRACT = {In this paper, we present a method for the verification
                  of so-called \emph{universal} properties of fair
                  parameterized networks of similar processes, that is,
                  properties of the form $\forall p_1\dots p_n:\psi$, where
                  $\psi$ is a quantifier-free LTL formula. To prove an
                  universal property of a parameterized network, we first
                  model the infinite family of networks by a single fair
                  WS1S transition system, that is, a transition system
                  whose variables are set (2nd-order) variables and whose
                  transitions are described in WS1S. Then, we abstract the
                  WS1S system into a finite state system that can be
                  model-checked. We present a generic abstraction relation
                  for verifying universal properties as well as an
                  algorithm for computing an abstract system. However, the
                  abstract system may contain infinite computations that
                  have no corresponding fair computations at the concrete
                  level, and hence, in case the property of interest is a
                  progress property, verification may fail because of
                  this. Therefore, we present methods that allow to
                  synthesize fairness conditions from the parameterized
                  network and discuss under which conditions and how to
                  lift fairness conditions of this network to fairness
                  conditions on the abstract system. We implemented our
                  methods in a tool, called {PAX}, and applied it to several
                  examples.}
}