The Psi-Calculi Workbench: A Generic Tool for Applied Process Calculi
2015 (English)In: ACM Transactions on Embedded Computing Systems, ISSN 1539-9087, E-ISSN 1558-3465, Vol. 14, no 1, 9Article in journal (Refereed) Published
Psi-calculi is a parametric framework for extensions of the pi-calculus with arbitrary data and logic. All instances of the framework inherit machine-checked proofs of the metatheory such as compositionality and bisimulation congruence. We present a generic analysis tool for psi-calculus instances, enabling symbolic execution and (bi)simulation checking for both unicast and broadcast communication. The tool also provides a library for implementing new psi-calculus instances. We provide examples from traditional communication protocols and wireless sensor networks. We also describe the theoretical foundations of the tool, including an improved symbolic operational semantics, with additional support for scoped broadcast communication.
Place, publisher, year, edition, pages
2015. Vol. 14, no 1, 9
Research subject Computer Science
IdentifiersURN: urn:nbn:se:uu:diva-233750DOI: 10.1145/2682570ISI: 000349302200009OAI: oai:DiVA.org:uu-233750DiVA: diva2:754138
FunderSwedish Foundation for Strategic Research , RIT080065