Paper Details

Communicating Process Architectures (CPA)
 Title: Verifying Mobile Systems: Take Two
 Conference: Communicating Process Architectures 2018
 Authors: Frédéric Peschanski
Sorbonne University
 Abstract: This papers relates the design and development of two “proof of concept” analysis tools for the pi-calculus. The main functionality of the first tool, named PiEx- plorer, is to construct the state-space of a finitary pi-calculus process as a directed graph akin to a finite-state automaton. As counterintuitive as it may seem, this is a rather complex objective. The second tool is an implementation of the main pi-calculus features (especially name-passing) in the Promela language. This enables the use of the Spin model checker for the verification task. Although very different, these two prototypes share a common foundation: a notion of a stateful observer for pi-calculus processes. This is the central idea discussed in the paper. 
Files:


BibTeX Entry


Full paper