LTSmin: Difference between revisions

Revision as of 12:01, 9 June 2020

LTSmin Extension of ProB

LTSmin is a high-performance language-independent model checker that allows numerous modelling language front-ends to be connected to various analysis algorithms, through a common interface. We have implemented an integration of LTSmin with ProB for symbolic reachability and for explicit state model checking:

Symbolic Reachability Analysis of B Through ProB and LTSmin, Proceedings of iFM'2016
State-of-the-Art Model Checking for B and Event-B Using ProB and LTSmin, Proceedings iFM'2018.

In order to set up the LTSmin and ProB integraiton, do the following:

Download the latest LTSmin release: https://github.com/utwente-fmt/ltsmin/releases and extract it
(Linux only) start ProB via LD_LIBRARY_PATH=lib/ ./prob if you have not installed ZeroMQ and CZMQ
In ProB, go to Preferences > All Preferences (alphabetical)…
Set the LTSmin preference to the bin/ subfolder of the extracted LTSmin archive
Start Model Checking via Verify > External Tools > Model Checking with LTSmin

Note that the LTSmin extension is not available for Windows.

@@ Line 6: / Line 6: @@
 We have implemented an integration of LTSmin with ProB for symbolic reachability and for explicit state model checking:
-* [https://link.springer.com/chapter/10.1007%2F978-3-319-33693-0_18 Symbolic Reachability Analysis of B Through ProB and LTSmin]
+* [https://link.springer.com/chapter/10.1007%2F978-3-319-33693-0_18 Symbolic Reachability Analysis of B Through ProB and LTSmin], Proceedings of iFM'2016
 * [https://link.springer.com/chapter/10.1007%2F978-3-319-98938-9_16 State-of-the-Art Model Checking for B and Event-B Using ProB and LTSmin], Proceedings iFM'2018.