CMC-UMC

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

CMC-UMC: a framework for the verification of abstract service-oriented properties

Full text

Pdf (383 KB)

Source

Symposium on Applied Computing archive
Proceedings of the 2009 ACM symposium on Applied Computing table of contents

Honolulu, Hawaii

SESSION: Service oriented architectures and programming track table of contents

Pages 2111-2117

Year of Publication: 2009

ISBN:978-1-60558-166-8

Authors

Maurice H. ter Beek	ISTI--CNR, Pisa, Italy
Franco Mazzanti	ISTI--CNR, Pisa, Italy
Stefania Gnesi	ISTI--CNR, Pisa, Italy

Sponsor

SIGAPP: ACM Special Interest Group on Applied Computing

Publisher

ACM New York, NY, USA

Bibliometrics

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

Additional Information:

abstract references index terms collaborative colleagues

Tools and Actions:	Request Permissions 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/1529282.1529751 What is a DOI?

ABSTRACT

CMC and UMC are two prototypical instantiations of a common logical verification framework for the analysis of functional properties of service-oriented systems. The service-oriented SocL logic is used to describe the required system properties. Computational models of the system can be built either using the COWS specification language or designing the system as a collection of interacting UML state machines, and an on-the-fly model checker can be used to verify the satisfaction of the requirements and possibly to generate counterexamples or witnesses for them. An automotive case study is used to illustrate the overall framework.

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	G. Alonso, F. Casati, H. Kuno, and V. Machiraju. Web Services. Springer, 2004.
	2	L. F. Andrade et alii. AGILE: Software Architectures for Mobility In WADT'02, volume 2755 of LNCS, pages 1--33. Springer, 2003.
	3	M. H. ter Beek, A. Fantechi, S. Gnesi, and F. Mazzanti. An action/state-based model-checking approach for the analysis of communication protocols for Service-Oriented Applications. In FMICS'07, volume 4916 of LNCS, pages 133--148. Springer, 2008.
	4	Maurice H. ter Beek , Stefania Gnesi , Franco Mazzanti , Corrado Moiso, Formal Modelling and Verification of an Asynchronous Extension of SOAP, Proceedings of the European Conference on Web Services, p.287-296, December 04-06, 2006 [doi>10.1109/ECOWS.2006.22]
	5	Maurice H. ter Beek , Stefania Gnesi , Nora Koch , Franco Mazzanti, Formal verification of an automotive scenario in service-oriented computing, Proceedings of the 30th international conference on Software engineering, May 10-18, 2008, Leipzig, Germany [doi>10.1145/1368088.1368173]
	6	L. Bocchi, A. Fantechi, L. Gönczy, and N. Koch. Prototype language for service modelling: SOA ontology in structured natural language. SENSORIA deliverable D1.1a, 2006.
	7	Edmund M. Clarke, Jr. , Orna Grumberg , Doron A. Peled, Model checking, MIT Press, Cambridge, MA, 2000
	8	Rocco De Nicola , Frits Vaandrager, Three logics for branching bisimulation, Journal of the ACM (JACM), v.42 n.2, p.458-487, March 1995 [doi>10.1145/201019.201032]
	9	A. Fantechi, S. Gnesi, A. Lapadula, F. Mazzanti, R. Pugliese, and F. Tiezzi. A model checking approach for verifying COWS specifications. Tech. Report, Univ. of Florence, 2007. http://rap.dsi.unifi.it/cows.
	10	A. Fantechi, S. Gnesi, A. Lapadula, F. Mazzanti, R. Pugliese, and F. Tiezzi. A model checking approach for verifying COWS specifications. In FASE'08, volume 4961 of LNCS, pages 230--245. Springer, 2008.
	11	S. Gnesi and F. Mazzanti. On the Fly Verification of Networks of Automata. In PDPTA'99 (Special session on Current limits to automated verification for distributed systems). CSREA Press, 1999.
	12	S. Gnesi and F. Mazzanti. On the fly model checking of communicating UML State Machines In SERA'04, pages 331--338, 2004.
	13	N. Koch and D. Berndl. Requirements modelling and analysis of selected scenarios: Automotive case study. SENSORIA deliverable D8.2a, 2006.
	14	A. Lapadula, R. Pugliese, and F. Tiezzi. A Calculus for Orchestration of Web Services (full version). Tech. Report, Univ. of Florence, 2007. http://rap.dsi.unifi.it/cows.
	15	A. Lapadula, R. Pugliese, and F. Tiezzi. A Calculus for Orchestration of Web Services. In ESOP'07, volume 4421 of LNCS, pages 33--47. Springer, 2007.
	16	F. Mazzanti. UMC User Guide (Version 3.3). ISTI Tech. Report 2006-TR-33, 2006.
	17	CMC--UMC online. http://fmt.isti.cnr.it/cmc http://fmt.isti.cnr.it/umc
	18	Robert Meolic , Tatjana Kapus , Zmago Brezočnik, ACTLW - An action-based computation tree logic with unless operator, Information Sciences: an International Journal, v.178 n.6, p.1542-1557, March, 2008 [doi>10.1016/j.ins.2007.10.023]
	19	Object Management Group. UML 2.0 Superstructure Specification, ptc/03-08-02, OMG, 2003.
	20	EU project SENSORIA (IST-2005-016004). http://www.sensoria-ist.eu/.