A model-checking approach for service component architectures

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

doi:10.1007/978-3-642-02138-1_15

A model-checking approach for service component architectures

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

Science and Engineering Office

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

16 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 language	English
Title of host publication	Formal Techniques for Distributed Systems
Subtitle of host publication	Joint 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
Editors	David Lee, Antonia Lopes, Arnd Poetzsch-Heffter
Place of Publication	Berlin, Heidelberg
Publisher	Springer
Pages	219-224
Number of pages	6
ISBN (Electronic)	978-3-642-02138-1
ISBN (Print)	3642021379, 9783642021374
DOIs	https://doi.org/10.1007/978-3-642-02138-1_15
Publication status	Published - 28 Sept 2009
Event	11th 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 2009 → 12 Jun 2009

Publication series

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

Conference

Conference	11th 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
Country/Territory	Portugal
City	Lisboa
Period	9/06/09 → 12/06/09

ASJC Scopus subject areas

Theoretical Computer Science
General Computer Science

Access to Document

10.1007/978-3-642-02138-1_15

Cite this

Abreu, J., Mazzanti, F., Fiadeiro, J. L., & Gnesi, S. (2009). A model-checking approach for service component architectures. In D. Lee, A. Lopes, & A. Poetzsch-Heffter (Eds.), Formal Techniques for Distributed Systems: Joint 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 (pp. 219-224). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 5522 LNCS). Springer . https://doi.org/10.1007/978-3-642-02138-1_15

Abreu, João ; Mazzanti, Franco ; Fiadeiro, José Luiz et al. / A model-checking approach for service component architectures. Formal Techniques for Distributed Systems: Joint 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. editor / David Lee ; Antonia Lopes ; Arnd Poetzsch-Heffter. Berlin, Heidelberg : Springer , 2009. pp. 219-224 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{2fd6e235770848ee904a6fa29223a588,

title = "A model-checking approach for service component architectures",

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.",

author = "Jo{\~a}o Abreu and Franco Mazzanti and Fiadeiro, {Jos{\'e} Luiz} and Stefania Gnesi",

year = "2009",

month = sep,

day = "28",

doi = "10.1007/978-3-642-02138-1_15",

language = "English",

isbn = "3642021379",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer ",

pages = "219--224",

editor = "David Lee and Antonia Lopes and Arnd Poetzsch-Heffter",

booktitle = "Formal Techniques for Distributed Systems",

note = "11th 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 ; Conference date: 09-06-2009 Through 12-06-2009",

}

Abreu, J, Mazzanti, F, Fiadeiro, JL & Gnesi, S 2009, A model-checking approach for service component architectures. in D Lee, A Lopes & A Poetzsch-Heffter (eds), Formal Techniques for Distributed Systems: Joint 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. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 5522 LNCS, Springer , Berlin, Heidelberg, pp. 219-224, 11th 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, 9/06/09. https://doi.org/10.1007/978-3-642-02138-1_15

A model-checking approach for service component architectures. / Abreu, João; Mazzanti, Franco; Fiadeiro, José Luiz et al.
Formal Techniques for Distributed Systems: Joint 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. ed. / David Lee; Antonia Lopes; Arnd Poetzsch-Heffter. Berlin, Heidelberg: Springer , 2009. p. 219-224 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 5522 LNCS).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

TY - GEN

T1 - A model-checking approach for service component architectures

AU - Abreu, João

AU - Mazzanti, Franco

AU - Fiadeiro, José Luiz

AU - Gnesi, Stefania

PY - 2009/9/28

Y1 - 2009/9/28

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=70349309667&partnerID=8YFLogxK

U2 - 10.1007/978-3-642-02138-1_15

DO - 10.1007/978-3-642-02138-1_15

M3 - Conference contribution

AN - SCOPUS:70349309667

SN - 3642021379

SN - 9783642021374

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 219

EP - 224

BT - Formal Techniques for Distributed Systems

A2 - Lee, David

A2 - Lopes, Antonia

A2 - Poetzsch-Heffter, Arnd

PB - Springer

CY - Berlin, Heidelberg

T2 - 11th 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

Y2 - 9 June 2009 through 12 June 2009

ER -

Abreu J, Mazzanti F, Fiadeiro JL, Gnesi S. A model-checking approach for service component architectures. In Lee D, Lopes A, Poetzsch-Heffter A, editors, Formal Techniques for Distributed Systems: Joint 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. Berlin, Heidelberg: Springer . 2009. p. 219-224. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-642-02138-1_15

A model-checking approach for service component architectures

Abstract

Publication series

Conference

ASJC Scopus subject areas

Access to Document

Other files and links

Fingerprint

Cite this