Abstract
In this paper, we present a new automatic transformation algorithm called excommunication that transforms π-calculus processes to remove parallelism, and hence internal communication. We prove that the transformation is correct and that it always terminates for any specification in which the named processes are in a particular syntactic form we call serial form. We argue that this transformation facilitates the proving of properties of mobile processes, and demonstrate this by showing how it can be used to simplify a leakage analysis.
Original language | English |
---|---|
Title of host publication | Proceedings of the 25th Brazilian Symposium on Formal Methods |
Publisher | Springer |
Pages | 109-123 |
Number of pages | 15 |
ISBN (Electronic) | 9783031224768 |
ISBN (Print) | 9783031224751 |
DOIs | |
Publication status | Published - 1 Dec 2022 |
Event | 25th Brazilian Symposium on Formal Methods - Online Duration: 5 Dec 2022 → 9 Dec 2022 https://sites.google.com/dcomp.ufs.br/sbmf2022/home |
Publication series
Name | Lecture Notes in Computer Science |
---|---|
Publisher | Springer |
Volume | 13768 |
ISSN (Print) | 0302-9743 |
ISSN (Electronic) | 1611-3349 |
Conference
Conference | 25th Brazilian Symposium on Formal Methods |
---|---|
Abbreviated title | SBMF 2022 |
Period | 5/12/22 → 9/12/22 |
Internet address |
Keywords
- Formal Methods
- Pi Calculus
- Process Algebra
- Program Transformation
- Security