zbMATH — the first resource for mathematics

Parameterized verification of \(\pi\)-calculus systems. (English) Zbl 1180.68181
Hermanns, Holger (ed.) et al., Tools and algorithms for the construction and analysis of systems. 12th international conference, TACAS 2006, held as part of the joint European conferences on theory and practice of software, ETAPS 2006, Vienna, Austria, March 25 – April 2, 2006. Proceedings. Berlin: Springer (ISBN 3-540-33056-9/pbk). Lecture Notes in Computer Science 3920, 42-57 (2006).
Summary: In this paper we present an automatic verification technique for parameterized systems where the subsystem behavior is modeled using the \(\pi\)-calculus. At its core, our technique treats each process instance in a system as a property transformer. Given a property \(\varphi\) that we want to verify of an \(N\)-process system, we use a partial model checker to infer the property \(\varphi'\) (stated as a formula in a sufficiently rich logic) that must hold of an \((N-1)\)-process system. If the sequence of formulas \(\varphi\), \(\varphi', \dots\) thus constructed converges, and the limit is satisfied by the deadlocked process, we can conclude that the \(N\)-process system satisfies \(\varphi\). To this end, we develop a partial model checker for the \(\pi\)-calculus that uses an expressive value-passing logic as the property language. We also develop a number of optimizations to make the model checker efficient enough for routine use, and a light-weight widening operator to accelerate convergence. We demonstrate the effectiveness of our technique by using it to verify properties of a wide variety of parameterized systems that are beyond the reach of existing techniques.
For the entire collection see [Zbl 1103.68005].

68Q60 Specification and verification (program logics, model checking, etc.)
68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
Full Text: DOI