SpecSatisfiabilityTool for testing
specifications on XML documents SpecSatisfiabilityTool for testing
specifications on XML documents
SpecSatisfiabilityTool is a tool for testing the satisfiability of (a kind of) specifications on (abstract) XML documents, by means of a Refutation Procedure.
Specifications are given by means of constraints built on Boolean XPath patterns.
In particular, this tool allows you:
a) to test the satisfiability of a given specification (under two refutation algorithms),
b) to test if a given document is a model of a given specification,
c) to do some operations on patterns (which are the atoms of the constraints that conform the specifications).
At present, the application is written in Spanish. It includes some examples for easy first testing.
Version of SpecSatisfiabilityTool: July 2014 (but currently it is being improved!)
This application is portable, so it comes with no installation file. However, it is necessary to have already installed some external programs and configure them properly.
The application's requirements are the following ones:
- Operating System Windows 7/XP. The application might work with other versions of Windows, but no tests have been made on other versions of Windows nor on any other Operating Systems.
- SWI-Prolog. It is necessary to have installed the program SWI-Prolog, which will execute the logic of the application. It is possible to download it from http://www.swi-prolog.org/Download.html.
- Java. It is necessary to have installed Java 1.7 (jre7). As with the Operating System, we don't know if the application would work with other different Java versions.
Configuration of the Java-Prolog bridge. Once SWI-Prolog is installed, the configuration of the Java-Prolog bridge consists of two steps:
1. Creating an Environment Variable SWI_HOME_DIR. For that, go to "Control Panel -> System and Security -> System" (or go to "System Properties"). Click on "Advanced system settings" and click on the button "Environment Variables...". Then, click on "New..." in the "System Variables" panel and enter the following information:
Variable name: SWI_HOME_DIR
Variable value: SWI-Prolog's installation directory
2. Modifying the environment variable "Path". On the same screen than in the previous step ("Environment Variables...") look for the system variable "Path", select it and click on "Edit...". Enter as the variable value: %SWI_HOME_DIR%\bin. If the variable already had a value, do not delete its value. Add ";" and then write %SWI_HOME_DIR%\bin.
Download here: prototipo.zip
It is a zip file containing different files: The Java application SpecSatisfiabilityTool.jar to run the procedure; the Prolog program patrones.pl with the designed algorithms (used by the interface) and some example documents (that must be loaded from the interface).
The first algorithm of our Refutation Procedure (called version 1) consists of three main inference rules, named R1, R2 and R3, which are used to deduce more clauses from the input specification. The procedure also uses some subsumption and simplification rules, in order to delete and respectively simplify clauses during the refutation process. This procedure is sound: If the clause FALSE is deduced, then the input specification is insatisfiable. However this algorithm is not complete.
The second algorithm of our Refutation Procedure (called version 2) adds some unfolding rules, named Unfold1 and Unfold 2, to the previous algorithm in order to obtain a complete procedure (whose formal proof is now being studied). The new rules allow decomposing some positive literals in some clauses, for a greater applicability of the inference rules.
See below the related publications, in concrete see the Appendix A.3. Manual de uso (pg 105 in [1] ).
[1] Procedimiento de refutación para un conjunto de restricciones sobre documentos XML (in Spanish)
Javier Albors. Proyecto Fin de Carrera (supervised by Marisa Navarro), Facultad de Informática de San Sebastián (Julio 2014).
[2] Proving Satisfiability of Constraint Specifications on XML Documents
Navarro, M., and Orejas, F. Proceedings of X Jornadas sobre Programación y Lenguajes, CEDI2010, Valencia (2010).
[3] A Logic of Graph Constraints
Orejas, F., Ehrig, H., and Prange, U. Fundamental Approaches to Software Engineering, FASE 2008. LNCS 4961 (2008) 179-198.
This work has been partially supported by the Spanish Project TIN2007-66523.
Last Modified: 7 August 2014