• London Software Systems (Imperial College London and University College London)
  
• Contact:
• www.sensoria-ist.eu/wse

• LocUsT Model Checker - The LocUsT tool is a model checker which verifies safety properties on the behaviour of services. LocUsT is used both as a static checker of usage policies, and as a verification core for the call-by-contract service orchestration framework developed within SENSORIA.
  

• Università di Trento, Università di Pisa
  
• Contact:

• The SocL Logical Framework -  SocL is a service-oriented logical framework (logic + verification engine) with the following characteristics: The logic is an efficiently verifiable, state- and event-based, parametric, branching-time temporal logic which allows to naturally express typical service-oriented properties like session data correlation, service availability, and service responsiveness. Its verification engine is an on-the fly verification engine which uses a bounded model-checking approach for the verification of formulas also on infinite models, which generates “on demand” only the needed fragment of the overall state space, and which abstracts from the internal details of the underlying computational model by just viewing it as an abstract doubly-labelled structure.

• CMC-UMC - CMC and UMC are two prototypical instantiations of the SocL logical verification framework for the analysis of qualitative properties of service-oriented systems. They only differ w.r.t. the underlying computational models which are based on COWS specifications in the case of CMC, and on UML statecharts in the case of UMC.
  
  Both tools can be publicly accessed as web applications, downloaded as platform-specific native applications (for Linux, Mac, Windows) or as platform-independent Java packages, and their basic functionalities are available as plugins inside the SDE. Automated / interactive translation aids allow service designers to specify service-oriented applications as UML4SOA diagrams and analyze them by means of the CMC-UMC verification framework.
  

• ISTI, Università di Firenze
  
• Contact:
  

• BPEL Analysis and Back-Annotation - BPEL is the industrial de-facto standard used for modelling service orchestrations. We have developed an end-to-end method which facilitates the analysis of several liveness and safety properties of such an orchestration. Although several such methods exist, very little attention has been paid on the back-annotation of the results to the original process modelling language; our method helps both the intuitive definition of requirements and shows analysis results directly on the business process, allowing an interactive “simulation” of traces generated by model checking.
  
   
  BPEL analysis and back annotation process

• Budapest University of Technology and Economics
  
• Contact: