Types as models, model checking message-passing programs. Abstraction and composition are the fundamental issues in making model checking viable for software. This paper proposes new techniques for automating abstraction and decomposition using source level type information provided by the programmer. Our system includes two novel components to achieve this end: (1) a behavioral type-and-effect system for the π-calculus, which extracts sound models as types, and (2) an assume-guarantee proof rule for carrying out compositional model checking on the types. Open simulation between CCS processes is used as both the subtyping relation in the type system and the abstraction relation for compositional model checking. We have implemented these ideas in a tool – PIPER. PIPER exploits type signatures provided by the programmer to partition the model checking problem, and emit model checking obligations that are discharged using the SPIN model checker. We present the details on applying PIPER on two examples: (1) the SIS standard for managing trouble tickets across multiple organizations and (2) a file reader from the pipelined implementation of a web server.

This software is also peer reviewed by journal TOMS.

References in zbMATH (referenced in 28 articles )

Showing results 1 to 20 of 28.
Sorted by year (citations)

1 2 next

  1. Degano, Pierpaolo; Ferrari, Gian-Luigi; Mezzetti, Gianluca: Regular and context-free nominal traces (2017)
  2. Gay, Simon J.; Gesbert, Nils; Ravara, António; Vasconcelos, Vasco T.: Modular session types for objects (2015)
  3. Laneve, Cosimo; Padovani, Luca: An algebraic theory for web service contracts (2015)
  4. Giachino, Elena; Laneve, Cosimo: Deadlock detection in linear recursive programs (2014)
  5. Caires, Luís; Seco, João C.: The type discipline of behavioral separation (2013)
  6. Acciai, Lucia; Boreale, Michele: Deciding safety properties in infinite-state pi-calculus via behavioural types (2012)
  7. Padovani, Luca: On projecting processes into session types (2012)
  8. Ravara, António; Resende, Pedro; Vasconcelos, Vasco T.: An algebra of behavioural types (2012)
  9. Lapadula, A.; Pugliese, R.; Tiezzi, F.: A WSDL-based type system for asynchronous WS-BPEL processes (2011)
  10. Acciai, Lucia; Boreale, Michele: Spatial and behavioral types in the pi-calculus (2010)
  11. Caires, Luís; Vieira, Hugo Torres: Conversation types (2010)
  12. Caires, Luís: Spatial-behavioral types for concurrency and resource control in distributed systems (2008)
  13. Iwama, Futoshi; Kobayashi, Naoki: A new type system for JVM lock primitives (2008)
  14. Kobayashi, Naoki; Sangiorgi, Davide: A hybrid type system for lock-freedom of mobile processes (2008)
  15. Caires, Luís: Spatial-behavioral types, distributed services, and resources (2007)
  16. Lapadula, Alessandro; Pugliese, Rosario; Tiezzi, Francesco: A calculus for orchestration of web services (2007)
  17. Vasconcelos, Vasco T.; Gay, Simon J.; Ravara, António: Type checking a multithreaded functional language with session types (2006)
  18. Bonelli, Eduardo; Compagnoni, Andriana; Gunter, Elsa: Correspondence assertions for process synchronization in concurrent communications (2005)
  19. Gay, Simon; Hole, Malcolm: Subtyping for session types in the pi calculus (2005)
  20. Naik, Mayur; Palsberg, Jens: A type system equivalent to a model checker (2005)

1 2 next