Basset: A Tool for Systematic Testing of Actor Programs

Welcome to the Basset project homepage. Basset is a tool and framework that allows users to systematically test actor programs that compile to Java bytecode. Basset is an extension for the Java PathFinder model checker developed at NASA Ames. Basset can currently check actor programs written in the Scala programming language or the ActorFoundry library for Java.

On This Page

• Publications
• Download
• Build
• Run
• Acknowledgements

Publicationsback to the top

A Framework for State-Space Exploration of Java-based Actor Programs

By Steven Lauterburg, Mirco Dotta, Darko Marinov, Gul Agha.
In Proc. of 24th IEEE/ACM International Conference on Automated Software Engineering
(ASE 2009), Auckland, New Zealand, November 2009. [pdf].

Evaluating Ordering Heuristics for Dynamic Partial-order Reduction Techniques

By Steven Lauterburg, Rajesh K. Karmani, Darko Marinov, Gul Agha.
In Proc. of Fundamental Approaches to Software Engineering
(FASE 2010), Paphos, Cyprus, March 2010. [pdf].

Mutation Operators for Actor Systems

By Vilas Jagannath, Milos Gligoric, Steven Lauterburg, Darko Marinov, Gul Agha.
In the 5th International Workshop on Mutation Analysis
(Mutation 2010), Paris, France, April 2010. [pdf].

Basset: A Tool for Systematic Testing of Actor Programs

By Steven Lauterburg, Rajesh K. Karmani, Darko Marinov, Gul Agha.
In the 18th ACM SIGSOFT International Symposium on the Foundations of Software Engineering, Formal Research Demonstration
(FSE Demo 2010), Santa Fe, NM, November 2010. [pdf].

Downloadback to the top

• Download the latest version of the Java PathFinder core (jpf-core) from the JPF website. (You should choose to download and build JPF from the Mercurial source repository; the provided binary snapshots are for an older version of jpf-core that is not compatible with Basset.) The following instructions assume that you will use default directory locations when installing JPF.

  mkdir ~/projects/jpf
  cd ~/projects/jpf
  hg clone http://babelfish.arc.nasa.gov/hg/jpf/jpf-core
  

• Download the latest version of the Basset extension (jpf-actor) from the JPF source repository.

  cd ~/projects/jpf
  hg clone http://babelfish.arc.nasa.gov/hg/jpf/jpf-actor
  

  Make sure to create a JPF site.properties file in your ~/.jpf directory as directed in the jpf-core installation instructions. Add the location of the jpf-actor extension to this file. If you have not previously used JPF, your site.properties file should look something like:

  jpf.home = ${user.home}/projects/jpf
  jpf-core = ${jpf.home}/jpf-core
  jpf-actor = ${jpf.home}/jpf-actor
  ...
  extensions=${jpf-core}
  

• If you wish to use Basset's Scala language support, you will need to download two Scala archive files (the compiler and the runtime library) into Basset's lib directory. Basset was tested to work with at least version 2.7.3.

  cd ~/projects/jpf/jpf-actor/lib
  wget http://mir.cs.illinois.edu/basset/scala-compiler-2.7.3.jar
  wget http://mir.cs.illinois.edu/basset/scala-library-2.7.3.jar
  

Buildback to the top

• Use ant to build the jpf-core and jpf-actor projects.

  cd ~/projects/jpf/jpf-core
  bin/ant
  # ... lots of output, at the end you should see something like:
  # BUILD SUCCESSFUL
  cd ~/projects/jpf/jpf-actor
  bin/ant
  # ... lots of output, at the end you should see something like:
  # BUILD SUCCESSFUL
  

Runback to the top

• To explore the ActorFoundry subjects provided in src/examples, run Basset under JPF, additionally specifying the fully qualified class name for the subject's test driver along with any applicable arguments for the driver. For example, the following command will test the ActorFoundry program "pi" using one master actor and three worker actors. This may take a minute to run.

  bin/jpf gov.nasa.jpf.actor.Basset pi.Driver 3

• Similarly, the following command will test the Scala program "server" provided in scala-src/examples. Note the addition of the option "+basset.language=scala". In the example above, no language was specified as "foundry" is the default for Basset. Defaults such as this can be overridden in the jpf.properties file located in the actor-jpf directory.

  bin/jpf +basset.language=scala gov.nasa.jpf.actor.Basset scalaexamples.clientserver.ClientServer

• To apply a dynamic partial-order reduction (DPOR) to the exploration of a subject, specify which DPOR you would like to use. For example, to explore our "pi" subject using a DPOR based on persistent sets, use the following command, which will result in a significantly smaller exploration space.

  bin/jpf +basset.dpor=3 gov.nasa.jpf.actor.Basset pi.Driver 3

Acknowledgementsback to the top

This material is based upon work partially supported by the National Science Foundation under Grant Nos. CCF-0916893, CNS-0851957, CCF-0746856, CNS-0615372, and CNS-0509321. Any opinions, findings, and conclusions or recommendations expressed in this material are those of the author(s) and do not necessarily reflect the views of the National Science Foundation (NSF).

Milos Gligoric was supported by the Saburo Muroga fellowship while working on a part of this project.

We would like to thank Stoyan Gaydarov, Bobak Hadidi, Viktor Kuncak, P. Madhusudan, Edgar Pek, Vasko Popstojanov, and Samira Tasharofi for discussions and other assistance during the course of this project.

We thank the students from the "CS 598GA: Actor Languages, Compilers and Runtime Systems" (Fall 2009 and Fall 2008), "CS 524: Concurrent Programming Languages" (Spring 2009), and "CS 427: Software Engineering I" (Fall 2009) classes at the University of Illinois for constructive feedback on Basset.