This paper presents Web Service Analysis Tool (WSAT), a tool for analyzing and verifying composite web service designs, with the state of the art model checking techniques. Web services are loosely coupled distributed systems communicating via XML messages. Communication among web services is asynchronous, and it is supported by messaging platforms such as JMS which provide FIFO queues to store incoming messages. Data transmission among web services is standardized via XML, and the specification of web service itself (invocation interface and behavior signature) relies on a stack of XML based standards (e.g. WSDL, BPEL4WS, WSCI and etc.). The characteristics of web services, however, raise several challenges in the application of model checking: (1) Numerous competing web service standards, most of which lack formal semantics, complicate the formal specification of web service composition. (2) Asynchronous messaging makes most interesting verification problems undecidable, even when XML message contents are abstracted away. (3) XML data and expressive XPath based manipulation are not supported by current model checkers.

References in zbMATH (referenced in 31 articles , 1 standard article )

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

1 2 next

  1. Basu, Samik; Bultan, Tevfik: On deciding synchronizability for asynchronously communicating systems (2016)
  2. Sheng, Quan Z.; Maamar, Zakaria; Yao, Lina; Szabo, Claudia; Bourne, Scott: Behavior modeling and automated verification of web services (2014)
  3. Deng, Ting; Fan, Wenfei; Libkin, Leonid; Wu, Yinghui: On the aggregation problem for synthesized web services (2013)
  4. Fiadeiro, José Luiz; Lopes, Antónia: An interface theory for service-oriented design (2013)
  5. Gao, Yang; Xu, Ming; Zhan, Naijun; Zhang, Lijun: Model checking conditional CSL for continuous-time Markov chains (2013)
  6. Simmonds, Jocelyn; Ben-David, Shoham; Chechik, Marsha: Monitoring and recovery for web service applications (2013)
  7. Basu, Samik; Bultan, Tevfik; Ouederni, Meriem: Deciding choreography realizability (2012)
  8. Basu, Samik; Bultan, Tevfik; Ouederni, Meriem: Synchronizability for verification of asynchronously communicating systems (2012)
  9. Deng, Ting; Huai, Jinpeng; Wo, Tianyu: Complexity of synthesis of composite service with correctness guarantee (2012)
  10. Durán, Francisco; Ouederni, Meriem; Salaün, Gwen: A generic framework for $n$-protocol compatibility checking (2012)
  11. Fiadeiro, José; Lopes, Antónia; Abreu, João: A formal model for service-oriented interactions (2012)
  12. Li, Mu; Li, Bo; Huai, Jinpeng: Reliability-aware automatic composition approach for web services (2012)
  13. Polini, Andrea; Polzonetti, Andrea; Re, Barbara: Formal methods to improve public administration business processes (2012)
  14. Cubo, Javier; Canal, Carlos; Pimentel, Ernesto: Model-based dependable composition of self-adaptive systems (2011)
  15. Martín, J.A.; Pimentel, E.: Contracts for security adaptation (2011)
  16. Nam, Wonhong; Kil, Hyunyoung; Lee, Dongwon: On the computational complexity of behavioral description-based web service composition (2011)
  17. Roohi, Nima; Salaün, Gwen: Realizability and dynamic reconfiguration of chor specifications (2011)
  18. van der Aalst, W.M.P.; van Hee, K.M.; ter Hofstede, A.H.M.; Sidorova, N.; Verbeek, H.M.W.; Voorhoeve, M.; Wynn, M.T.: Soundness of workflow nets: classification, decidability, and analysis (2011)
  19. Ramos, Rodrigo; Sampaio, Augusto; Mota, Alexandre: Conformance notions for the coordination of interaction components (2010)
  20. Huang, Tao; Wu, Guo-Quan; Wei, Jun: Runtime monitoring compositeWeb services through stateful aspect extension (2009)

1 2 next

Further publications can be found at: