LoLA: 1.17 - A Low Level Petri Net Analyser

LoLA is a tool that can verify a broad variety of behavioral properties on a
given Petri net. It is based on explicit state space verification, i.e. an
exhaustive enumeration of reachable state. LoLA gets its power from several
state-of-the-art state space reduction techniques. These techniques have the
effect that only a tiny portion of the overall state space is explored which,
however, behaves equivalently to the original state space with respect to the
investigated property.

LoLA has been implemented for the validation of reduction techniques for
place/transition net state spaces. Its particular strengths include:

- A large number of available state space reduction techniques many of which
  may be applied jointly;
- A high degree of automation for various state space reduction techniques
- Availability of dedicated variations of state space reduction techniques
  for several frequently used properties
- efficient implementation exploiting the particular nature of Petri net models
- simple textual interaction for easy integration into other tools

Signed-off-by: Adam Vandenberg <flangy@gmail.com>
GNU BPEL2oWFN: 2.4 - from BPEL to Petri nets

GNU BPEL2oWFN translates a Web service expressed in WS-BPEL (Web Service
Business Process Execution Language) into a Petri net model. This model can be
used to:

- check for controllability or generate the operating guideline using the
  tools Fiona or Wendy,
- check for deadlocks or any other Petri net property, or
- check any temporal logic formula with a variety of model checking tools.

Furthermore, GNU BPEL2oWFN can translate a BPEL4Chor choreography to a Petri
net model. This model can be used to analyze properties of a complete
choreography or to synthesize a fitting service for an incomplete choreography.

GNU BPEL2oWFN uses static analysis to make the generated Petri net model as
compact as possible to analyze a chosen property. This is called flexible model
generation. Furthermore, several design flaws can be detected using control and
data flow analysis.

Signed-off-by: Adam Vandenberg <flangy@gmail.com>
Genet: 1.2 - Generalised Net Synthesis

Genet is a tool for the synthesis and mining of Petri nets from transition
systems. The tool is based on the theory of regions. The input of the tool is a
transition system and, depending on the usage of the tool, it can generate a
k-bounded Petri net with reachability graph

- bisimilar to the input transition system (synthesis), or
- with (maybe proper) superset language of the input's transition system
  language (mining).

Signed-off-by: Adam Vandenberg <flangy@gmail.com>
NuSMV: 2.54 - A Symbolic Model Checker

NuSMV is a reimplementation and extension of SMV, the first model checker based
on BDDs. NuSMV has been designed to be an open architecture for model checking,
which can be reliably used for the verification of industrial designs, as a
core for custom verification tools, as a testbed for formal verification
techniques, and applied to other research areas.

NuSMV2, combines BDD-based model checking component that exploits the CUDD
library developed by Fabio Somenzi at Colorado University and SAT-based model
checking component that includes an RBC-based Bounded Model Checker, which can
be connected to the Minisat SAT Solver and/or to the ZChaff SAT Solver. The
University of Genova has contributed SIM, a state-of-the-art SAT solver used
until version 2.5.0, and the RBC package use in the Bounded Model Checking
algorithms.

Signed-off-by: Adam Vandenberg <flangy@gmail.com>