A model-prover for constrained dynamic conversations

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

A model-prover for constrained dynamic conversations

Full text

Pdf (200 KB)

Source

International Conference on Information Integration and web-based Applications and Services archive
Proceedings of the 10th International Conference on Information Integration and Web-based Applications & Services table of contents

Linz, Austria

WORKSHOP SESSION: iiWAS 2008 workshops: ERPAS 2008: Business and service model table of contents

Pages 630-633

Year of Publication: 2008

ISBN:978-1-60558-349-5

Authors

Diletta Cacciagrano	University of Camerino, Camerino, Italy
Flavio Corradini	University of Camerino, Camerino, Italy
Rosario Culmone	University of Camerino, Camerino, Italy
Luca Tesei	University of Camerino, Camerino, Italy
Leonardo Vito	University of Camerino, Camerino, Italy

Sponsor

SIGWEB: ACM Special Interest Group on Hypertext, Hypermedia, and Web

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 0, Downloads (12 Months): 20, Citation Count: 0

Additional Information:

abstract references index terms collaborative colleagues

Tools and Actions:	Review this Article Save this Article to a Binder Display Formats: BibTeX EndNote ACM Ref

DOI Bookmark:	Use this link to bookmark this Article: http://doi.acm.org/10.1145/1497308.1497428 What is a DOI?

ABSTRACT

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.

REFERENCES

Note: OCR errors may be found in this Reference List extracted from the full text article. ACM has opted to expose the complete List rather than only correct and linked references.

	1	The Alloy analyzer, http://alloy.mit.edu/.
	2	BPML: Business Process Modeling Language, http://www.bpmi.org/.
	3	Object Constraint Language Specification V. 2.0, http://www.klasse.nl/ocl/ocl-subm.html/.
	4	OCL 1.4 syntax checker, http://www.klasse.nl/ocl/.
	5	OCLE 1.0, http://lci.cs.ubbcluj.ro/ocle/.
	6	W3C XML Schema, http://www.w3.org/xml/schema/.
	7	WS-CDL: Web Service Choreography Description Language, http://www.w3.org/tr/ws-cdl-10/.
	8	WSCI: Web Service Choreography Interface, http://www.w3.org/tr/wsci/.
	9	WSCL: Web Service Conversation Language, http://www.w3.org/tr/wscl10/.
	10	WSDL: Web Service Definition Language, http://www.w3.org/tr/wsdl/.
	11	XML Path Language (XPath) V. 2.0, http://www.w3.org/tr/xpath20/.
	12	K. Anastasakis, B. Bordbar, G. Georg, and I. Ray. UML2Alloy: A challenging model transformation. pages 436--450. 2007.
	13	D. B. Aredo. A framework for semantics of UML Sequence Diagrams in PVS. Journal of Universal Computer Science, 8(7):674--697, 2002.
	14	Achim D. Brucker , Burkhart Wolff, A Proposal for a Formal OCL Semantics in Isabelle/HOL, Proceedings of the 15th International Conference on Theorem Proving in Higher Order Logics, p.99-114, August 20-23, 2002
	15	Tevfik Bultan , Xiang Fu , Richard Hull , Jianwen Su, Conversation specification: a new approach to design and analysis of e-service composition, Proceedings of the 12th international conference on World Wide Web, May 20-24, 2003, Budapest, Hungary [doi>10.1145/775152.775210]
	16	D. Cacciagrano, F. Corradini, R. Culmone, and L. Vito. Dynamic constraint-based invocation of Web Services. In M. Bravetti, M. Nez, and G. Zavattaro, editors, WS-FM, volume 4184 of Lecture Notes in Computer Science, pages 138--147. Springer, 2006.
	17	H. Foster, S. Uchitel, J. Magee, and J. Kramer. Model-based verification of Web Service compositions. pages 152--163. IEEE Computer Society, 2003.
	18	Xiang Fu , Tevfik Bultan , Jianwen Su, Analysis of interacting BPEL web services, Proceedings of the 13th international conference on World Wide Web, May 17-20, 2004, New York, NY, USA [doi>10.1145/988672.988756]
	19	M. D. M. Gallardo, P. Merino, and E. Pimentel. Debugging UML designs with model checking. Journal of Object Technology, 1:101--117, 2002.
	20	Geri Georg , Jores Bieman , Robert B. France, Using Alloy and UML/OCL to Specify Run-Time Configuration Management: A Case Study, Workshop of the pUML-Group held together with the «UML»2001 on Practical UML-Based Rigorous Development Methods - Countering or Integrating the eXtremists, p.128-141, October 01, 2001
	21	Gerard J. Holzmann, The Model Checker SPIN, IEEE Transactions on Software Engineering, v.23 n.5, p.279-295, May 1997 [doi>10.1109/32.588521]
	22	H. Hussmann, B. Demuth, and F. Finger. Modular architecture for a toolset supporting OCL. In A. Evans, S. Kent, and B. Selic, editors, UML 2000 - The Unified Modeling Language. Advancing the Standard. Third International Conference, York, UK, October 2000, Proceedings, volume 1939 of LNCS, pages 278--293. Springer, 2000.
	23	R. Marcano and N. Levy. Transformation rules of OCL constraints into B formal expressions. In J. Jürjens, M. V. Cengarle, E. B. Fernandez, B. Rumpe, and R. Sandner, editors, Critical Systems Development with UML -- Proceedings of the UML '02 workshop, pages 155--162. Technische Universität München, Institut für Informatik, 2002.
	24	M. Richters and M. Gogolla. Validating UML models and OCL constraints. pages 265--277. Springer, 2000.