SpecSatisfiabilityTool: A tool for testing the satisfiability of specifications on XML documents

TL;DR

SpecSatisfiabilityTool is a Prolog-based Java tool that tests satisfiability of XML specifications using logical rules on Boolean XPath patterns, providing visual explanations and pattern relations.

Contribution

Introduces a novel tool combining logical rule-based satisfiability testing with visual pattern relation analysis for XML specifications.

Findings

Successfully tests satisfiability of specifications

Visualizes pattern relations and pattern combinations

Proves the effectiveness of the tool in real use cases

Abstract

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.