MobilityReadingGroup

A Theory of Design-by-Contract for Distributed Multiparty Interactions

Laura BOCCHI, Kohei HONDA, Emilio TUOSTO, Nobuko YOSHIDA

Design by Contract (DbC) promotes reliable software development through elaboration of type signatures for sequential programs with logical predicates. This paper presents an assertion method, based on the π-calculus with full recursion, which generalises the notion of DbC to multiparty distributed interactions to enable effective specification and verification of distributed multiparty protocols. Centring on global assertions and their projections onto endpoint assertions, our method allows clear specifications for typed sessions, constraining the content of the exchanged messages, the choice of sub-conversations to follow, and invariants on recursions. The paper presents key theoretical foundations of this framework, including a sound and relatively complete compositional proof system for verifying processes against assertions.

@inproceedings{BHTY2010,
  author = {Laura Bocchi and Kohei Honda and Emilio Tuosto and Nobuko Yoshida},
  title = {{A Theory of Design-by-Contract for Distributed Multiparty Interactions}},
  booktitle = {21th International Conference on Concurrency Theory},
  series = {LNCS},
  volume = {6269},
  pages = {162--176},
  publisher = {Springer},
  year = 2010
}

@inproceedings{BHTY2010,
  author = {Laura Bocchi and Kohei Honda and Emilio Tuosto and Nobuko Yoshida},
  title = {{A Theory of Design-by-Contract for Distributed Multiparty Interactions}},
  booktitle = {21th International Conference on Concurrency Theory},
  series = {LNCS},
  volume = {6269},
  pages = {162--176},
  publisher = {Springer},
  doi = "10.1007/978-3-642-15375-4",
  year = 2010
}