Skip to Main content Skip to Navigation
Journal articles

Static analysis of active XML systems

Serge Abiteboul 1, 2 Luc Segoufin 2 Victor Vianu 3 
1 GEMO - Integration of data and knowledge distributed over the web
LRI - Laboratoire de Recherche en Informatique, UP11 - Université Paris-Sud - Paris 11, Inria Saclay - Ile de France, CNRS - Centre National de la Recherche Scientifique : UMR8623
2 DAHU - Verification in databases
LSV - Laboratoire Spécification et Vérification [Cachan], Inria Saclay - Ile de France
Abstract : Active XML is a high-level specification language tailored to data-intensive, 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, and so may activate new subtasks. The focus of this article is on the verification of temporal properties of runs of Active XML systems, specified in a tree-pattern-based temporal logic, Tree-LTL, which 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.
Document type :
Journal articles
Complete list of metadata
Contributor : Luc Segoufin Connect in order to contact the contributor
Submitted on : Tuesday, May 10, 2022 - 2:00:01 PM
Last modification on : Sunday, June 26, 2022 - 12:18:26 PM


Files produced by the author(s)



Serge Abiteboul, Luc Segoufin, Victor Vianu. Static analysis of active XML systems. ACM Transactions on Database Systems, Association for Computing Machinery, 2009, 34 (4), pp.1-44. ⟨10.1145/1620585.1620590⟩. ⟨hal-03663772⟩



Record views


Files downloads