Projection Temporal Logic Oriented Model Checking for Web Services
Zhenhua Duan · Xi'an Jiaotong Daxue xuebao · 2009
To satisfy the reliability of web services,a model checking approach with the projection temporal logic(PTL) is adopted to verify web services.An executable subset of PTL is used to model OWL-S,and the propositional projection temporal logic(PPTL) is selected to describe desired properties.The model M and property P are both presented in PTL,then the aim of model checking is obtained by determining the validity of M implies P,namely,the unsatisfiability of the conjunction of M and not P,and the unsatisfiability of the conjunction is checked by constructing its normal form graph with the help of the normal forms of M and not P.Executing the example,it shows that the presented model checker can be used to verify the system properties and hence to ensure the reliability of web services.