An action/state-based model-checking approach for the analysis of an asynchronous protocol for Service-Oriented Applications (Contributo in atti di convegno)

Type

• Prodotto della ricerca (Classe)
• Contributo in atti di convegno (Classe)

Label

• An action/state-based model-checking approach for the analysis of an asynchronous protocol for Service-Oriented Applications (Contributo in atti di convegno) (literal)

Anno

• 2007-01-01T00:00:00+01:00 (literal)

Alternative label

• Ter Beek M. H.; Fantechi A.; Gnesi S.; Mazzanti F. (2007)
  An action/state-based model-checking approach for the analysis of an asynchronous protocol for Service-Oriented Applications
  in 12th International Workshop on Formal Methods for Industrial Critical Systems (FMICS 2007), Berlino, Germania
  (literal)

Http://www.cnr.it/ontology/cnr/pubblicazioni.owl#autori

• Ter Beek M. H.; Fantechi A.; Gnesi S.; Mazzanti F. (literal)

Http://www.cnr.it/ontology/cnr/pubblicazioni.owl#note

• In: 12th International Workshop on Formal Methods for Industrial Critical Systems (FMICS 2007) (Berlino, Germania, 1-2 Luglio 2007). Proceedings, pp. 135 - 147. Stefan Leue and Pedro Merino (ed.). Universität Konstanz / Universidad de Málaga, Germany / Spain, 2007. (literal)

Http://www.cnr.it/ontology/cnr/pubblicazioni.owl#descrizioneSinteticaDelProdotto

• 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 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)

Titolo

• An action/state-based model-checking approach for the analysis of an asynchronous protocol for Service-Oriented Applications (literal)

Prodotto di

• Istituto di scienza e tecnologie dell'informazione \"Alessandro Faedo\" (ISTI) (Istituto)
• Metodi e Strumenti per la Progettazione di Sistemi Software-Intensive ad Elevata Complessità (ICT.P09.008.002) (Modulo)

Autore CNR

• MAURICE HENRI TER BEEK (Persona)
• ALESSANDRO FANTECHI (Unità di personale esterno)

Insieme di parole chiave

• Parole chiave di "An action/state-based model-checking approach for the analysis of an asynchronous protocol for Service-Oriented Applications" (Insieme di parole chiave)

Incoming links:

Prodotto

• Istituto di scienza e tecnologie dell'informazione \"Alessandro Faedo\" (ISTI) (Istituto)
• Metodi e Strumenti per la Progettazione di Sistemi Software-Intensive ad Elevata Complessità (ICT.P09.008.002) (Modulo)

Autore CNR di

• MAURICE HENRI TER BEEK (Persona)
• ALESSANDRO FANTECHI (Unità di personale esterno)

Insieme di parole chiave di

• Parole chiave di "An action/state-based model-checking approach for the analysis of an asynchronous protocol for Service-Oriented Applications" (Insieme di parole chiave)