InforLorV4, Main, Curation, bibRecord, 001734

A Bounded Model Checking Approach for the Verification of Web Services Composition

Identifieur interne : 001734 ( Main/Curation ); précédent : 001733; suivant : 001735

A Bounded Model Checking Approach for the Verification of Web Services Composition

Auteurs : Ehtesham Zahoor [Pakistan] ; Kashif Munir [Pakistan] ; Olivier Perrin [France] ; Claude Godart [France]

Source :

International journal of web services research [ 1545-7362 ] ; 2013.

RBID : Pascal:15-0039086

Descripteurs français

Pascal (Inist)
- Vérification modèle, Machine état fini, Service web, Orienté service, Coordination, Intergiciel publication souscription, Vérification programme, Composition, Processus service, Satisfiabilité, Spécification modèle, Exigence usager, Architecture basée modèle, Satisfaction contrainte, Modélisation, Analyse statique, ..

English descriptors

KwdEn :
- Composition, Constraint satisfaction, Coordination, Finite state machine, Model checking, Model driven architecture, Model specification, Modeling, Program verification, Publish subscribe middleware, Satisfiability, Service oriented, Service process, Static analysis, User requirement, Web service.

Abstract

In this paper, we propose a bounded model-checking based approach for the verification of declarative Web services composition processes using satisfiability solving (SAT). The need for the bounded model-checking approach stems from the nature of declarative processes as they are defined by only specifying the constraints that mark the boundary of the solution to the composition process. The proposed approach relies on using Event Calculus (EC) as the modeling formalism with a sound and complete EC to SAT encoding process. The use of EC as the modeling also formalism allows for a highly expressive approach for both the specification of composition model and for the specification of verification properties. Furthermore, as the conflict clauses returned by the SAT solver can be significantly large for complex processes and verification requirements, we propose afiltering criterion and defined patterns for identifying the clauses of interest for process verification.

Links toward previous steps (curation, corpus...)

to stream PascalFrancis, to step Corpus: Pour aller vers cette notice dans l'étape Curation :000001
to stream PascalFrancis, to step Curation: Pour aller vers cette notice dans l'étape Curation :000A02
to stream PascalFrancis, to step Checkpoint: Pour aller vers cette notice dans l'étape Curation :000082
to stream Main, to step Merge: Pour aller vers cette notice dans l'étape Curation :001753

Links to Exploration step

Pascal:15-0039086

Le document en format XML

<record><TEI><teiHeader><fileDesc><titleStmt><title xml:lang="en" level="a">A Bounded Model Checking Approach for the Verification of Web Services Composition</title>
<author><name sortKey="Zahoor, Ehtesham" sort="Zahoor, Ehtesham" uniqKey="Zahoor E" first="Ehtesham" last="Zahoor">Ehtesham Zahoor</name>
<affiliation wicri:level="1"><inist:fA14 i1="01"><s1>National University of Computer and Emerging Sciences</s1>
<s2>Islamabad</s2>
<s3>PAK</s3>
<sZ>1 aut.</sZ>
<sZ>2 aut.</sZ>
</inist:fA14>
<country>Pakistan</country>
<wicri:noRegion>National University of Computer and Emerging Sciences</wicri:noRegion>
</affiliation>
</author>
<author><name sortKey="Munir, Kashif" sort="Munir, Kashif" uniqKey="Munir K" first="Kashif" last="Munir">Kashif Munir</name>
<affiliation wicri:level="1"><inist:fA14 i1="01"><s1>National University of Computer and Emerging Sciences</s1>
<s2>Islamabad</s2>
<s3>PAK</s3>
<sZ>1 aut.</sZ>
<sZ>2 aut.</sZ>
</inist:fA14>
<country>Pakistan</country>
<wicri:noRegion>National University of Computer and Emerging Sciences</wicri:noRegion>
</affiliation>
</author>
<author><name sortKey="Perrin, Olivier" sort="Perrin, Olivier" uniqKey="Perrin O" first="Olivier" last="Perrin">Olivier Perrin</name>
<affiliation wicri:level="1"><inist:fA14 i1="02"><s1>Laboratoire Lorrain de Recherche en Informatique et Ses Applications (LORIA), Universiteé de Lorraine</s1>
<s2>Lorraine</s2>
<s3>FRA</s3>
<sZ>3 aut.</sZ>
<sZ>4 aut.</sZ>
</inist:fA14>
<country>France</country>
<wicri:noRegion>Lorraine</wicri:noRegion>
<wicri:noRegion>Universiteé de Lorraine</wicri:noRegion>
<wicri:noRegion>Lorraine</wicri:noRegion>
</affiliation>
</author>
<author><name sortKey="Godart, Claude" sort="Godart, Claude" uniqKey="Godart C" first="Claude" last="Godart">Claude Godart</name>
<affiliation wicri:level="1"><inist:fA14 i1="02"><s1>Laboratoire Lorrain de Recherche en Informatique et Ses Applications (LORIA), Universiteé de Lorraine</s1>
<s2>Lorraine</s2>
<s3>FRA</s3>
<sZ>3 aut.</sZ>
<sZ>4 aut.</sZ>
</inist:fA14>
<country>France</country>
<wicri:noRegion>Lorraine</wicri:noRegion>
<wicri:noRegion>Universiteé de Lorraine</wicri:noRegion>
<wicri:noRegion>Lorraine</wicri:noRegion>
</affiliation>
</author>
</titleStmt>
<publicationStmt><idno type="wicri:source">INIST</idno>
<idno type="inist">15-0039086</idno>
<date when="2013">2013</date>
<idno type="stanalyst">PASCAL 15-0039086 INIST</idno>
<idno type="RBID">Pascal:15-0039086</idno>
<idno type="wicri:Area/PascalFrancis/Corpus">000001</idno>
<idno type="wicri:Area/PascalFrancis/Curation">000A02</idno>
<idno type="wicri:Area/PascalFrancis/Checkpoint">000082</idno>
<idno type="wicri:explorRef" wicri:stream="PascalFrancis" wicri:step="Checkpoint">000082</idno>
<idno type="wicri:doubleKey">1545-7362:2013:Zahoor E:a:bounded:model</idno>
<idno type="wicri:Area/Main/Merge">001753</idno>
<idno type="wicri:Area/Main/Curation">001734</idno>
</publicationStmt>
<sourceDesc><biblStruct><analytic><title xml:lang="en" level="a">A Bounded Model Checking Approach for the Verification of Web Services Composition</title>
<author><name sortKey="Zahoor, Ehtesham" sort="Zahoor, Ehtesham" uniqKey="Zahoor E" first="Ehtesham" last="Zahoor">Ehtesham Zahoor</name>
<affiliation wicri:level="1"><inist:fA14 i1="01"><s1>National University of Computer and Emerging Sciences</s1>
<s2>Islamabad</s2>
<s3>PAK</s3>
<sZ>1 aut.</sZ>
<sZ>2 aut.</sZ>
</inist:fA14>
<country>Pakistan</country>
<wicri:noRegion>National University of Computer and Emerging Sciences</wicri:noRegion>
</affiliation>
</author>
<author><name sortKey="Munir, Kashif" sort="Munir, Kashif" uniqKey="Munir K" first="Kashif" last="Munir">Kashif Munir</name>
<affiliation wicri:level="1"><inist:fA14 i1="01"><s1>National University of Computer and Emerging Sciences</s1>
<s2>Islamabad</s2>
<s3>PAK</s3>
<sZ>1 aut.</sZ>
<sZ>2 aut.</sZ>
</inist:fA14>
<country>Pakistan</country>
<wicri:noRegion>National University of Computer and Emerging Sciences</wicri:noRegion>
</affiliation>
</author>
<author><name sortKey="Perrin, Olivier" sort="Perrin, Olivier" uniqKey="Perrin O" first="Olivier" last="Perrin">Olivier Perrin</name>
<affiliation wicri:level="1"><inist:fA14 i1="02"><s1>Laboratoire Lorrain de Recherche en Informatique et Ses Applications (LORIA), Universiteé de Lorraine</s1>
<s2>Lorraine</s2>
<s3>FRA</s3>
<sZ>3 aut.</sZ>
<sZ>4 aut.</sZ>
</inist:fA14>
<country>France</country>
<wicri:noRegion>Lorraine</wicri:noRegion>
<wicri:noRegion>Universiteé de Lorraine</wicri:noRegion>
<wicri:noRegion>Lorraine</wicri:noRegion>
</affiliation>
</author>
<author><name sortKey="Godart, Claude" sort="Godart, Claude" uniqKey="Godart C" first="Claude" last="Godart">Claude Godart</name>
<affiliation wicri:level="1"><inist:fA14 i1="02"><s1>Laboratoire Lorrain de Recherche en Informatique et Ses Applications (LORIA), Universiteé de Lorraine</s1>
<s2>Lorraine</s2>
<s3>FRA</s3>
<sZ>3 aut.</sZ>
<sZ>4 aut.</sZ>
</inist:fA14>
<country>France</country>
<wicri:noRegion>Lorraine</wicri:noRegion>
<wicri:noRegion>Universiteé de Lorraine</wicri:noRegion>
<wicri:noRegion>Lorraine</wicri:noRegion>
</affiliation>
</author>
</analytic>
<series><title level="j" type="main">International journal of web services research</title>
<idno type="ISSN">1545-7362</idno>
<imprint><date when="2013">2013</date>
</imprint>
</series>
</biblStruct>
</sourceDesc>
<seriesStmt><title level="j" type="main">International journal of web services research</title>
<idno type="ISSN">1545-7362</idno>
</seriesStmt>
</fileDesc>
<profileDesc><textClass><keywords scheme="KwdEn" xml:lang="en"><term>Composition</term>
<term>Constraint satisfaction</term>
<term>Coordination</term>
<term>Finite state machine</term>
<term>Model checking</term>
<term>Model driven architecture</term>
<term>Model specification</term>
<term>Modeling</term>
<term>Program verification</term>
<term>Publish subscribe middleware</term>
<term>Satisfiability</term>
<term>Service oriented</term>
<term>Service process</term>
<term>Static analysis</term>
<term>User requirement</term>
<term>Web service</term>
</keywords>
<keywords scheme="Pascal" xml:lang="fr"><term>Vérification modèle</term>
<term>Machine état fini</term>
<term>Service web</term>
<term>Orienté service</term>
<term>Coordination</term>
<term>Intergiciel publication souscription</term>
<term>Vérification programme</term>
<term>Composition</term>
<term>Processus service</term>
<term>Satisfiabilité</term>
<term>Spécification modèle</term>
<term>Exigence usager</term>
<term>Architecture basée modèle</term>
<term>Satisfaction contrainte</term>
<term>Modélisation</term>
<term>Analyse statique</term>
<term>.</term>
</keywords>
</textClass>
</profileDesc>
</teiHeader>
<front><div type="abstract" xml:lang="en">In this paper, we propose a bounded model-checking based approach for the verification of declarative Web services composition processes using satisfiability solving (SAT). The need for the bounded model-checking approach stems from the nature of declarative processes as they are defined by only specifying the constraints that mark the boundary of the solution to the composition process. The proposed approach relies on using Event Calculus (EC) as the modeling formalism with a sound and complete EC to SAT encoding process. The use of EC as the modeling also formalism allows for a highly expressive approach for both the specification of composition model and for the specification of verification properties. Furthermore, as the conflict clauses returned by the SAT solver can be significantly large for complex processes and verification requirements, we propose afiltering criterion and defined patterns for identifying the clauses of interest for process verification.</div>
</front>
</TEI>
</record>

Pour manipuler ce document sous Unix (Dilib)

EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Main/Curation

HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 001734 | SxmlIndent | more

HfdSelect -h $EXPLOR_AREA/Data/Main/Curation/biblio.hfd -nk 001734 | SxmlIndent | more

Pour mettre un lien sur cette page dans le réseau Wicri

{{Explor lien
   |wiki=    Wicri/Lorraine
   |area=    InforLorV4
   |flux=    Main
   |étape=   Curation
   |type=    RBID
   |clé=     Pascal:15-0039086
   |texte=   A Bounded Model Checking Approach for the Verification of Web Services Composition
}}

This area was generated with Dilib version V0.6.33.
Data generation: Mon Jun 10 21:56:28 2019. Site generation: Fri Feb 25 15:29:27 2022

	Serveur d'exploration sur la recherche en informatique en Lorraine
	Attention, ce site est en cours de développement ! Attention, site généré par des moyens informatiques à partir de corpus bruts. Les informations ne sont donc pas validées.

Serveur d'exploration sur la recherche en informatique en Lorraine

A Bounded Model Checking Approach for the Verification of Web Services Composition

A Bounded Model Checking Approach for the Verification of Web Services Composition

Source :

Descripteurs français

English descriptors

Abstract

Links toward previous steps (curation, corpus...)

Links to Exploration step

Le document en format XML

Pour manipuler ce document sous Unix (Dilib)

Pour mettre un lien sur cette page dans le réseau Wicri