Tools

Tools

This page presents the tools developed at LVL.

Interlocking Model
NuSMV model of the interlocking of NamÍche station in Belgium.

LTSA-Delforge
LTSA-Delforge is an extension of LTSA adding extensive LTS layout capabilities.

Milestones
The Milestones model checker combines symbolic techniques and POR. Its goal is to verify temporal properties on concurrents systems.

NuSMV-ARCTL-TLACE
NuSMV-ARCTL-TLACE is an extension of NuSMV adding two main functionalities: model checking of ARCTL and generation of tree-like annotated counter-examples. It is provided with a tool to visualize and browse tree-like annotated counter-examples.

PyNuSMV
PyNuSMV is a Python interface to NuSMV, allowing to use NuSMV as a Python library. It is composed of several classes representing NuSMV data structures and providing functionalities on these data.

{=$:ToolName}?
{=$:Summary}