Paper Info
Title
Modeling and Verifying Web Service Applications with Time Constraints
Abstract
Web services are a very appropriate communication mechanism to perform distributed business processes among several organizations. These processes should be reliable, because a failure in them can cause high economic losses. In this paper, we present an approach to verify Web Service applications with time restrictions which are defined by BPEL4WS using model checking techniques. We introduce a formalism, called WS Timed Automata, to capture the timed behavior of the web service applications, and methods to translate description of web service applications written in BPEL4WS to WS Timed Automata is proposed in this paper. The formal verification tool Uppaal is used to verify related properties of the system. A particular case study, an airline travel reservation system is taken as illustration.
Year
DOI
Venue
2010
10.1109/ICIS.2010.20
ACIS-ICIS
Keywords
Field
DocType
automata theory,bpel4ws,airline travel reservation system,economic losses,communication mechanism,distributed business processes,web services,travel industry,formal verification tool,model checking,ws timed automata,high economic loss,web service application,business process,time constraints,web service,appropriate communication mechanism,model checking technique,verifying web service applications,uppaal,particular case study,formal verification,timed automata,model checking techniques,business,service model,automata,unified modeling language,xml
Automata theory,Model checking,Unified Modeling Language,Software engineering,Business process,Computer science,Automaton,Web modeling,Web service,Database,Formal verification
Conference
ISBN
Citations 
PageRank 
978-1-4244-8198-9
0
0.34
References 
Authors
7
4
Name
Order
Citations
PageRank
Jia Mei1162.75
Huaikou Miao245168.03
Qingguo Xu3174.11
Pan Liu4173.42