SpecSatisfiabilityTool: A tool for testing the satisfiability of specifications on XML documents
This tool addresses the need for verifying XML specifications in domains like data validation or software engineering, but it is incremental as it builds on existing logical methods with a new interface.
The authors tackled the problem of testing the satisfiability of specifications on XML documents using Boolean XPath patterns, resulting in a prototype tool that implements logical rules to prove satisfiability, justify decisions with execution history, and visually show operations like finding relations between patterns.
We present a prototype that implements a set of logical rules to prove the satisfiability for a class of specifications on XML documents. Specifications are given by means of constrains built on Boolean XPath patterns. The main goal of this tool is to test whether a given specification is satisfiable or not, and justify the decision showing the execution history. It can also be used to test whether a given document is a model of a given specification and, as a by-product, it permits to look for all the relations (monomorphisms) between two patterns and to combine patterns in different ways. The results of these operations are visually shown and therefore the tool makes these operations more understandable. The implementation of the algorithm has been written in Prolog but the prototype has a Java interface for an easy and friendly use. In this paper we show how to use this interface in order to test all the desired properties.