Model checking XML manipulating software

13 years 10 months ago
Model checking XML manipulating software
The use of XML as the de facto data exchange standard has allowed integration of heterogeneous web based software systems regardless of implementation platforms and programming languages. On the other hand, the rich tree-structured data representation, and the expressive XML query languages (such as XPath) make formal specification and verification of software systems that manipulate XML data a challenge. In this paper, we present our initial efforts in automated verification of XML data manipulation operations using the SPIN model checker. We present algorithms for translating (bounded) XML data and XPath expressions to Promela, the input language of SPIN. The techniques presented in this paper constitute the basis of our Web Service Analysis Tool (WSAT) which verifies LTL properties of composite web services. Categories and Subject Descriptors D.2.4 [Software Engineering]: Software/Program Verification— formal methods, model checking General Terms Verification, Design Keywor...
Xiang Fu, Tevfik Bultan, Jianwen Su
Added 30 Jun 2010
Updated 30 Jun 2010
Type Conference
Year 2004
Authors Xiang Fu, Tevfik Bultan, Jianwen Su
Comments (0)