Jun.-Prof. Dr. Roland Meyer

 

1 Publications (with abstracts)

[MS10]

R. Meyer and T. Strazny. Petruchio: From dynamic networks to nets. In Tayssir Touili, Byron Cook, and Paul Jackson, editors, Proceedings of the 22nd International Conference on Computer Aided Verification 2010, CAV 2010, volume 6174 of LNCS, pages 175-179. Springer-Verlag, 2010.
[ bib ]

We introduce Petruchio, a tool for computing Petri net translations of dynamic networks. To cater for unbounded architectures beyond the capabilities of existing implementations, the principle fixed-point engine runs interleaved with coverability queries. We discuss algorithmic enhancements and provide experimental evidence that Petruchio copes with models of reasonable size.

[OM09]

E.-R. Olderog and R. Meyer. Automata-theoretic verification based on counterexample specification. In V. Diekert, K. Weicker, and N. Weicker, editors, Informatik als Dialog zwischen Theorie und Anwendung, pages 217-225. Vieweg-Teubner, 2009.
[ bib ]

[KM08]

V. Khomenko and R. Meyer. Checking π-calculus structural congruence is graph isomorphism complete. Technical Report CS-TR: 1100, School of Computing Science, Newcastle University, 2008. 20 pages.
[ bib | http ]

We show that the problems of checking π-Calculus structural congruence (πSC) and graph isomorphism (GI) are Karp reducible to each other. The reduction from GI to πSC is given explicitly, and the reduction in the opposite direction proceeds by transforming π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 π-Calculus. Furthermore, we address the question of solving πSC in practice, and describe a number of optimisations exploiting specific features of π-Calculus terms, which allow one to significantly reduce the size of the resulting graphs that have to be checked for isomorphism.

Keywords: structural congruence, graph isomorphism, π-Calculus, computational complexity

[MFHR08]

R. Meyer, J. Faber, J. Hoenicke, and A. Rybalchenko. Model checking duration calculus: A practical approach. Formal Aspects of Computing, 20(4-5):481-505, July 2008. ISSN 0934-5043 (Print) 1433-299X (Online).
[ bib | .pdf ]

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).

Keywords: Model checking, Verification, Duration Calculus, Timed automata, Real-time systems, European Train Control System, Case study

[Mey08]

R. Meyer. On boundedness in depth in the π-calculus. In Proc. of the 5th IFIP International Conference on Theoretical Computer Science, IFIP TCS 2008, volume 273 of IFIP. Springer-Verlag, 2008. To appear.
[ bib ]

We investigate the class P_BD of π-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 π-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_BD.

Keywords: π-Calculus, structural congruence, well-structured transition systems, termination

[MKS09]

R. Meyer, V. Khomenko, and T. Strazny. A practical approach to verification of mobile systems using net unfoldings. Fundamenta Informaticae, 94(3-4):439-471, 2009. Special Issue on Petri Nets 2008, invited version of the ATPN 2008 paper.
[ bib ]

We propose a technique for verification of mobile systems. We translate finite control processes, which are a well-known subset of , 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 processes, 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. We also demonstrate the applicability of our method on a realistic model of an automated manufacturing system.

Keywords: finite control processes, safe processes, π-Calculus, mobile systems, model checking, Petri net unfoldings

[MKS08a]

R. Meyer, V. Khomenko, and T. Strazny. A practical approach to verification of mobile systems using net unfoldings. In Proc. of the 29th International Conference on Application and Theory of Petri Nets and Other Models of Concurrency, ATPN 2008, volume 5062 of LNCS, pages 327-347. Springer-Verlag, 2008.
[ bib ]

In this paper we propose a technique for verification of mobile systems.We translate finite control processes, which are a well-known subset of π-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.

Keywords: finite control processes, safe processes, π-Calculus, mobile systems, model checking, Petri net unfoldings

[MKS08b]

R. Meyer, V. Khomenko, and T. Strazny. A practical approach to verification of mobile systems using net unfoldings. Technical Report CS-TR: 1064, School of Computing Science, Newcastle University, January 2008. 29 pages.
[ bib ]

In this paper we propose a technique for verification of mobile systems.We translate finite control processes, which are a well-known subset of π-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.

Keywords: finite control processes, safe processes, π-Calculus, mobile systems, model checking, Petri net unfoldings

[Mey07]

R. Meyer. A Petri Net Semantics for π-Calculus Verification. In Dagstuhl ''zehn plus eins'', pages 76-77. Verlagshaus Mainz GmbH Aachen, 2007.
[ bib ]

[MFR06]

R. Meyer, J. Faber, and A. Rybalchenko. Model checking duration calculus: A practical approach. In K. Barkaoui, A. Cavalcanti, and A. Cerone, editors, Theoretical Aspects of Computing - ICTAC 2006, volume 4281 of LNCS, pages 332-346, 2006. This publication is available at SpringerLink.
[ bib | .pdf ]

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).

[Mey06a]

R. Meyer. Model checking the π-calculus. In Proceedings of the International Research Training Groups Workshop, volume 3 of Trustworthy Software Systems, page 15. GITO, 2006.
[ bib ]

[FM06]

J. Faber and R. Meyer. Model checking data-dependent real-time properties of the european train control system. In Formal Methods in Computer Aided Design, 2006. FMCAD '06, pages 76-77. IEEE Computer Society Press, November 2006. This publication is available free of charge at IEEE Digital Library.
[ bib ]

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.

[Mey06b]

R. Meyer. Model checking using testing. In W. Hasselbring and S. Giesecke, editors, Dependability Engineering, volume 2 of Trustworthy Software Systems, pages 147-171. GITO, 2006.
[ bib ]

[EFM⁺05]

C. Eichner, H. Fleischhack, R. Meyer, U. Schrimpf, and C. Stehno. Compositional semantics for uml 2.0 sequence diagrams using petri nets. In SDL 2005: Model Driven, volume 3530 of LNCS, pages 133-148. Springer-Verlag, 2005.
[ bib ]