Applied Calculi

With increasing numbers of processor cores, cache coherence algorithms for globally consistent shared memory become very costly, and chip manufacturers (Cell, SCC) and systems builders (BarrelFish) instead turn towards using and implementing explicit message-passing. A successful means of modelling message-passing concurrent systems is process calculi,
miniature formal languages which enable formal reasoning about a system and its semantics.

When modelling real world problems in pure process calculi one soon discovers that the model becomes big and hard to understand due to a lack of more complex datatypes and constructs. To address this, several "applied" calculi have emerged, e.g. the spi-calculus and the applied pi-calculus. So far, they have mainly been used for verification of security protocols.

In an attempt to unify these extensions and to get simpler semantics we are developing a framework in which these extensions can be formulated. Since the meta-theory of applied process calculi is complicated and prone to errors, we formalize the theory in the theorem prover Isabelle/HOL-Nominal as it is being developed, thereby ensuring that the theory is indeed correct.

Developing formally verified theory and tool support for modelling message-passing systems and programs.

Much of this work will be generally applicable to a wide range of fields, but in the context of UPMARC the focus is on enabling the modelling and formal verification of multicore protocols and algorithms, ensuring the correctness of multicore systems.

A family of process calculi, with members that faithfully model interesting parallel communicating systems, and tool support for debugging and verifying aspects of such models.

• Development of theoretical frameworks for defining applied process calculi for modelling certain classes of message-passing systems.
• Formal verification of the meta-thory of the framework and the validity of definitions of calculi in the theorem prover Isabelle/Hol-Nominal.
• Validation of the framework by modelling interesting message-passing programs and systems.
• Development of tool support for simulation and equivalence proofs for models in calculi within the framework.

We have developed Psi-calculi, a framework for defining applied calculi. By instantiating three data types and four operators that must respect a handful of requirements we show that you get a process calculus that is compositional and respects the usual structural rules. The data types are terms (used for both communication channels and data), conditions (used for tests), and assertions (used for statements about data). The operators are channel equivalence (saying which terms are deemed to be equal channels), composition (saying how to compose assertions), unit (an assertion being the unit element of the composition operator), and entailment (saying which conditions can be entailed from which assertions).

Achievements

• The framework itself, some instantiations of it, and important meta-theoretical results about it (the validity of the standard structural congruence rules, and the compositionality of strong labelled bisimilarity) have all been machine-checked in Isabelle/HOL-Nominal.
  Psi-calculi in Isabelle. Jesper Bengtson and Joachim Parrow. In Theorem Proving in Higher Order Logics, volume 5674 of Lecture Notes in Computer Science, pp 99-114, Springer-Verlag, Berlin, 2009. (DOI).

  Psi-calculi: Mobile processes, nominal data, and logic. Jesper Bengtson, Magnus Johansson, Joachim Parrow, and Björn Victor. In Proc. 24th Annual IEEE Symposium on Logic in Computer Science, pp 39-48, IEEE, Piscataway, NJ, 2009. (DOI).
• The initial equivalence given for Psi-calculi is of the strong kind, i.e. it does not abstract from internal actions. We have defined a weak variant of Psi-calculi equivalence where certain internal actions are ignored, and thus we get a coarser equivalence that coincides with barbed equivalence. Much of this work has also been machine-checked.
  Weak Equivalences in Psi-calculi. Magnus Johansson, Jesper Bengtson, Joachim Parrow, and Björn Victor. In Proc. 25th Symposium on Logic in Computer Science: LICS 2010, pp 322-331, IEEE, Piscataway, NJ, 2010. (DOI).
• As defined, Psi-calculi are unsuitable for some kinds of automated reasoning; to overcome this we have developed a symbolic operational semantics for Psi-calculi, that is fully abstract with respect to the concrete one. This semantics also allows automated bisimulation checking for finite-state processes.
  Computing Strong and Weak Bisimulations for Psi-Calculi. Magnus Johansson, Björn Victor, and Joachim Parrow. In Journal of Logic and Algebraic Programming, volume 81, number 3, pp 162-180, Elsevier, 2012. (DOI).

  A Fully Abstract Symbolic Semantics for Psi-Calculi. Magnus Johansson, Björn Victor, and Joachim Parrow. In Proc. 6th Workshop on Structural Operational Semantics: SOS 2009, volume 18 of Electronic Proceedings in Theoretical Computer Science, pp 17-31, 2010. (DOI).
• The framework has been extended to model wireless broadcast communication, with machine-checked proofs of important meta-theoretical results. We have modelled a wireless ad-hoc routing algorithm (LUNAR). Presented at SEFM'11; a long version is in print.
  Broadcast psi-calculi with an application to wireless protocols. Johannes Borgström, Shuqin Huang, Magnus Johansson, Palle Raabjerg, Björn Victor, Johannes Åman Pohjola, and Joachim Parrow. In Software and Systems Modeling, volume 14, number 1, pp 201-216, Springer, 2015. (DOI, fulltext:postprint).

  Broadcast Psi-calculi with an Application to Wireless Protocols. Johannes Borgström, Shuqin Huang, Magnus Johansson, Palle Raabjerg, Björn Victor, Johannes Åman Pohjola, and Joachim Parrow. In Software Engineering and Formal Methods: SEFM 2011, volume 7041 of Lecture Notes in Computer Science, pp 74-89, Springer Berlin/Heidelberg, 2011. (DOI, fulltext:postprint).
• The framework has been extended to model higher-order communication, with machine-checked proofs of important meta-theoretical results. In addition to those results, we also have machine-checked proofs that we can lift any (first-order) Psi instance to an higher-order one, and that case statements and replication are encodable in such canonical higher-order instances.
  Higher-order psi-calculi. Joachim Parrow, Johannes Borgström, Palle Raabjerg, and Johannes Åman Pohjola. In Mathematical Structures in Computer Science, volume 24, number 2, Cambridge University Press, 2014. (DOI, fulltext:postprint).
• We have added sorting and generalised pattern-matching to the framework, in order to treat models where communication on transmitted data is important. This refinement also admits exact (strong operational) correspondences to value-passing CCS and standard pi-calculus extensions.
  A Sorted Semantic Framework for Applied Process Calculi (extended abstract). Johannes Borgström, Ramunas Gutkovas, Joachim Parrow, Björn Victor, and Johannes Åman Pohjola. In Trustworthy Global Computing: TGC 2013, volume 8358 of Lecture Notes in Computer Science, pp 103-118, Springer Berlin/Heidelberg, 2014. (DOI).
• A prototype modelling and pre-orderbased verification tool has been developed (see below).

Software

• Automated Psi instantiation: Framework in Isabelle for automated instantiation proofs for Psi. Master's thesis project of Johannes Åman Pohjola.
• A Psi Workbench. The tool contains functionality common to all instances of the psi-calculus, while the tool user starts by implementing the parameters of a psi-calculus instance in ML. Currently the tool provides computation of the symbolic transition graph of a process, and computation of logical conditions for bisimilarity of two processes. The symbolic transition constraints and the bisimulation constraints are solved by user-provided constraint solvers. One novelty is the support for both unicast and broadcast communication in the same model. The tool is in active development.
  A Parametric Tool for Applied Process Calculi. Johannes Borgström, Ramunas Gutkovas, Ioana Rodhe, and Björn Victor. In 13th International Conference on Application of Concurrency to System Design (ACSD 2013), International Conference on Application of Concurrency to System Design, pp 180-185, IEEE Computer Society, 2013. (DOI).

Publications

• Broadcast psi-calculi with an application to wireless protocols. Johannes Borgström, Shuqin Huang, Magnus Johansson, Palle Raabjerg, Björn Victor, Johannes Åman Pohjola, and Joachim Parrow. In Software and Systems Modeling, volume 14, number 1, pp 201-216, Springer, 2015. (DOI, fulltext:postprint).
• A Sorted Semantic Framework for Applied Process Calculi (extended abstract). Johannes Borgström, Ramunas Gutkovas, Joachim Parrow, Björn Victor, and Johannes Åman Pohjola. In Trustworthy Global Computing: TGC 2013, volume 8358 of Lecture Notes in Computer Science, pp 103-118, Springer Berlin/Heidelberg, 2014. (DOI).
• Higher-order psi-calculi. Joachim Parrow, Johannes Borgström, Palle Raabjerg, and Johannes Åman Pohjola. In Mathematical Structures in Computer Science, volume 24, number 2, Cambridge University Press, 2014. (DOI, fulltext:postprint).
• Program Analysis and Verification Based on Kleene Algebra in Isabelle/HOL. Alasdair Armstrong, Georg Struth, and Tjark Weber. In Interactive Theorem Proving: ITP 2013, volume 7998 of Lecture Notes in Computer Science, pp 197-212, Springer Berlin/Heidelberg, 2013. (DOI, fulltext:postprint).
• A Parametric Tool for Applied Process Calculi. Johannes Borgström, Ramunas Gutkovas, Ioana Rodhe, and Björn Victor. In 13th International Conference on Application of Concurrency to System Design (ACSD 2013), International Conference on Application of Concurrency to System Design, pp 180-185, IEEE Computer Society, 2013. (DOI).
• Kleene Algebra. Alasdair Armstrong, Georg Struth, and Tjark Weber. In Archive of Formal Proofs, 2013. (External link).
• The impact of trace and adversary models on location privacy provided by K-anonymity. Volkan Cambazoglu, Christian Rohner, and Björn Victor. In Proc. 1st Workshop on Measurement, Privacy, and Mobility, ACM Press, New York, 2012. (DOI).
• Computing Strong and Weak Bisimulations for Psi-Calculi. Magnus Johansson, Björn Victor, and Joachim Parrow. In Journal of Logic and Algebraic Programming, volume 81, number 3, pp 162-180, Elsevier, 2012. (DOI).
• Broadcast Psi-calculi with an Application to Wireless Protocols. Johannes Borgström, Shuqin Huang, Magnus Johansson, Palle Raabjerg, Björn Victor, Johannes Åman Pohjola, and Joachim Parrow. In Software Engineering and Formal Methods: SEFM 2011, volume 7041 of Lecture Notes in Computer Science, pp 74-89, Springer Berlin/Heidelberg, 2011. (DOI, fulltext:postprint).
• Maintaining Database Integrity with Refinement Types. Ioannis G. Baltopoulos, Johannes Borgström, and Andrew D. Gordon. In ECOOP 2011 – Object-Oriented Programming, volume 6813 of Lecture Notes in Computer Science, pp 484-509, Springer-Verlag, Berlin, 2011. (DOI).
• Verified Stateful Programs with Substructural State and Hoare Types. Johannes Borgström, Juan Chen, and Nikhil Swamy. In Proc. 5th ACM Workshop on Programming Languages Meets Program Verification, pp 15-26, ACM Press, New York, 2011. (DOI).
• Refinement types for secure implementations. Jesper Bengtson, Karthikeyan Bhargavan, Cédric Fournet, Andrew D. Gordon, and Sergio Maffeis. In ACM Transactions on Programming Languages and Systems, volume 33, number 2, pp 8:1-45, 2011. (DOI).
• Lower trees with fixed degrees: a recipe for efficient secure hierarchical aggregation in WSNs. Davor Sutic, Ioana Rodhe, Christian Rohner, and Björn Victor. In 2011 IEEE WIRELESS COMMUNICATIONS AND NETWORKING CONFERENCE (WCNC), pp 659-664, IEEE Computer Society, 2011. (DOI).
• Psi-calculi: a framework for mobile processes with nominal data and logic. Jesper Bengtson, Magnus Johansson, Joachim Parrow, and Björn Victor. In Logical Methods in Computer Science, volume 7, number 1, p 11, 2011. (DOI).
• Psi-calculi: a framework for mobile process calculi: Cook your own correct process calculus - just add data and logic. Magnus Johansson. Ph.D. thesis, Uppsala Dissertations from the Faculty of Science and Technology nr 94, Acta Universitatis Upsaliensis, Uppsala, 2010. (fulltext).
• Weak Equivalences in Psi-calculi. Magnus Johansson, Jesper Bengtson, Joachim Parrow, and Björn Victor. In Proc. 25th Symposium on Logic in Computer Science: LICS 2010, pp 322-331, IEEE, Piscataway, NJ, 2010. (DOI).
• A Fully Abstract Symbolic Semantics for Psi-Calculi. Magnus Johansson, Björn Victor, and Joachim Parrow. In Proc. 6th Workshop on Structural Operational Semantics: SOS 2009, volume 18 of Electronic Proceedings in Theoretical Computer Science, pp 17-31, 2010. (DOI).
• Formalising the ?-calculus using nominal logic. Jesper Bengtson and Joachim Parrow. In Logical Methods in Computer Science, volume 5, number 2, pp 16:1-36, 2009. (DOI, fulltext).
• Psi-calculi in Isabelle. Jesper Bengtson and Joachim Parrow. In Theorem Proving in Higher Order Logics, volume 5674 of Lecture Notes in Computer Science, pp 99-114, Springer-Verlag, Berlin, 2009. (DOI).
• Psi-calculi: Mobile processes, nominal data, and logic. Jesper Bengtson, Magnus Johansson, Joachim Parrow, and Björn Victor. In Proc. 24th Annual IEEE Symposium on Logic in Computer Science, pp 39-48, IEEE, Piscataway, NJ, 2009. (DOI).
• Re?nement Types for Secure Implementations. Jesper Bengtson, Karthikeyan Bhargavan, Cédric Fournet, Andrew D. Gordon, and Sergio Maffeis. In Proc. 21st IEEE Computer Security Foundations Symposium, pp 17-32, IEEE, Piscataway, NJ, 2008. (DOI, fulltext).
• Extended pi-Calculi. Magnus Johansson, Joachim Parrow, Björn Victor, and Jesper Bengtson. In Automata, Languages and Programming, PT 2: Proceedings of ICALP 2008, volume 5126 of Lecture Notes in Computer Science, pp 87-98, 2008. (DOI).
• Expressiveness of Process Algebras. Joachim Parrow. In Electronic Notes in Theoretical Computer Science, volume 209, pp 173-186, 2008. (DOI).

Presentations, PR, press clippings, awards

• Extended pi-calculi. Reykjavik, July 2008, at ICALP 2008. (presentation by Magnus Johansson)
• Verifying psi-calculi. Uppsala University, October 2008, master's thesis presentation. (presentation by Johannes Åman Pohjola )
• Three holy grails of programming models. KTH, May 2009, invited seminar. (presentation by Joachim Parrow )
• Psi-calculi: Mobile processes, nominal data, and logic. UCLA, July 2009, at LICS 2009 (presentation by Joachim Parrow )
• Psi-calculi in Isabelle. TU Munich, August 2009, at TPHOLs 2009. (presentation by Jesper Bengtson)
• A fully abstract symbolic semantics for psi-calculi. Bologna, August 2009, at SOS 2009. (presentation by Magnus Johansson)
• Three holy grails of programming models. Ecole Polytechnique, Paris, May 2009, invited seminar (presentation by Joachim Parrow )
• Concurrency: Semantics, models and proofs. Uppsala, March 2010, at the UPMARC review (presentation by Joachim Parrow )
• Psi-calculi. Cambridge, November 2010, at the MSRC type wrestling seminar. (presentation by Johannes Borgström )
• Weak equivalences in psi-calculi. Edinburgh, July 2010, at LICS 2010. (presentation by Björn Victor )
• Commemoration of Robin Milner. Perpignan, September 2010, invited talk at SAS 2010 (presentation by Joachim Parrow )
• Concurrency and Proofs. Gothenburgh, October 2010, part of the distinguished lecture series. (presentation by Joachim Parrow )
• Concurrency and Proofs. Turku, November 2010, invited talk at NWPT 2010. (presentation by Joachim Parrow )
• From pi to extended pi to Psi to extended Psi. Aalborg, November 2010. Seminar at Aalborg University. (presentation by Palle Raabjerg )
• Exercising Psi-calculi: A Psi-calculi Workbench. Uppsala University, June 2011, master's thesis presentation. (presentation by Ramunas Gutkovas )
• Shortest ever talk on the Psi-calculus. Bayrischzell, August 2011. Student talk at International Summer School Marktoberdorf. (presentation by Palle Raabjerg )
• Applied process calculi made easy as pi. Aachen, September 2011, invited talk at EXPRESS'11 (presentation by Björn Victor )
• Psi-calculi: mobile processes from nominal data and logic. Edinburgh, November 2011, talk at the LFCS lunch seminar (presentation by Johannes Borgström )
• Broadcast Psi-calculi with an application to wireless protocols. Montevideo, November 2011, presentation at SEFM 2011 Björn Victor and Johannes Åman Pohjola).
• The pi-calculus: Origin and recent development. Edinburgh, April 2012, invited talk at the Robin Milner memorial symposium. (presentation by Joachim Parrow)
• A Parametric Tool for Applied Process Calculi: Psi-Calculi Workbench. Barcelona, July 2013, presentation at ACSD 2013 by Ramunas Gutkovas
• A Sorted Semantic Framework for Applied Process Calculi. Buenos Aires, September 2013, presentation at TGC 2013 by Björn Victor

Senior: Joachim Parrow (Contact), Björn Victor, Tjark Weber
Research Fellow: Johannes Borgström
Ph.D. students: Palle Raabjerg, Johannes Åman Pohjola, Ramunas Gutkovas
Earlier contributors: Jesper Bengtson, Shuqin Huang, Magnus Johansson, Amin KhorsandiAghai