Model Checker for SOA systems modeled in the Conversation Calculus

Version 2.01 supports the specification of systems using the Conversation Calculus, a model for dynamic multiparty service-oriented applications introduced by Vieira, Caires and Seco. This extension to the tool allows to model-check Conversation Calculus specifications against dynamic spatial logic properties. The development of this extension of the tool was supported by IP Sensoria (EU IST FP6).