Refinement-centric Reliable Software Development:
The EBON (Extended Business Object Notation) Tool Suite

Funded by the IRCSET Embark Initiative

IRCSET Fellow: Fintan Fairmichael

Popular high-level "modeling" languages in current use (e.g., UML) are not amenable to formal analysis because of a lack of semantics and interoperable tool support. Even so, high-level representations are compelling and useful in modern software engineering practise and software engineers regularly struggle with using these inadequate languages, even for mission critical applications.

BON is a high-level specification language for describing structured systems, including programs, web sites, databases, etc. BON, unlike some of its more popular counterparts like UML, has a semantics, is very easy to learn and write, has a graphical and textual notation, and can be used for many different domains.

A BON lexer, parser, and typechecker are now available as a part of the BONc Tool Suite, available via KindSoftware. EBON stands for "Extended BON". It is a richer specification language that adds a number of new constructs called "semantic properties".

These properties are domain-specific and have rich but intuitive semantics that are directly expressed in software engineering artifacts and processes. Examples of domains currently covered with semantic properties include concurrency, ownership, responsibility, bug tracking, literate programming, and version control.

The goal of this project is to take the next steps in the development of EBON, namely a formal specification of its semantics within a logical framework and the evolution of an EBON software architecture.

The semantics will be written in kind theory, a higher-order logic developed previously for reasoning about reusable assets. A formal bi-refinement must also be defined between EBON and JML.

The software architecture includes the development of EBON parser, typechecker, visualizer, and documentation generator. The aforementioned refinement relation will facilitate code generation from specifications and ensuring that high-level specifications remain uniformly consistent with respect to a given implementation, particularly with respect to rich semantic properties. The target language, as previously mentioned, is JML-annotated Java. This architecture will be integrated into the JML toolsuite and the MOBIUS PVE.