InforLorV4, PascalFrancis, Corpus, bibRecord, 000001

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

Identifieur interne : 000001 ( PascalFrancis/Corpus ); précédent : 000000; suivant : 000002

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

Auteurs : Ehtesham Zahoor ; Kashif Munir ; Olivier Perrin ; Claude Godart

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.

Notice en format standard (ISO 2709)

Pour connaître la documentation sur le format Inist Standard.

A01	`01`	`1`		`@0 1545-7362`
A05				`@2 10`
A06				`@2 4`
A08	`01`	`1`	`ENG`	`@1 A Bounded Model Checking Approach for the Verification of Web Services Composition`
A09	`01`	`1`	`ENG`	`@1 Services Discovery and Verification`
A11	`01`	`1`		`@1 ZAHOOR (Ehtesham)`
A11	`02`	`1`		`@1 MUNIR (Kashif)`
A11	`03`	`1`		`@1 PERRIN (Olivier)`
A11	`04`	`1`		`@1 GODART (Claude)`
A12	`01`	`1`		`@1 LUO (Min) @9 ed.`
A14	`01`			`@1 National University of Computer and Emerging Sciences @2 Islamabad @3 PAK @Z 1 aut. @Z 2 aut.`
A14	`02`			`@1 Laboratoire Lorrain de Recherche en Informatique et Ses Applications (LORIA), Universiteé de Lorraine @2 Lorraine @3 FRA @Z 3 aut. @Z 4 aut.`
A15	`01`			`@1 Shannon Lab @2 Huawei, Shenzhen @3 CHN @Z 1 aut.`
A20				`@1 62-81`
A21				`@1 2013`
A23	`01`			`@0 ENG`
A43	`01`			`@1 INIST @2 28349 @5 354000501855950030`
A44				`@0 0000 @1 © 2015 INIST-CNRS. All rights reserved.`
A45				`@0 1 p.1/4`
A47	`01`	`1`		`@0 15-0039086`
A60				`@1 P`
A61				`@0 A`
A64	`01`	`1`		`@0 International journal of web services research`
A66	`01`			`@0 USA`
C01	`01`		`ENG`	@0 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.
C02	`01`	`X`		`@0 001D02B10`
C02	`02`	`X`		`@0 001D02B04`
C02	`03`	`X`		`@0 001D02A05`
C03	`01`	`X`	`FRE`	`@0 Vérification modèle @5 06`
C03	`01`	`X`	`ENG`	`@0 Model checking @5 06`
C03	`01`	`X`	`SPA`	`@0 Verificación modelo @5 06`
C03	`02`	`X`	`FRE`	`@0 Machine état fini @5 07`
C03	`02`	`X`	`ENG`	`@0 Finite state machine @5 07`
C03	`02`	`X`	`SPA`	`@0 Máquina estado finito @5 07`
C03	`03`	`X`	`FRE`	`@0 Service web @5 08`
C03	`03`	`X`	`ENG`	`@0 Web service @5 08`
C03	`03`	`X`	`SPA`	`@0 Servicio web @5 08`
C03	`04`	`X`	`FRE`	`@0 Orienté service @5 09`
C03	`04`	`X`	`ENG`	`@0 Service oriented @5 09`
C03	`04`	`X`	`SPA`	`@0 Orientado servicio @5 09`
C03	`05`	`X`	`FRE`	`@0 Coordination @5 10`
C03	`05`	`X`	`ENG`	`@0 Coordination @5 10`
C03	`05`	`X`	`SPA`	`@0 Coordinación @5 10`
C03	`06`	`X`	`FRE`	`@0 Intergiciel publication souscription @5 11`
C03	`06`	`X`	`ENG`	`@0 Publish subscribe middleware @5 11`
C03	`06`	`X`	`SPA`	`@0 Intergicial editor suscriptor @5 11`
C03	`07`	`X`	`FRE`	`@0 Vérification programme @5 12`
C03	`07`	`X`	`ENG`	`@0 Program verification @5 12`
C03	`07`	`X`	`SPA`	`@0 Verificación programa @5 12`
C03	`08`	`X`	`FRE`	`@0 Composition @5 18`
C03	`08`	`X`	`ENG`	`@0 Composition @5 18`
C03	`08`	`X`	`SPA`	`@0 Composicion @5 18`
C03	`09`	`X`	`FRE`	`@0 Processus service @5 19`
C03	`09`	`X`	`ENG`	`@0 Service process @5 19`
C03	`09`	`X`	`SPA`	`@0 Proceso servicio @5 19`
C03	`10`	`X`	`FRE`	`@0 Satisfiabilité @5 20`
C03	`10`	`X`	`ENG`	`@0 Satisfiability @5 20`
C03	`10`	`X`	`SPA`	`@0 Satisfactibilidad @5 20`
C03	`11`	`X`	`FRE`	`@0 Spécification modèle @5 21`
C03	`11`	`X`	`ENG`	`@0 Model specification @5 21`
C03	`11`	`X`	`SPA`	`@0 Especificación modelo @5 21`
C03	`12`	`X`	`FRE`	`@0 Exigence usager @5 22`
C03	`12`	`X`	`ENG`	`@0 User requirement @5 22`
C03	`12`	`X`	`SPA`	`@0 Exigencia usuario @5 22`
C03	`13`	`X`	`FRE`	`@0 Architecture basée modèle @5 23`
C03	`13`	`X`	`ENG`	`@0 Model driven architecture @5 23`
C03	`13`	`X`	`SPA`	`@0 Arquitectura basada modelo @5 23`
C03	`14`	`X`	`FRE`	`@0 Satisfaction contrainte @5 24`
C03	`14`	`X`	`ENG`	`@0 Constraint satisfaction @5 24`
C03	`14`	`X`	`SPA`	`@0 Satisfaccion restricción @5 24`
C03	`15`	`X`	`FRE`	`@0 Modélisation @5 25`
C03	`15`	`X`	`ENG`	`@0 Modeling @5 25`
C03	`15`	`X`	`SPA`	`@0 Modelización @5 25`
C03	`16`	`X`	`FRE`	`@0 Analyse statique @5 26`
C03	`16`	`X`	`ENG`	`@0 Static analysis @5 26`
C03	`16`	`X`	`SPA`	`@0 Análisis estática @5 26`
C03	`17`	`X`	`FRE`	`@0 . @4 INC @5 82`
N21				`@1 075`
N44	`01`			`@1 OTO`
N82				`@1 OTO`

Format Inist (serveur)

NO :	PASCAL 15-0039086 INIST
ET :	A Bounded Model Checking Approach for the Verification of Web Services Composition
AU :	ZAHOOR (Ehtesham); MUNIR (Kashif); PERRIN (Olivier); GODART (Claude); LUO (Min)
AF :	National University of Computer and Emerging Sciences/Islamabad/Pakistan (1 aut., 2 aut.); Laboratoire Lorrain de Recherche en Informatique et Ses Applications (LORIA), Universiteé de Lorraine/Lorraine/France (3 aut., 4 aut.); Shannon Lab/Huawei, Shenzhen/Chine (1 aut.)
DT :	Publication en série; Niveau analytique
SO :	International journal of web services research; ISSN 1545-7362; Etats-Unis; Da. 2013; Vol. 10; No. 4; Pp. 62-81; Bibl. 1 p.1/4
LA :	Anglais
EA :	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.
CC :	001D02B10; 001D02B04; 001D02A05
FD :	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; .
ED :	Model checking; Finite state machine; Web service; Service oriented; Coordination; Publish subscribe middleware; Program verification; Composition; Service process; Satisfiability; Model specification; User requirement; Model driven architecture; Constraint satisfaction; Modeling; Static analysis
SD :	Verificación modelo; Máquina estado finito; Servicio web; Orientado servicio; Coordinación; Intergicial editor suscriptor; Verificación programa; Composicion; Proceso servicio; Satisfactibilidad; Especificación modelo; Exigencia usuario; Arquitectura basada modelo; Satisfaccion restricción; Modelización; Análisis estática
LO :	INIST-28349.354000501855950030
ID :	15-0039086

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><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>
</affiliation>
</author>
<author><name sortKey="Munir, Kashif" sort="Munir, Kashif" uniqKey="Munir K" first="Kashif" last="Munir">Kashif Munir</name>
<affiliation><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>
</affiliation>
</author>
<author><name sortKey="Perrin, Olivier" sort="Perrin, Olivier" uniqKey="Perrin O" first="Olivier" last="Perrin">Olivier Perrin</name>
<affiliation><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>
</affiliation>
</author>
<author><name sortKey="Godart, Claude" sort="Godart, Claude" uniqKey="Godart C" first="Claude" last="Godart">Claude Godart</name>
<affiliation><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>
</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>
</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><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>
</affiliation>
</author>
<author><name sortKey="Munir, Kashif" sort="Munir, Kashif" uniqKey="Munir K" first="Kashif" last="Munir">Kashif Munir</name>
<affiliation><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>
</affiliation>
</author>
<author><name sortKey="Perrin, Olivier" sort="Perrin, Olivier" uniqKey="Perrin O" first="Olivier" last="Perrin">Olivier Perrin</name>
<affiliation><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>
</affiliation>
</author>
<author><name sortKey="Godart, Claude" sort="Godart, Claude" uniqKey="Godart C" first="Claude" last="Godart">Claude Godart</name>
<affiliation><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>
</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>
<inist><standard h6="B"><pA><fA01 i1="01" i2="1"><s0>1545-7362</s0>
</fA01>
<fA05><s2>10</s2>
</fA05>
<fA06><s2>4</s2>
</fA06>
<fA08 i1="01" i2="1" l="ENG"><s1>A Bounded Model Checking Approach for the Verification of Web Services Composition</s1>
</fA08>
<fA09 i1="01" i2="1" l="ENG"><s1>Services Discovery and Verification</s1>
</fA09>
<fA11 i1="01" i2="1"><s1>ZAHOOR (Ehtesham)</s1>
</fA11>
<fA11 i1="02" i2="1"><s1>MUNIR (Kashif)</s1>
</fA11>
<fA11 i1="03" i2="1"><s1>PERRIN (Olivier)</s1>
</fA11>
<fA11 i1="04" i2="1"><s1>GODART (Claude)</s1>
</fA11>
<fA12 i1="01" i2="1"><s1>LUO (Min)</s1>
<s9>ed.</s9>
</fA12>
<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>
</fA14>
<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>
</fA14>
<fA15 i1="01"><s1>Shannon Lab</s1>
<s2>Huawei, Shenzhen</s2>
<s3>CHN</s3>
<sZ>1 aut.</sZ>
</fA15>
<fA20><s1>62-81</s1>
</fA20>
<fA21><s1>2013</s1>
</fA21>
<fA23 i1="01"><s0>ENG</s0>
</fA23>
<fA43 i1="01"><s1>INIST</s1>
<s2>28349</s2>
<s5>354000501855950030</s5>
</fA43>
<fA44><s0>0000</s0>
<s1>© 2015 INIST-CNRS. All rights reserved.</s1>
</fA44>
<fA45><s0>1 p.1/4</s0>
</fA45>
<fA47 i1="01" i2="1"><s0>15-0039086</s0>
</fA47>
<fA60><s1>P</s1>
</fA60>
<fA61><s0>A</s0>
</fA61>
<fA64 i1="01" i2="1"><s0>International journal of web services research</s0>
</fA64>
<fA66 i1="01"><s0>USA</s0>
</fA66>
<fC01 i1="01" l="ENG"><s0>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.</s0>
</fC01>
<fC02 i1="01" i2="X"><s0>001D02B10</s0>
</fC02>
<fC02 i1="02" i2="X"><s0>001D02B04</s0>
</fC02>
<fC02 i1="03" i2="X"><s0>001D02A05</s0>
</fC02>
<fC03 i1="01" i2="X" l="FRE"><s0>Vérification modèle</s0>
<s5>06</s5>
</fC03>
<fC03 i1="01" i2="X" l="ENG"><s0>Model checking</s0>
<s5>06</s5>
</fC03>
<fC03 i1="01" i2="X" l="SPA"><s0>Verificación modelo</s0>
<s5>06</s5>
</fC03>
<fC03 i1="02" i2="X" l="FRE"><s0>Machine état fini</s0>
<s5>07</s5>
</fC03>
<fC03 i1="02" i2="X" l="ENG"><s0>Finite state machine</s0>
<s5>07</s5>
</fC03>
<fC03 i1="02" i2="X" l="SPA"><s0>Máquina estado finito</s0>
<s5>07</s5>
</fC03>
<fC03 i1="03" i2="X" l="FRE"><s0>Service web</s0>
<s5>08</s5>
</fC03>
<fC03 i1="03" i2="X" l="ENG"><s0>Web service</s0>
<s5>08</s5>
</fC03>
<fC03 i1="03" i2="X" l="SPA"><s0>Servicio web</s0>
<s5>08</s5>
</fC03>
<fC03 i1="04" i2="X" l="FRE"><s0>Orienté service</s0>
<s5>09</s5>
</fC03>
<fC03 i1="04" i2="X" l="ENG"><s0>Service oriented</s0>
<s5>09</s5>
</fC03>
<fC03 i1="04" i2="X" l="SPA"><s0>Orientado servicio</s0>
<s5>09</s5>
</fC03>
<fC03 i1="05" i2="X" l="FRE"><s0>Coordination</s0>
<s5>10</s5>
</fC03>
<fC03 i1="05" i2="X" l="ENG"><s0>Coordination</s0>
<s5>10</s5>
</fC03>
<fC03 i1="05" i2="X" l="SPA"><s0>Coordinación</s0>
<s5>10</s5>
</fC03>
<fC03 i1="06" i2="X" l="FRE"><s0>Intergiciel publication souscription</s0>
<s5>11</s5>
</fC03>
<fC03 i1="06" i2="X" l="ENG"><s0>Publish subscribe middleware</s0>
<s5>11</s5>
</fC03>
<fC03 i1="06" i2="X" l="SPA"><s0>Intergicial editor suscriptor</s0>
<s5>11</s5>
</fC03>
<fC03 i1="07" i2="X" l="FRE"><s0>Vérification programme</s0>
<s5>12</s5>
</fC03>
<fC03 i1="07" i2="X" l="ENG"><s0>Program verification</s0>
<s5>12</s5>
</fC03>
<fC03 i1="07" i2="X" l="SPA"><s0>Verificación programa</s0>
<s5>12</s5>
</fC03>
<fC03 i1="08" i2="X" l="FRE"><s0>Composition</s0>
<s5>18</s5>
</fC03>
<fC03 i1="08" i2="X" l="ENG"><s0>Composition</s0>
<s5>18</s5>
</fC03>
<fC03 i1="08" i2="X" l="SPA"><s0>Composicion</s0>
<s5>18</s5>
</fC03>
<fC03 i1="09" i2="X" l="FRE"><s0>Processus service</s0>
<s5>19</s5>
</fC03>
<fC03 i1="09" i2="X" l="ENG"><s0>Service process</s0>
<s5>19</s5>
</fC03>
<fC03 i1="09" i2="X" l="SPA"><s0>Proceso servicio</s0>
<s5>19</s5>
</fC03>
<fC03 i1="10" i2="X" l="FRE"><s0>Satisfiabilité</s0>
<s5>20</s5>
</fC03>
<fC03 i1="10" i2="X" l="ENG"><s0>Satisfiability</s0>
<s5>20</s5>
</fC03>
<fC03 i1="10" i2="X" l="SPA"><s0>Satisfactibilidad</s0>
<s5>20</s5>
</fC03>
<fC03 i1="11" i2="X" l="FRE"><s0>Spécification modèle</s0>
<s5>21</s5>
</fC03>
<fC03 i1="11" i2="X" l="ENG"><s0>Model specification</s0>
<s5>21</s5>
</fC03>
<fC03 i1="11" i2="X" l="SPA"><s0>Especificación modelo</s0>
<s5>21</s5>
</fC03>
<fC03 i1="12" i2="X" l="FRE"><s0>Exigence usager</s0>
<s5>22</s5>
</fC03>
<fC03 i1="12" i2="X" l="ENG"><s0>User requirement</s0>
<s5>22</s5>
</fC03>
<fC03 i1="12" i2="X" l="SPA"><s0>Exigencia usuario</s0>
<s5>22</s5>
</fC03>
<fC03 i1="13" i2="X" l="FRE"><s0>Architecture basée modèle</s0>
<s5>23</s5>
</fC03>
<fC03 i1="13" i2="X" l="ENG"><s0>Model driven architecture</s0>
<s5>23</s5>
</fC03>
<fC03 i1="13" i2="X" l="SPA"><s0>Arquitectura basada modelo</s0>
<s5>23</s5>
</fC03>
<fC03 i1="14" i2="X" l="FRE"><s0>Satisfaction contrainte</s0>
<s5>24</s5>
</fC03>
<fC03 i1="14" i2="X" l="ENG"><s0>Constraint satisfaction</s0>
<s5>24</s5>
</fC03>
<fC03 i1="14" i2="X" l="SPA"><s0>Satisfaccion restricción</s0>
<s5>24</s5>
</fC03>
<fC03 i1="15" i2="X" l="FRE"><s0>Modélisation</s0>
<s5>25</s5>
</fC03>
<fC03 i1="15" i2="X" l="ENG"><s0>Modeling</s0>
<s5>25</s5>
</fC03>
<fC03 i1="15" i2="X" l="SPA"><s0>Modelización</s0>
<s5>25</s5>
</fC03>
<fC03 i1="16" i2="X" l="FRE"><s0>Analyse statique</s0>
<s5>26</s5>
</fC03>
<fC03 i1="16" i2="X" l="ENG"><s0>Static analysis</s0>
<s5>26</s5>
</fC03>
<fC03 i1="16" i2="X" l="SPA"><s0>Análisis estática</s0>
<s5>26</s5>
</fC03>
<fC03 i1="17" i2="X" l="FRE"><s0>.</s0>
<s4>INC</s4>
<s5>82</s5>
</fC03>
<fN21><s1>075</s1>
</fN21>
<fN44 i1="01"><s1>OTO</s1>
</fN44>
<fN82><s1>OTO</s1>
</fN82>
</pA>
</standard>
<server><NO>PASCAL 15-0039086 INIST</NO>
<ET>A Bounded Model Checking Approach for the Verification of Web Services Composition</ET>
<AU>ZAHOOR (Ehtesham); MUNIR (Kashif); PERRIN (Olivier); GODART (Claude); LUO (Min)</AU>
<AF>National University of Computer and Emerging Sciences/Islamabad/Pakistan (1 aut., 2 aut.); Laboratoire Lorrain de Recherche en Informatique et Ses Applications (LORIA), Universiteé de Lorraine/Lorraine/France (3 aut., 4 aut.); Shannon Lab/Huawei, Shenzhen/Chine (1 aut.)</AF>
<DT>Publication en série; Niveau analytique</DT>
<SO>International journal of web services research; ISSN 1545-7362; Etats-Unis; Da. 2013; Vol. 10; No. 4; Pp. 62-81; Bibl. 1 p.1/4</SO>
<LA>Anglais</LA>
<EA>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.</EA>
<CC>001D02B10; 001D02B04; 001D02A05</CC>
<FD>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; .</FD>
<ED>Model checking; Finite state machine; Web service; Service oriented; Coordination; Publish subscribe middleware; Program verification; Composition; Service process; Satisfiability; Model specification; User requirement; Model driven architecture; Constraint satisfaction; Modeling; Static analysis</ED>
<SD>Verificación modelo; Máquina estado finito; Servicio web; Orientado servicio; Coordinación; Intergicial editor suscriptor; Verificación programa; Composicion; Proceso servicio; Satisfactibilidad; Especificación modelo; Exigencia usuario; Arquitectura basada modelo; Satisfaccion restricción; Modelización; Análisis estática</SD>
<LO>INIST-28349.354000501855950030</LO>
<ID>15-0039086</ID>
</server>
</inist>
</record>

Pour manipuler ce document sous Unix (Dilib)

EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/PascalFrancis/Corpus

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

HfdSelect -h $EXPLOR_AREA/Data/PascalFrancis/Corpus/biblio.hfd -nk 000001 | SxmlIndent | more

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

{{Explor lien
   |wiki=    Wicri/Lorraine
   |area=    InforLorV4
   |flux=    PascalFrancis
   |étape=   Corpus
   |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

Notice en format standard (ISO 2709)

Format Inist (serveur)

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