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.
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.
Our emphasis on time and space resources requires that we deal with processes and objects. (1) For design and specification we use the Circus family so that we build on notations that have already been successful in industrial settings. (2) We select refinement-based algebraic proof strategies and model checking for analysis and verification. (3) For programming we select the Open Group's Safety critical Java Level 1.
Team Members:
- Ana Cavalcanti (PI)
- Andy Wellings
- Jim Woodcock
- Frank Zeyda
- Kun Wei
- Neeraj Singh
- Chris Marriott
- Alvaro Miyazawa
- Pedro Ribeiro
- James Baxter
Project Partners:
- AWE Plc
- Praxis Systems Ltd
- Sun Microsystems Ltd
Funding: