CitLab          NuSeen



 A Laboratory for Combinatorial Interaction Testing 

Although the research community around combinatorial interaction testing has been very active for several years, it has failed to find common solutions on some issues. First of all, there is not a common abstract nor concrete language to express combinatorial problems. Combinatorial testing generator tools are strongly decoupled making difficult their interoperability and the exchange of models and data. In this project, we propose an abstract and concrete specific language for combinatorial problems. It features and formally defines the concepts of parameters and types, constraints, seeds, and test goals. The language is defined by means of Xtext, a framework for the definition of domain-specific languages.  Xtext is used to derive a powerful editor integrated with eclipse and with all the expected features of a modern editor.

CITLab features: 

• A rich abstract language with a precise formal semantics for specifying combinatorial problems.

• A concrete syntax with a well-defined grammar that allows practitioners to write models and researchers to share examples and benchmarks written in a "common" notation. Besides the concrete syntax given in  Xtext, CITLab provides also an ANTLR grammar and an XMI interchange format for CIT models.

• A framework based on the Eclipse Modeling Framework (EMF) which provides tools and run-time support to (automatically) produce a set of Java classes for combinatorial models, along with a set of adapter classes and utility libraries that enable manipulating combinatorial problems in Java application using simple APIs. This allows developers to access combinatorial models inside their programs and tools.

• An editor integrated in the Eclipse IDE for editing combinatorial problems. The editor provides users with all the expected features in a modern programming environment like syntax highlighting, code completion, runtime error checking, quick fixes, and outline view. 

• A simple EMF meta-model also for combinatorial test suites.

• A rich collection of Java utility classes and methods, specifically developed for combinatorial problems in CITLab, which can be reused for manipulating combinatorial models and test suites. For instance, CITLab provides utility methods for generating all the test requirements for a combinatorial coverage of strength t, a set of methods to check if a test suite satisfies all the requirements, and a set of methods for semantic validation of models and test suites.

• A framework for introducing new test generation algorithms which can be added to CITLab as plugins. This allows researchers to develop new generation techniques and plug them in the framework without the burden of defining a grammar, a parser, an abstract syntax tree visitor, and so on.

• A framework for introducing code translators for importing and exporting models and tests to other notations based on Model to Text (M2T) or Model to Model (M2M) transformations. This could facilitate the use of CITLab language as language for exchanging models and benchmarks.



NuSeen: an eclipse-based environment for the NuSMV model checker

NuSeen is an eclipse-based environment for NuSMV, with the aim of helping NuSMV users. It mainly focuses in easing the use of the NuSMV tool by means of graphical elements like buttons, menu, text highlighting, and so on. It features:

  • language defined by a grammar (concrete syntax) and provided with metamodel (abstract syntax) - using Xtext
  • An editor that can be used to write NuSMV models and provides an useful feedback like syntax highlighting, autocompletion, and outline.
  • A way to execute the NuSMV model checker inside eclipse.
  • An integrated version of the model advisor which can be executed in eclipse.
  • new: a dependency decomposition tecnique that can be used for test generation


  • Paolo Arcaini
  • Angelo Gargantini
  • Elvinia Riccobene
  • Paolo Vavassori
  • Bruno Zambelli


Arcaini, Paolo, Gargantini, Angelo, and Vavassori, Paolo
NuSeen: an eclipse-based environment for the NuSMV model checker
in Eclipse-IT 2013 - VIII Workshop della Comunita' Italiana di Eclipse (2013) ISBN 978-88-904388-4-4
[abstract] [download the pdf file] [url]

Arcaini, Paolo, Gargantini, Angelo, and Riccobene, Elvinia
A Model Advisor for NuSMV Specifications
in Innovations in Systems and Software EngineeringSpringer London, vol. 7 (2011): 97-107
[abstract] [download the pdf file] [DOI]

How to install

Use the following eclipse update site:

The sourceforge project can be found here: