A model-checking approach for service component architectures

João Abreu, Franco Mazzanti, José Luiz Fiadeiro, Stefania Gnesi

Research output: Chapter in Book/Report/Conference proceedingConference contribution

15 Citations (Scopus)

Abstract

We present a strategy for model-checking the correctness of service composition. We do so in the context of SRML, a formal modelling framework for service-oriented computing being defined within the SENSORIA project. We introduce a methodology for encoding patterns of typical service interaction with UML state machines and present a strategy for checking SRML specifications of service composition based on such patterns. For that purpose, we use the action-state branching time temporal logic UCTL and the model-checker UMC.

Original languageEnglish
Title of host publicationFormal Techniques for Distributed Systems
Subtitle of host publicationJoint 11th IFIP WG 6.1 International Conference FMOODS 2009 and 29th IFIP WG 6.1 International Conference FORTE 2009, Lisboa, Portugal, June 9-12, 2009. Proceedings
EditorsDavid Lee, Antonia Lopes, Arnd Poetzsch-Heffter
Place of PublicationBerlin, Heidelberg
PublisherSpringer
Pages219-224
Number of pages6
ISBN (Electronic)978-3-642-02138-1
ISBN (Print)3642021379, 9783642021374
DOIs
Publication statusPublished - 28 Sep 2009
Event11th International Conference on Formal Methods for Open Object-Based Distributed Systems, FMOODS 2009 and 29th International Conference on Formal Techniques for Networked and Distributed Systems, FORTE 2009 - Lisboa, Portugal
Duration: 9 Jun 200912 Jun 2009

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume5522 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference11th International Conference on Formal Methods for Open Object-Based Distributed Systems, FMOODS 2009 and 29th International Conference on Formal Techniques for Networked and Distributed Systems, FORTE 2009
CountryPortugal
CityLisboa
Period9/06/0912/06/09

Fingerprint Dive into the research topics of 'A model-checking approach for service component architectures'. Together they form a unique fingerprint.

Cite this