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.

Thanks to this central pivot and model to model transformations that leverage EMF, we can support many commonly used formalisms in other tools such as Spin or Uppaal.

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.

Getting started

We cover a few different scenarios here, if you’re unsure just try the eclipse front-end.

I want to use the eclipse front-end

I want to use the command line Model-Checking Contest edition of the tool

I want to use the command line symbolic tools only

I’m interested in contributing

End user oriented documentation

GAL presentation and syntax, see also GAL meta-model for more technical details.

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.

Working with Time Petri nets (compatible with Tina, Romeo)

Working with Timed Automata.

Working with DVE models.

Working with Promela/Spin models.

Working with LTSmin.

Technical and research documentation

LibDDD our C++ library for Hierarchical Set Decision Diagrams.

LibITS our C++ library for symbolic model-checking of ITS and related tools.

Choosing an LTL algorithm

Scientific papers on the tool and its algorithms.

Citing

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.

Reporting Issues

Please use the Github integrated issues page to report issues you might encounter or mail me if you don’t have a GitHub account.

Acknowledgments

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.