Paper Titles

Coordination Degree Analysis of Real Estate Investment and the National Economy in China - Based on Principal Component Analysis Method
p.2870

Research on Predicted Model of Least Squares Support Vector Machine Based on Genetic Algorithm
p.2875

The Design of Electronic Flat Guitar Based on LabVIEW
p.2882

Bayesian Estimations of Mixed Exponential Distribution with Type-I Censored Data
p.2887

Web Service Composition Verification of Safety Properties: An Approach Based on Predicate Abstraction
p.2892

A Hybrid Hypergraph Partitioning Algorithm for Scientific Computing
p.2900

Reliability Analysis for Link Mechanism under Influence of Multiple Factors Based on Support Vector Machine
p.2904

A Multilevel Hypergraph Partitioning Algorithm Based on Simulated Annealing
p.2908

An Out-of-Core Method for CFD Simulation in Heterogeneous Environment
p.2912

HomeAdvanced Materials ResearchAdvanced Materials Research Vols. 753-755Web Service Composition Verification of Safety...

Web Service Composition Verification of Safety Properties: An Approach Based on Predicate Abstraction

Article Preview

Abstract:

The biggest problem in model checking is state space explosion. Using predicate abstraction, state space of colored Petri net models were abstracted, and an algorithm was proposed to obtain the abstracted state space of a colored Petri net model without its original state space generated. A method to verify safety properties of Web service composition by abstracted state space was proposed. The problem of state space explosion is solved to some extend in this way. Finally an application of the method is illustrated with an example, which its efficiency shown.

You might also be interested in these eBooks

Materials Processing and Manufacturing III

Info:

Periodical:

Advanced Materials Research (Volumes 753-755)

Pages:

2892-2899

DOI:

https://doi.org/10.4028/www.scientific.net/AMR.753-755.2892

Citation:

Cite this paper

Online since:

August 2013

Authors:

Yu Ying Wang*, Ping Chen

Keywords:

Colored Petri Net, Model Checking, Predicate Abstraction, Safety Property, Web Service Composition

Export:

RIS, BibTeX

Price:

Permissions CCC:

Request Permissions

Permissions PLS:

Request Permissions

Сopyright:

© 2013 Trans Tech Publications Ltd. All Rights Reserved

Share:

Citation:

* - Corresponding Author

[1] Clarke E M, Grumberg O, and Peled DA. Model checking[M]. MIT Press, Cambridge, MA, USA, (1999).

[2] Lin H M, Zhang W H. Model Checking: Theory, Mothod and Application [J]．Chinese Journal of Electrinics, 2002, 12(3): 1906-912.

[3] Huth M, Ryan M. Logic in Computer Science[M]. Cambridge University Press: (2005).

[4] Khaxar M, Jalili S and Khakpour N. Monitoring Safety Properties of Composite Web Services at Runtime Using CSP[C]. proceeding of: Workshops Proceedings of the 12th IEEE International Enterprise Distributed Object Computing Conference, EDOCw 2009, September 2009, Auckland, New Zealand.

DOI: 10.1109/edocw.2009.5332007

[5] Breugel F van, Koshkina M. Models and Verification of BPEL [OL]. http: /www. cse. yorku. ca/~franck/research/drafts/tutorial. pdf. September (2006).

[6] Zhang G Q, Shi H J. Model Checking for Asynchronous Web Service Composition Based on XYZ/ADL[J]. Web Information Systems and Mining , Lecture Notes in Computer Science, 2011, 6988: 428-435.

DOI: 10.1007/978-3-642-23982-3_52

[7] Foster J S, Terauchi T, and Aiken A. Flow-sensitive type qualifiers[C]. In PLDI02: Programming Language Design and Implementation, ACM, 2002: 1-12.

DOI: 10.1145/512529.512531

[8] Das M, Lerner S, and Seigle M. ESP: Path-sensitive program verification in polynomial time[C]. In PLDI 02: Programming Language Design and Implementation, ACM, 2002: 57-68.

DOI: 10.1145/512529.512538

[9] Alur R, Itai A, Kurshan RP, et al. Timing verification by successive approximation[J]. Information and Computation, 1995, 118(1): 142-157.

DOI: 10.1006/inco.1995.1059

[10] Ball T , Rajamani SK. Automatically validating temporal safety properties of interfaces[C]. In SPIN 2001: SPIN Workshop, LNCS 2057, Springer-Verlag, 2001: 103-122.

DOI: 10.1007/3-540-45139-0_7

[11] Saidi H. Model checking guided abstraction and analysis[C]. In SAS 00: Static-Analysis Symposium,. LNCS 1824, Springer-Verlag, 2000: 377-396.

[12] Clarke E, Grumberg O, Jha S, et al. Counterexample-guided abstraction refinement[C]. In CAV 00: Computer Aided Verification, LNCS 1855, Springer-Verlag, 2000: 154-169.

DOI: 10.1007/10722167_15

[13] S. Das. Predicate Abstraction. Ph.D. Thesis. Department of Electrical Engineering, Stanford University, December (2003).

[14] S. Graf, H. Saidi. Construction of abstract state graphs with PVS. Proceedings of the 9th Conference on Computer-Aided Verification (CAV'97), Haifa, Israel, June 1997, pages72−83.

DOI: 10.1007/3-540-63166-6_10

[15] Clarke E M, Grumberg O, Long D E. Model checking and abstraction[J]. ACM Trans. Program, 1994, 16(5): 1512–1542.

DOI: 10.1145/186025.186051

[16] http: /wiki. daimi. au. dk/cpntools/cpntools. wiki[OL]. (2009).

[17] Kristensen L M. State Space Methods for Coloured Petri Nets[R]. Department of Computer Science, University of Aarhus, Denmark, (2000).

[18] Clarke E, Grumberg O, and Jha S, et al. Counterexample-guided abstraction refinement[C]. In CAV00: Computer Aided Verification, LNCS 1855, Springer-Verlag, 2000: 154-169.

DOI: 10.1007/10722167_15

[19] WANG Yu-ying, CHEN Ping. Models of BPEL's flow activity based on color Petri nets[J]. Application Research of Computers, 2011, 28(2): 631-634.

[20] WANG Yu-ying, CHEN Ping. Models of Web Services Composition Based on Timed Color Petri Nets [J]. COMPUTER SCIENCE, 2010, 37（10）：151-155.

[21] OASIS. Web Services Business Process Execution Language Version 2. 0[OL].

[22] Ranjit Jhala. Program Verification by Lazy Abstraction. Ph.D. Thesis. Computer Science, UNIVERSITY of CALIFORNIA at BERKELEY. Fall, (2004).