LTSA-WS: a tool for model-based verification of web service compositions and choreography. In this paper we describe a tool for a model-based approach to verifying compositions of web service implementations. The tool supports verification of properties created from design specifications and implementation models to confirm expected results from the viewpoints of both the designer and implementer. Scenarios are modeled in UML, in the form of Message Sequence Charts (MSCs), and then compiled into the Finite State Process (FSP) process algebra to concisely model the required behavior. BPEL4WS implementations are mechanically translated to FSP to allow an equivalence trace verification process to be performed. By providing early design verification and validation, the implementation, testing and deployment of web service compositions can be eased through the understanding of the behavior exhibited by the composition. The approach is implemented as a plug-in for the Eclipse development environment providing cooperating tools for specification, formal modeling, verification and validation of the composition process.

This software is also peer reviewed by journal TOMS.

References in zbMATH (referenced in 14 articles )

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

  1. Menghi, Claudio; Rizzi, Alessandro Maria; Bernasconi, Anna; Spoletini, Paola: TOrPEDO : witnessing model correctness with topological proofs (2021)
  2. Lanese, Ivan; Montesi, Fabrizio; Zavattaro, Gianluigi: The evolution of Jolie. From orchestrations to adaptable choreographies (2015)
  3. Dong, Jin Song; Liu, Yang; Sun, Jun; Zhang, Xian: Towards verification of computation orchestration (2014)
  4. Durán, Francisco; Ouederni, Meriem; Salaün, Gwen: A generic framework for (n)-protocol compatibility checking (2012)
  5. Bădică, Amelia; Bădică, Costin: FSP and FLTL framework for specification and verification of middle-agents (2011)
  6. Cubo, Javier; Canal, Carlos; Pimentel, Ernesto: Context-aware composition and adaptation based on model transformation (2011) ioport
  7. Lapadula, A.; Pugliese, R.; Tiezzi, F.: A WSDL-based type system for asynchronous WS-BPEL processes (2011)
  8. Martín, J. A.; Pimentel, E.: Contracts for security adaptation (2011)
  9. Mayer, Philip: MDD4SOA. Model-driven development for service-oriented architectures. (2010)
  10. Huai, Jinpeng; Deng, Ting; Li, Xianxian; Du, Zongxia; Guo, Huipeng: AutoSyn: A new approach to automated synthesis of composite web services with correctness guarantee (2009)
  11. Wu, Zhaohui; Deng, Shuiguang; Li, Ying; Wu, Jian: Computing compatibility in dynamic service composition (2009) ioport
  12. Di Nitto, Elisabetta; Ghezzi, Carlo; Metzger, Andreas; Papazoglou, Mike; Pohl, Klaus: A journey to highly dynamic, self-adaptive service-based applications (2008) ioport
  13. Haddad, Serge; Poizat, Pascal: Transactional reduction of component compositions (2007)
  14. Prasetya, I. S. W. B.; Vos, T. E. J.; Swierstra, S. D.: Web Cube (2006)