A model-checking approach for service component architectures
Abreu J., Mazzanti F., Fiadeiro L. J., Gnesi S.
D.2.2 Design Tools and Techniques D.2.4 Software/Program Verification Formal modelling framework for service-oriented computing - SRML Branching time temporal logic UCTL model-checker UMC
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.
Source: Lecture notes in computer science 5522 (2009): 219–224.
Publisher: Springer, Berlin , Germania
Back to previous page
@article{oai:it.cnr:prodotti:44246,
title = {A model-checking approach for service component architectures},
author = {Abreu J. and Mazzanti F. and Fiadeiro L. J. and Gnesi S.},
publisher = {Springer, Berlin , Germania},
journal = {Lecture notes in computer science},
volume = {5522},
pages = {219–224},
year = {2009}
}
0000-0002-0139-0421