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...

• Type: Conference
• Year: 2004
• Where: ISSTA
• Authors: Xiang Fu, Tevfik Bultan, Jianwen Su
• Keywords: Expressive Xml Query, ISSTA 2004, XML Data, XML Data Manipulation