New screencast from nusmv-tools

I created a screencast which shows the features of the nusmv-tools Eclipse editor. The editor is build using Xtext, so many thanks to the itemis AG team!

You can watch the video also in HD.

nusmv-tools Eclipse editor in action from Siamak Haschemi on Vimeo.

Happy model editing!

Access NuSMV from Java

NuSMV is a symbolic model checker, which I use as part of my PhD thesis. However, NuSMV is written in C and I could not found any Java API to use the model checker from Java. Luckily, creating Java libraries out from C-headers becomes very easy by using JNA and JNAerator:

JNA stands for Java Native Access and is a alternative to JNI, the official way to access shared native libraries. The advantage of JNA is the dynamic binding to shared libraries, whithout writing anything but Java code. Principally, you write a Java Interface with methods machting the corresponding C-header of the library and provide that Java Interface to JNA. More info‘s and examples can be found on the project‘s website.

While JNA provides the dynamic bridging between calls to the java interface, you still have to write the Java Interface and therefore you also need the knowledge about the conversion conventions from C to Java. Here comes JNAerator into the game. JNAerator is a tool to parse C headers and generate the corresponding JNA Java Interfaces. It comes with a Graphical User Interface, but can also be used on the command-line.

To create a Java API for NuSMV, first a dynamic library has to be created out of the sources. Unfortunately, this library is not created by the make files. I host some scripts for the current NuSMV 2.5.2 to help you out with windows, linux, and osx.
Having the shared library for NuSMV (nusmv.dll, libnusmv.so, libnusmv.jnilib), we can go an create the Java API using JNAerator (I also host the script for that). What we get is a java interface which now gives us access to NuSMV.

Accessing NuSMV becomes now as easy as:

import static org.eclipselabs.nusmvtools.nusmv4j.NusmvLibraryUtil.toByteBuffer;

import java.io.File;
import java.io.PrintStream;

import org.eclipselabs.nusmvtools.nusmv4j.NuSMV4J;
import org.eclipselabs.nusmvtools.nusmv4j.NusmvLibrary;

public class Main {
  public static void main(final String[] args) throws Exception {
    final File file = new File("testModel.nusmv");
    final PrintStream ps = new PrintStream(file);
    ps.println("MODULE main");
    ps.println("  VAR");
    ps.println("    x : boolean;");
    ps.flush();
    ps.close();

    final NusmvLibrary nusmvLibrary = NuSMV4J.getNusmvLibrary();
    nusmvLibrary.Cmd_CommandExecute(toByteBuffer("reset"));
    nusmvLibrary.Cmd_CommandExecute(toByteBuffer("set default_trace_plugin 4"));
    nusmvLibrary.Cmd_CommandExecute(toByteBuffer("read_model -i testModel.nusmv"));
    nusmvLibrary.Cmd_CommandExecute(toByteBuffer("go"));
    nusmvLibrary.Cmd_CommandExecute(toByteBuffer("check_ctlspec -p \"!x\""));
    nusmvLibrary.Cmd_CommandExecute(toByteBuffer("show_traces"));

    file.delete();
  }
}

When you run the above class, you get the following line on the console:

-- specification !x  is false
-- as demonstrated by the following execution sequence
<?xml version="1.0" encoding="UTF-8"?>
<counter-example type="0" desc="CTL Counterexample" >
  <node>
    <state id="1">
      <value variable="x">TRUE</value>
    </state>
  </node>
  <loops> </loops>
</counter-example>

If you don't want to take the above steps on your own, you should take a look at my project nusmv-tools, which contains some Eclipse based tools like an Eclipse editor for NuSMV files (see blow), an API to read the NuSMV counterexamples in java, a model advisor, and the libraries for accessing NuSMV from java, which I presented in this post.



Happy model checking!

Verify And Beautify Model-2-Text Transformation Output

One of the projects which I developed during my PhD thesis is Azmun, a model based testing framework based on various MDD technologies. One of the tasks within Azmun is to transform an UML-based test model to a model checking problem in order to use a model checker for automated test case generation. Although Azmun does not require a specific model checker, I mostly use NuSMV for my research. NuSMV has an own language to describe a system, and I developed a model-2-text (m2t) transformation from UML to NuSMV using Xpand. And here comes the problem:

Q: How do we ensure that the output of our Xpand transformation is syntactically correct, and how can we format our output?

These two questions may seem to be independend, but as you will see in a minute, we can tackle both problems with one approach. As a side project, I created the nusmv-tools Eclipselabs project, which hosts some Eclipse-based tools. One of these tools is a rich text editor based on Xtext. And now we have the solution for our problem:

A: We create a Xpand beautifier based on the Xtext parser and serializer.

The following lines show how we solve our problem in Azmun:

public final class NuSMVCodeGenerator extends WorkflowComponentWithModelSlot {
  private Generator m_generator = null;

  @Override
  public void checkConfiguration(final Issues p_issues) {
    super.checkConfiguration(p_issues);

    m_generator = new Generator();
    m_generator.addMetaModel(new UML2MetaModel());
    // add other metamodels

    m_generator.setFileEncoding("utf-8");
    m_generator.setExpand("foo::bar::UML2NuSMV() FOR " + getModelSlot());

    final Outlet outlet = new Outlet("/some/path");
    outlet.addPostprocessor(new PostProcessor() {

      @Override
      public void beforeWriteAndClose(final FileHandle p_fileHandle) {
      }

      @Override
      public void afterClose(final FileHandle p_fileHandle) {
        try {
          if (p_fileHandle.getAbsolutePath() == null 
            || !p_fileHandle.getAbsolutePath().endsWith(".nusmv")) {
            return;
          }
          NuSMVStandaloneSetup.doSetup();
          final ResourceSet resourceSet = new ResourceSetImpl();
          final URI fileURI = URI.createFileURI(p_fileHandle.getAbsolutePath());
          final Resource resource = resourceSet.getResource(fileURI, true);
          for (final Diagnostic diagnostic : resource.getWarnings()) {
            p_issues.addWarning(diagnostic.getMessage());
          }
          for (final Diagnostic diagnostic : resource.getErrors()) {
            p_issues.addError(diagnostic.getMessage());
          }
          if (!resource.getErrors().isEmpty()) {
            return;
          }
          final SaveOptions saveOptions = SaveOptions.newBuilder().format().getOptions();
          resource.save(saveOptions.toOptionsMap());
        } catch (final Exception e) {
          throw new RuntimeException(e);
        }
      }
    });
    m_generator.addOutlet(outlet);
    m_generator.checkConfiguration(p_issues);
  }

  @Override
  protected void invokeInternal(final WorkflowContext p_ctx, 
      final ProgressMonitor p_monitor, final Issues p_issues) {
    m_generator.invoke(p_ctx, p_monitor, p_issues);
    m_generator = null;
  }
}

We configure the Xpand workflow component with a PostProcessor, which is called for every file we create during the m2t transformation. In the afterClose method, we load the generated file using the standard EMF ResourceSet mechanism, and immediately save the resource. The options we add to the Resource.save method specify that we want the output to be formatted by Xtext.

With this approach, we can be sure that the output we generate in the m2t transformations conforms to the NuSMV language. And as a side-effect we format our output.

Happy transforming!