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

• Type: Conference
• Year: 2008
• Where: IIWAS
• Authors: Diletta Cacciagrano, Flavio Corradini, Rosario Culmone, Luca Tesei, Leonardo Vito
• Keywords: First-order Constrained Client-server, IIWAS 2008, Internet Technology, Software Engineering, UML Class Diagrams