Simon Busard, Franco Raimondi, Josť Vander Meulen
, ,

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 : (06 Dec 2013)

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


Simon Busard, Franco Raimondi, Josť Vander Meulen

Related Publications: