HIJAC: High-Integrity Java applications using circus

The use of computers and computer programs is pervasive nowadays, but every computer user knows that programs go wrong. While it is just annoying when our favourite text editor loses a bit of our work, the consequences are potentially much more serious when a computer program that, for instance, controls parts of an airplane goes wrong. Software validation and verification are central to the development of this sort of application. In fact, the software industry in general spends a very large amount of money in these activities.

One of the measures taken to promote correctness of programs is the use of a restricted set of features available in programming languages. This usually means that most of the more recent advances in software engineering are left out. In this project, we propose to provide development, validation, and verification facilities that allow object-orientation and a modern real-time computational model to be used for the programming of safety-critical systems. In particular, we will work with one of the most popular programming languages: Java, or more specifically, its profiles for high-integrity engineering proposed by the Open Group.

As our main case study, we will verify parts of the controller of the first Java Powered Industrial Robot, developed by Sun. One of our collaborators, a senior engineer in Sun tells in an interview that "Distributed Real-Time Systems are really hard to build and the engineering community doesn't really know how to build them in a coherent repeatable way."(java.dzone.com/articles) Real-Time Java is entering the industrial automation and automotive markets. Lawyers did not allow the Java Robot to get anywhere near a human, even in a JavaOne conference demo. To proceed in that kind market, better support is needed.

Programming is just one aspect of the development of a modern system; typically, a large number of extra artefacts are produced to guide and justify its design. Just like several models of a large building are produced before bricks and mortar are put together, several specification and design models of a program are developed and used before programs are written. These models assist in the validation and verification of the program. To take our civil engineering metaphor one step further, we observe that, just like there can be various models of a building that reflect several points of view, like electricity cabling, plumbing, and floor plans, for example, we also have several models of a system. Different modelling and design notations concentrate on different aspects of the program: data models, concurrent and reactive behaviour, timing, and so on. No single notation or technique covers all the aspects of the problem, and a combination of them needs to be employed in the development of large complex systems.

In this project, we propose to investigate a novel integrated approach to validation and verification. Our aim is to provide a sound and practical technique that covers data modelling, concurrency, distribution, and timing. For that, we plan to investigate the extension and combined use of validation and verification techniques that have been successfully applied in industry. We do not seek an ad hoc combination of notations and tools, but a justified approach that provides a reliable foundation for the use of practical techniques.

We will have succeeded if we verify a substantial part of the robot controller: using a model written in our notation, we will apply our techniques to verify parts of the existing implementation, execute it using our verified implementation of Safety-critical Java. Measure of success will be provided by our industrial partners and the influence of our results in their practice or business plans.