BON Software Model Consistency Checker for Eclipse

Note: This project (together with an Eclipse plugin) was completed successfully as a 2008-2009 Final Year Project by Eva Darulova. The project is called Beetlz (report | website).

Summary of Eva's Work

Beetlz - BON Software Model Consistency Checker for Eclipse

Winner of IBM Open Source Software competition
Eva Darulova, UCD 2009

Development of a software project usually involves, to some extent, both modelling and specification languages. Although both are useful in their own right, using them together in an interconnected way brings many benefits to all stages of the development process. Work can proceed on both the model and the implementation concurrently. However, this approach requires tool support that keeps the two versions consistent and updates them when necessary. This report discusses the theoretical and practical considerations of a such a combination between the Business Object Notation and Java, together with the Java Modelling Language. It defines and discusses relations between individual concepts and presents their implementation in the automatic consistency checking Eclipse IDE plugin and tool "Beetlz".

Consistency checks are commonly being performed during software development as they help to identify potential bugs and errors. Most common examples are compilers and typecheckers for specific languages but work has also been done on tools that check the consistency between different software models, different representations within the same notation or fully integrated industrial solutions. This report extends this work in that it presents a relation between the model language BON and the concrete implementation language Java. The successful partial implementation shows that an automatic consistency checking tool is indeed feasible and meaningful even if the relation is not always perfect. Surprisingly, mappings between BON and pure Java constructs prove to be more complex and more involved than relations on the assertion languages. It may also seem to the casual reader that those relations have many deficiencies, but in fact the details they are concerned with mostly turn out to be exotic and rather rare special cases. The Beetlz tool has been designed to be tolerant in those instances so that it can be readily used in software development. This project and the experience gained from concluding it also show that BON and JML are straightforward enough to be quickly learned by anyone with average knowledge of Java. It has been suggested before to use BON for introducing more formal approaches into software engineering and in universities especially. By providing tool support that links BON to a very popular programming language, Beetlz is thus also suitable for promoting formal methods.

The basic relations between BON and Java are implemented and ready for use but further work remains to be done. Some concepts can only be mapped unsatisfactorily, however these relations can be corrected by extending BON further and thus customising it towards Java and other similar object oriented languages. Instances for such extensions include static access, more elaborate generics and an exact definition of client relations. Furthermore, BON dynamic charts, another possible description of a project, have been entirely disregarded in this analysis, but may prove useful when specifying a program's behaviour. Support for additional JML elements, like multiple specification cases, heavy-weight specifications or further operators will also become important if Beetlz is to be used in actual software development. Another area of improvement is the generation of skeleton code. The current functionality works fine when used by itself, however creation of ASTs would make it possible to pass on information to other tools and thus provide more comprehensive functionality. (Currently this not possible due to limitations on third party projects but is in development). On the theoretical side, formalising the relations between BON and Java, which at present only exist in structured English, would make a very interesting but also quite involved future project.

This project outlines how it is possible and advantageous to use a model of the software together with its implementation in a seamless manner. With added tool support, as the Beetlz tool demonstrates, updating of the model and/or the implementation is taken care of mostly automatically and thus can serve two purposes:

  1. Encourage the use of software models in software engineering.
  2. Reduce faults and misunderstandings resulting from poor communication with customers and/or team members.

Original Project Specification

  • Supervisor Dr. Joseph Kiniry
  • Subject Area Software Engineering
  • Pre-requisite Good competency in programming in Java
  • Co-requisite (things you must learn along the way) knowledge of software design, software modelling, software specification, BON notation, JML notation
  • Subject Coverage Software Design, Software Models, BON, JML
  • Project Type Design & Implementation
  • Hardware/Software: PC, laptop or workstation capable of running Java and Eclipse

Description

Business Object Notation (BON) has been developed for designing and analysing object-oriented programs. It is designed to enable a seamless and reversible development process as well as software contracting. It provides a textual, graphical and an informal representation of the system to be developed. Thus it can close the communication gap between technical and non-technical people (e.g. programmer and project manager) involved in the design and implementation of software.

The Java Modeling Language (JML) is a formal specification language for Java. It follows the Java syntax closely and its annotations are inserted directly into code. By doing so, it is easy for developers to learn and convenient to apply. It employs the design by contract approach by specifying preconditions, postconditions and invariants. With its extensive tool support it is greatly suitable for development of commercial software.

To make the most of a software model it has to be used throughout the development process, not just for the initial draft. For example, it can be used to update high-level manager on possible changes in the implementation without confusing them with technical details. This can only be achieved when the model is always up-to-date during whole of the development process. This project aims to provide such synchronisation by checking the consistency between a BON model and the corresponding Java source code with JML annotations.

Mandatory

  1. Familiarisation with software modeling and the BON method/language
  2. Familiarisation with design by contract and the Java Modeling Language (JML)
  3. Familiarisation with development of Eclipse plugins
  4. Create a mapping between BON features and JML features and identify possible issues where the two notations may not be (fully) compatible
  5. Implement an Eclipse plugin that reads in a BON file (format to be decided) and highlights differences in the corresponding Java/JML source code
  6. Design and implement a test program

Discretionary

  1. Design a GUI that is clearly arranged and flexible
  2. Include the option to generate Java skeleton code with JML annotations from BON model
  3. Make checks possible in both directions (BON -> Java and Java -> BON)
  4. Internationalize the plugin
  5. Make the plugin effective (e.g., it will only check lines of code that have changed since the last check)
  6. Allow for JML and BON to be extendable (e.g., custom tags, keywords)

Exceptional

  1. Write, submit, and publish a paper on the results.

Sources of information and preparatory reading

  1. Seamless Object-Oriented Software Architecture---Analysis and Design of Reliable Systems by Kim Walden and Jean-Marc Nerson. Available online.
  2. JML Homepage
  3. Developing Eclipse Plugins (IBM)
  4. Java tutorial on Internationalization