http://www.cnr.it/ontology/cnr/individuo/prodotto/ID44144
An action/state-based model-checking approach for the analysis of communication protocols for service-oriented applications (Articolo in rivista)
- Type
- Label
- An action/state-based model-checking approach for the analysis of communication protocols for service-oriented applications (Articolo in rivista) (literal)
- Anno
- 2008-01-01T00:00:00+01:00 (literal)
- Alternative label
- Http://www.cnr.it/ontology/cnr/pubblicazioni.owl#autori
- Ter Beek M. H.; Fantechi A.; Gnesi S.; Mazzanti F. (literal)
- Pagina inizio
- Pagina fine
- Http://www.cnr.it/ontology/cnr/pubblicazioni.owl#numeroVolume
- Rivista
- Http://www.cnr.it/ontology/cnr/pubblicazioni.owl#note
- In: 12th International Workshop on Formal Methods for Industrial Critical Systems. FMICS'07 (Berlin, Germany, 1-2 July 2007). Proceedings, pp. 133 - 148. S. Leue and P. Merino (eds.). (Lecture Notes in Computer Science, vol. 4916). Springer-Verlag, Berlin, 2008. (literal)
- Note
- ISI Web of Science (WOS) (literal)
- Http://www.cnr.it/ontology/cnr/pubblicazioni.owl#affiliazioni
- CNR-ISTI, Pisa, CNR-ISTI, Pisa & Universita' di Firenze (literal)
- Titolo
- An action/state-based model-checking approach for the analysis of communication protocols for service-oriented applications (literal)
- Abstract
- In this paper we present an action/state-based logical framework for the analysis and verification of complex systems, which relies on the definition of doubly labelled transition systems. The defined temporal logic, called UCTL, combines the action paradigm - classically used to describe systems using labelled transition systems - with predicates that are true over states - as captured when using Kripke structures as semantic model. An efficient model checker for UCTL has been realized, exploiting an on-the-fly algorithm. We then show how to use UCTL, and its model checker, in the design phase of an asynchronous extension of the communication protocol SOAP, called aSOAP. For this purpose, we describe aSOAP as a set of communicating UML state machines, for which a semantics over doubly labelled transition systems has been provided. (literal)
- Prodotto di
- Autore CNR
- Insieme di parole chiave
Incoming links:
- Autore CNR di
- Prodotto
- Http://www.cnr.it/ontology/cnr/pubblicazioni.owl#rivistaDi
- Insieme di parole chiave di