Sciweavers

Share
IIWAS
2008

A model-prover for constrained dynamic conversations

9 years 8 months ago
A model-prover for constrained dynamic conversations
In a service-oriented architecture, systems communicate by exchanging messages. In this work, we propose a formal model based on OCL-constrained UML Class diagrams and a methodology based on Alloy Analyzer respectively for describing and verifying any first-order constrained client-server conversations. This framework allows us to verify conversation protocol designs at a fairly detailed level and to check first-order logic constraints on both message flows and message contents. Categories and Subject Descriptors C.2.4 [Computer-Communication Networks]: Client/server; D.2.1 [Software Engineering]: Methodologies; D.2.2 [Software Engineering]: Design tools and techniques; D.2.4 [Software Engineering]: Software/Program verification, Formal methods, Model checking, Validation Keywords Web Service, Conversations, WSDL, UML, OCL, Alloy
Diletta Cacciagrano, Flavio Corradini, Rosario Cul
Added 29 Oct 2010
Updated 29 Oct 2010
Type Conference
Year 2008
Where IIWAS
Authors Diletta Cacciagrano, Flavio Corradini, Rosario Culmone, Luca Tesei, Leonardo Vito
Comments (0)
books