Beetlz Summary

Beetlz is a consistency (refinement) checker for BON, the Business Object Notation (BON), and JML-annotated Java. It was originally developed as part of an undergraduate final year project. It takes your source files and specifications as input and returns feedback on whether and where they are inconsistent. The tool is available in a command-line and in a Eclipse plugin version.

Beetlz is being developed by Eva Darulova and Fintan Fairmichael under the supervision of Joe Kiniry.

More information on the Business Object Notation is found on the BON website, and by reading the book "Seamless Object-oriented Software Architecture: Analysis and Design of Reliable Systems" which is freely available on that site, since it is out of print.

Beetlz is written in Java and will run correctly on any system with a 1.6/6.0 or later virtual machine. It is based upon the BONc and OpenJML tool suites.

The latest pre-alpha version of Beetlz plugin is obtained from the BONc/Beetlz update site:

The command-line version and nicely packaged source distribution will be available on the first public release of Beetlz.


Please log problem tickets using the Mobius Trac at the following URL (requires a short registration):

Please include the following details (where possible):

  • the command-line arguments with which you invoked the tool
    (e.g., "beetlz -pureBON -noNullCheck bon/system.bon src"),
  • the operating system and Java VM version you are using,
  • any input files used to recreate the bug, and
  • the output generated when you detected the bug.

Filing bugs will help to improve this software, so if you notice something amiss please do report it!