Model checking for XML query evaluation

XMChecker (XML Model Checker) implements Simple XPath query evaluation via CTL
model checking. It exploits NuSMV extended with global_check_spec command, a state-of-art CTL model checker.

If you use these resources, please let us know. If you publish results obtained using the resources made available here, please include the following citation: XMChecker: Model Checking for XML Query Evaluation. ISLA, University of Amsterdam. URL:


XMChecker is written in Perl and consists of two translation subroutines, one for translating the tree representation of the XML document to NuSMV input format, and another for translating Simple XPath queries to CTL formulas. Besides these translations, it contains a subroutine that runs NuSMV, and a subroutine that interprets the truth set of a CTL formula, given in output by NuSMV, as a set of elements of the XML file.



In order to run first install:


usage: ./ [-c] [-d doc.xml] [-q "query"]


-d doc.xmldoc.xml is any XML document, conform the W3C specifications.
XMChecker extracts the tree representation of the XML document doc.xml and writes the explicit specification of the CTL model obtained into NuSMV input format. The output of the translation is doc.smv.-q "query"query is any Simple XPath query to be evaluated. XMChecker translates query into a CTL formula and outputs it to the standard output.-cmust be used in combination with -d doc.xml and -q "query". XMChecker invokes NuSMV to build an internal representation of (the translation of) doc.xml and then to perform global model checking on the CTL translation of query.



NuSMV extension with global_check_spec command


In order to use NuSMV with the new command you have to download the NuSMV source code at Follow the building instructions from README file.

Before compiling the source code download the modified source code of:

Replace the old source files with the new ones in the corresponding directories (nusmv/src/mc, nusmv/src/cmd and nusmv/src/prop) and follow further the indications in the README file of NuSMV.


The following command allows for the BDD-based global model checking of a NuSMV model. It runs in NuSMV interactive mode.

usage: global_check_spec [-h] [-m | -o file] [-n number | -p "ctl-expr"]

Prints the command usage.
Pipes output through the program specified by the “PAGER” environment variable if defined, else through the UNIX command “more”.
-o file
Writes the generated output to “file”.
-n number
Checks only the SPEC with the given index number.
-p "ctl-expr"
Checks only the given CTL formula and prints out the set of states that satisfies the formula.