Modern society is almost totally reliant on software-based infrastructure. This demands modelling and programming languages and techniques that facilitate and ensure quality. Two language (subsets) have dominated high-integrity real-time engineering. Ada provides good support through its Spark and Ravenscar subsets, and the Spark Examiner Toolset, but does not have a large sustained community. Safe(r) subsets of C/C++ are often the choice, but lack support for
formal development. In both cases, various modern programming features found useful in other sectors of the software industry are often left out the grounds of safety.
What we propose is to support an international effort to produce a high-integrity real-time version of perhaps one of the most popular programming languages ever:~Java. Safety-critical Java achieves a compromise between the safety of Ada and the popularity of C/C++, and provides an ambitious novel intake in the combined safe use of object orientation and real-time programming. It lacks, however, both a formal underpinning for its programming models and a rigorous
development framework for applications. We will address both these concerns.
We propose the development of a sound framework for specification, analysis, design, and programming of verified real-time systems. We will explore the use of languages and theories based on Circus, a language for refinement that builds on the industrial success of Z and CSP. (Ford, General Dynamics, and QinetiQ provide a few examples of their acceptance.) Circus has been applied in the verification of control systems in an industrial collaboration supported by EPSRC.
Its semantics is based on the Unifying Theories of Programming (UTP).
Our challenges are imposed by the complexity of Safety-critical Java. It is object-oriented, and involves constructs for concurrency and real-time, and a novel approach to memory management. There are various techniques to handle each of these aspects of a system, but sound and comprehensive approaches are still to be established. The UTP, a framework for refinement that allows study and combination of various programming paradigms, makes Circus well suited for this
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.
In summary, we need to verify safety-critical programs according to various standards, and current languages are not (or no longer) satisfactory. Safety-critical Java offers an exciting alternative, and we have the seed for a rich collection of applicable languages and theories based on Circus and the UTP. We propose to extend and exploit them in context of Java to provide a workable solution for the next generation of safety-critical programs.
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.
This is an ongoing project, so this is a report of partial results.
We have defined a process-algebraic semantics for SCJ programs (Level 1). Based on that semantics, we have defined a programming theory and technique for formal development of such programs. This comes in the form of a refinement strategy and technique. As a case study, we have tackled a concurrent version of a benchmark example adopted by the SCJ community.
On the theory front, we have been developing the semantic models that justify the use of the process algebra that we adopt in our work, namely, object-oriented timed extensions of Circus. We have formalised higher-order constructs in a setting that allow integration of all these paradigms. Based on that, we are tackling object orientation. We have also considered issues related to the time model.
Currently, we are addressing verification of memory safety of SCJ Level 1 programs, and a semantics for SCJ Level 2 programs.
|Effective start/end date||22/06/10 → 30/10/15|