Tools

NuSMV-ARCTL-TLACE

Contributors
Simon Busard, Franco Raimondi, José Vander Meulen
Tags
, ,

To link papers to this page, give a list of papers ids in the References field. (Same mechanism as the Research Themes pages)

NuSVM-ARCTL-TLACE is an extension of NuSMV adding two main functionalities: model checking of ARCTL and generation of tree-like annotated counter-examples.

ARCTL is an extension of the CTL logic adding action-restricted operators and is interpreted over Mixed Transition Systems.

A tree-like annotated counter-example gives all the information needed to understand why a given model does not satisfy a given specification.

This tool is composed of a modified version of NuSMV 2.2.2, able to model check ARCTL and to generate XML-format counter-examples, and TLACE Visualizer. TLACE Visualizer is a tool to visualize and browse tree-like annotated counter-examples.

Current version : NuSMV-TLACE-Dec2013.zip (06 Dec 2013)

If you want to add an historic, giving older versions, etc, you can do it here.

Historic

Contributor(s)
Simon Busard, Franco Raimondi, José Vander Meulen

Related Publications:

Tags Tags: , ,