Welcome to ITS-tools Homepage
ITS-tools is an easy to use and powerful award-winning model-checker supporting Safety, CTL and LTL properties for a variety of formalisms. It formally proves system correctness using exhaustive state space exploration.
This tool won the following awards at the Model-Checking Contest 2021 edition :
Reachability, UpperBounds, GlobalProperties gold :
CTL, LTL silver :
StateSpace bronze :
It thus was on the podium of all categories of the contest, and outright won half of them. See the dedicated page for ITS-Tools in MCC if this is the scenario you are interested in.
Its architecture relies on an abstract contract for formalisms called Instantiable Transition Systems ITS that enables their semantic composition. An ITS is basically a labeled Kripke Structure but they can be instantiated and composed (think Composite DP).
Our main concrete formalism is the Guarded Action Language (GAL), featuring a simple yet user friendly C-like syntax. It is very expressive and has simple interleaving semantics suitable for modeling concurrent systems of practically any kind.
Our eclipse front-end offers rich textual editor (or graphical for Petri nets) for these formalisms.
If you’d prefer to use a command line tool, that is also possible using our pre-packaged ITS-tools for Windows, Linux or MacOS.
ITS-tools includes its own symbolic model-checker powered by Hierarchical Set Decision Diagrams, but can also use an SMT solver such as Yices or Z3 to perform BMC/ K-Induction, and export models with fine grain partial order analysis for use in the excellent multi-core model-checker LTSmin that offers its own solution engines.
These varied solution engines, GAL simple syntax, and EMF support make GAL an attractive target in a process targeting verification of a DSL.
Because we are dedicated to FOSS we use only free open-source licenses, depending on files we use EPL and APL for Java front-end,GPL for C++ tools using the kernel, LGPL for the symbolic kernel libDDD.
We cover a few different scenarios here, if you’re unsure just try the eclipse front-end.
End user oriented documentation
Using the composite formalism in GAL files.
Using parameters in GAL.
Writing properties in GAL for invariants, reachability, bounds, CTL or LTL.
A quick guide on Running the tool and configuring its options.
Technical and research documentation
Please cite our Symbolic Model-Checking Using ITS-Tools TACAS’15 paper if you are using the tool currently in your research, or a more specific paper if you are referring to a specific technique we use.
Yann Thierry-Mieg is the main designer and author of these tools, with important contributions from colleagues and students. Maximilien Colange and Alexandre Hamez contributed to the symbolic kernel, as well as Jean-Michel Couvreur and Denis Poitrenaud who wrote the original libDDD. Much code was borrowed and adapted (hacked !) from open-source model-checking projects with friendly licenses, such as LTSmin and VIS, to which we are grateful.
We owe a lot also to the Eclipse project and its dedication to open source, we use a large number of FOSS plugins in our code base, notably EMF and XText.
Much of the Eclipse front-end was prototyped during internships of students at Paris 6 University.
See acknowledgement sections at bottom of the various pages of this site for more detailed acknowledgments, as well as source history publicly visible on GitHub.