LTSmin is a toolset for model checking and manipulating labelled transition systems. LTSmin already connects a sizeable number of existing (verification) tools: muCRL, mcrl2, DiVinE, SPIN via an included version of SpinJa, NIPS, CADP and opaal. Moreover, it allows to reuse existing tools with new state space generation techniques. Implementing support for a new language module is in the order of 200–600 lines of C ”glue” code, and automatically yields tools for standard reachability checking (e.g., for state space generation and verification of safety properties), reachability with symbolic state storage (vector set), fully symbolic (BDD-based) reachability, distributed reachability (MPI-based), and multi-core reachability (including multi-core compression and incremental hashing). The synergy effects in the LTSmin implementation are enabled by a clean interface: all LTSmin modules work with a unifying state representation of integer vectors of fixed size, and the PINS dependency matrix which exploits the combinatorial nature of model checking problems. This splits model checking tools into three mostly independent parts: language modules, PINS optimizations, and model checking algorithms. On the other hand, the implementation of a verification algorithm based on the PINS matrix automatically has access to muCRL, mcrl2, DVE, PROMELA, opaal and ETF language modules. Finally, all tools benefit from PINS2PINS optimizations, like local transition caching (which speeds up slow state space generators), matrix regrouping (which can drastically reduce run-time and memory consumption of symbolic algorithms), partial order reduction and linear temporal logic.
Keywords for this software
References in zbMATH (referenced in 11 articles )
Showing results 1 to 11 of 11.
- Barnat, Jiří: Quo vadis explicit-state model checking (2015)
- Garavel, Hubert; Lang, Frédéric; Mateescu, Radu: Compositional verification of asynchronous concurrent systems using CADP (2015)
- Cranen, Sjoerd; Groote, Jan Friso; Keiren, Jeroen J.A.; Stappers, Frank P.M.; de Vink, Erik P.; Wesselink, Wieger; Willemse, Tim A.C.: An overview of the mCRL2 toolset and its recent advances (2013)
- Křena, Bohuslav; Vojnar, Tomáš: Automated formal analysis and verification: an overview (2013)
- Barnat, Jiří; Bauch, Petr; Brim, Luboš; Češka, Milan: Designing fast LTL model checking algorithms for many-core GPUs (2012) ioport
- Dalsgaard, Andreas E.; Laarman, Alfons; Larsen, Kim G.; Olesen, Mads Chr.; van de Pol, Jaco: Multi-core reachability for timed automata (2012)
- Evangelista, Sami; Laarman, Alfons; Petrucci, Laure; van de Pol, Jaco: Improved multi-core nested depth-first search (2012)
- Hwong, Yi-Ling; Kusters, Vincent J.J.; Willemse, Tim A.C.: Analysing the control software of the compact Muon Solenoid experiment at the large hadron collider (2012) ioport
- Wijs, A.J.; Dashti, M.Torabi: Extended beam search for non-exhaustive state space analysis (2012)
- Laarman, Alfons; Langerak, Rom; van de Pol, Jaco; Weber, Michael; Wijs, Anton: Multi-core nested depth-first search (2011)
- Laarman, Alfons; van de Pol, Jaco; Weber, Michael: Multi-core LTSmin: Marrying modularity and scalability (2011) ioport
Further publications can be found at: http://fmt.cs.utwente.nl/tools/ltsmin/#sec2