Dipl.-Inform. Roland Meyer

 

1 Publications (BibTeX Source)

@TECHREPORT{KhomenkoMeyer2008ComplexityStructCong,
  AUTHOR = {V. Khomenko and R. Meyer},
  TITLE = {Checking $\pi$-Calculus Structural Congruence is Graph Isomorphism Complete},
  NUMBER = {CS-TR: 1100},
  INSTITUTION = {School of Computing Science, Newcastle University},
  YEAR = {2008},
  NOTE = {20 pages},
  URL = {http://www.cs.ncl.ac.uk/publications/trs/abstract/1100},
  KEYWORDS = {structural congruence, graph isomorphism, $\pi$-Calculus, computational
complexity},
  ABSTRACT = {We show that the problems of checking $\pi$-Calculus structural congruence
($\pi$SC) and graph isomorphism (GI) are Karp reducible to each other. The reduction
from GI to $\pi$SC is given explicitly, and the reduction in the opposite direction proceeds
by transforming $\pi$SC into an instance of the term equality problem (i.e., the problem
of deciding equivalence of two terms in the presence of associative and/or commutative
operations and commutative variable-binding quantifiers), which is known to be Karp
reducible to GI. Our result is robust in the sense that it holds for several variants of
structural congruence and some rather restrictive fragments of $\pi$-Calculus. 
Furthermore, we address the question of solving $\pi$SC in practice, and describe a number
of optimisations exploiting specific features of $\pi$-Calculus terms, which allow one to
significantly reduce the size of the resulting graphs that have to be checked for isomorphism.}
}


@ARTICLE{Meyer2008,
  AUTHOR = {R. Meyer and J. Faber and J. Hoenicke and A. Rybalchenko},
  TITLE = {Model Checking Duration Calculus: A Practical Approach},
  JOURNAL = {Formal Aspects of Computing},
  YEAR = {2008},
  PUBLISHER = {Springer London},
  VOLUME = {20},
  PAGES = {481--505},
  NUMBER = {4--5},
  MONTH = JUL,
  NOTE = {{ISSN} 0934-5043 (Print) 1433-299X (Online)},
  ABSTRACT = {Model checking of real-time systems against Duration Calculus (DC)
	specifications requires the translation of DC formulae into automata-based
	semantics. 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 realistic applications. Our algorithm significantly extends the
	subset of DC that can be checked automatically. The central part
	of the algorithm is the automatic decomposition of DC specifications
	into sub-properties that can be verified independently. The decomposition
	is based on a novel distributive law for DC. We implemented the algorithm
	in a tool chain for the automated verification of systems comprising
	data, communication, and real-time aspects. We applied the tool chain
	to verify safety properties in an industrial case study from the
	European Train Control System (ETCS).},
  DOI = {10.1007/s00165-008-0082-7},
  ISSN = {0934-5043},
  KEYWORDS = {Model checking, Verification, Duration Calculus, Timed automata, Real-time
	systems, European Train Control System, Case study},
  URL = {http://www.springerlink.com/content/81g876074077601g/fulltext.pdf},
}


@INPROCEEDINGS{Meyer2008BoundedDepth,
  AUTHOR = {R. Meyer},
  TITLE = {On Boundedness in Depth in the $\pi$-Calculus},
  BOOKTITLE = {Proc. of the 5th IFIP International
Conference on Theoretical Computer Science, IFIP TCS 2008},
  SERIES = {IFIP},
  VOLUME = {273},
  PUBLISHER = {Springer-Verlag},
  YEAR = {2008},
  PAGES = {},
  NOTE = {To appear},
  KEYWORDS = {$\pi$-Calculus, structural congruence, well-structured transition
systems, termination},
  ABSTRACT = {
We investigate the class $P_{\mathit{BD}}$ of $\pi$-Calculus processes that are
bounded in the function depth. First, we show that boundedness in depth has an
intuitive characterisation when we understand processes as graphs: a process is
bounded in depth if and only if the length of the simple paths is bounded. The
proof is based on a new normal form for the $\pi$-Calculus called anchored
fragments. Using this concept, we then show that processes of bounded depth have
well-structured transition systems (WSTS). As a consequence, the termination
problem is decidable for this class of processes. The instantiation of the WSTS
framework employs a new well-quasi-ordering for processes in $P_{\mathit{BD}}$.}
}


@INPROCEEDINGS{MeyerKhomenkoStrazny2008Unfolding,
  AUTHOR = {R. Meyer and V. Khomenko and T. Strazny},
  TITLE = {A Practical Approach to Verification of Mobile Systems Using Net Unfoldings},
  BOOKTITLE = {Proc. of the 29th International Conference on Application and Theory of Petri Nets and Other Models of Concurrency, ATPN 2008},
  SERIES = {LNCS},
  VOLUME = {5062},
  PUBLISHER = {Springer-Verlag},
  NOTE = {To appear},
  YEAR = {2008},
  KEYWORDS = {finite control processes, safe processes, $\pi$-Calculus, mobile
systems, model checking, Petri net unfoldings},
  ABSTRACT = {
In this paper we propose a technique for verification of mobile
systems.We translate finite control processes, which are a well-known
subset of $\pi$-Calculus, into Petri nets, which are subsequently used for
model checking. This translation always yields bounded Petri nets with
a small bound, and we develop a technique for computing a non-trivial
bound by static analysis. Moreover, we introduce the notion of safe pro-
cesses, which are a subset of finite control processes, for which our
translation
yields safe Petri nets, and show that every finite control process can
be translated into a safe one of at most quadratic size. This gives a
possibility
to translate every finite control process into a safe Petri net, for
which efficient unfolding-based verification is possible. Our experiments
show that this approach has a significant advantage over other existing
tools for verification of mobile systems in terms of memory consumption
and runtime.}
}


@TECHREPORT{MeyerKhomenkoStrazny2008UnfoldingTR,
  AUTHOR = {R. Meyer and V. Khomenko and T. Strazny},
  TITLE = {A Practical Approach to Verification of Mobile Systems Using Net
Unfoldings},
  INSTITUTION = {School of Computing Science, Newcastle University},
  MONTH = {January},
  YEAR = {2008},
  NUMBER = {CS-TR: 1064},
  NOTE = {29 pages},
  KEYWORDS = {finite control processes, safe processes, $\pi$-Calculus, mobile
systems, model checking, Petri net unfoldings},
  ABSTRACT = {
In this paper we propose a technique for verification of mobile
systems.We translate finite control processes, which are a well-known
subset of $\pi$-Calculus, into Petri nets, which are subsequently used for
model checking. This translation always yields bounded Petri nets with
a small bound, and we develop a technique for computing a non-trivial
bound by static analysis. Moreover, we introduce the notion of safe pro-
cesses, which are a subset of finite control processes, for which our
translation
yields safe Petri nets, and show that every finite control process can
be translated into a safe one of at most quadratic size. This gives a
possibility
to translate every finite control process into a safe Petri net, for
which efficient unfolding-based verification is possible. Our experiments
show that this approach has a significant advantage over other existing
tools for verification of mobile systems in terms of memory consumption
and runtime.
}
}


@INPROCEEDINGS{Meyer2007Dagstuhl,
  AUTHOR = {R. Meyer},
  TITLE = {{A Petri Net Semantics for $\pi$-Calculus Verification}},
  BOOKTITLE = {Dagstuhl ''zehn plus eins''},
  PAGES = {76--77},
  YEAR = {2007},
  PUBLISHER = {Verlagshaus Mainz GmbH Aachen},
}


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


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