A Practical Approach to Verification of Mobile Systems Using Net Unfoldings
A Practical Approach to Verification of Mobile Systems Using Net Unfoldings
复制标题
DOI：
10.3233/fi-2009-138
复制
发表时间：
2008-06
期刊：
影响因子：
--
通讯作者：
R. Meyer;Victor Khomenko;T. Strazny
中科院分区：
文献类型：
--
作者：
R. Meyer;Victor Khomenko;T. Strazny
我们提出了一种技术验证的移动的系统。我们翻译有限控制过程，一个众所周知的子集π演算，到Petri网，随后用于模型检验。这种翻译总是产生一个小的界限有界Petri网，我们开发了一种技术，用于计算一个非平凡的静态分析的范围。此外，我们引入了安全过程的概念，有限控制过程的一个子集，我们的翻译产生安全的Petri网，并表明，每一个有限的控制过程可以被翻译成一个安全的最二次大小。这使得将每个有限控制过程转换为安全的Petri网成为可能，从而可以进行有效的基于展开的验证。我们的实验表明，这种方法有一个显着的优势，在内存消耗和运行时间方面的其他现有的工具验证的移动的系统。我们还证明了我们的方法的自动化制造系统的现实模型的适用性。
We propose a technique for verification of mobile systems. We translate finite control processes, a well-known subset of π-Calculus, into Petri nets, which are subsequently used formodel 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, 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.