Static analysis of active XML systems

Active XML is a high-level specification language tailored to dataintensive, distributed, dynamic Web services. Active XML is based on XML documents with embedded function calls. The state of a document evolves depending on the result of internal function calls (local computations) or external ones (interactions with users or other services). Function calls return documents that may be active, so may activate new subtasks. The focus of the paper is on the verification of temporal properties of runs of Active XML systems, specified in a tree-pattern based temporal logic, Tree-LTL, that allows expressing a rich class of semantic properties of the application. The main results establish the boundary of decidability and the complexity of automatic verification of Tree-LTL properties. Categories and Subject Descriptors: H.2.3 [Database Management]: Languages ? XML General Terms: Reliability, Theory, Verification

• Type: Conference
• Year: 2008
• Where: PODS
• Authors: Serge Abiteboul, Luc Segoufin, Victor Vianu
• Keywords: Active XML, Active XML Systems, Database, Function Calls, PODS 2008