A Bounded Model Checking Approach for the Verification of Web Services Composition
Identifieur interne : 001734 ( Main/Curation ); précédent : 001733; suivant : 001735A 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.
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 :
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-0039086Le 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
Ou
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. | ![]() |