Istituto di Scienza e Tecnologie dell'Informazione     
Abreu J., Mazzanti F., Fiadeiro L. J., Gnesi S. A model-checking approach for service component architectures. In: FMOODS/FORTE 2009 - 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, 9-12 June 2009). Proceedings, pp. 219 - 224. David Lee, Antonia Lopes, Arnd Poetzsch-Heffter (eds.). (Lecture Notes in Computer Science, vol. 5522). Springer, 2009.
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.
URL: http://www.springerlink.com/content/p680x3783552/?p=124cd3168ef147cea370807b7d6a6a7a&pi=0
DOI: 10.1007/978-3-642-02138-1_15
Subject Formal modelling framework for service-oriented computing - SRML
Branching time temporal logic UCTL
model-checker UMC
D.2.2 Design Tools and Techniques
D.2.4 Software/Program Verification

Icona documento 1) Download Document PDF

Icona documento Open access Icona documento Restricted Icona documento Private


Per ulteriori informazioni, contattare: Librarian http://puma.isti.cnr.it

Valid HTML 4.0 Transitional