- Bomotest is a
formal conformance testing tool for the ioco-conformance. It uses labeled 1-bounded
Petri nets as its specification model, and employs specification coverage based test
selection heuristic incorporating bounded model checking algorithms.
This is joint work with Tuomo Pyhälä.
- boundsmodels is a bounded LTL-X model
checker which generates logic programs with stable model semantics from 1-bounded Petri nets.
It supports step and interleaving semantics.
- punroll is a bounded reachability
checker which generates constrained Boolean circuits from 1-bounded Petri nets. It supports
process, step, and interleaving semantics.
- unfsmodels is an LTL-X model checker with net unfoldings.
- mcsmodels is a deadlock
and reachability checker using finite complete prefixes generated by the
tool from 1-bounded Petri nets.
It uses the smodels constraint-based
logic programming system as its computational engine.
- PROD is a reachability analyzer
for Pr/T-nets with advanced features such as : stubborn sets, sleep sets, on-the-fly tester based
verification, on-the-fly LTL model checking, CTL model checking. The main authon of PROD
is Kimmo Varpaaniemi, I just implemented
the CTL model checking part.
- dlsmodels is an older version
of mcsmodels limited to deadlock checking only.