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.
The following tools have been developed in hiJaC:
The hiJaC Tools are openly available here.
The model translator produces Circus models from SCJ programs. To use the model translator on the cruise controller example, as reported in our paper submitted to The Computer Journal, please first use “ant” within the trunk folder to compile the source code and then execute the “run” script. The tools are currently only tested under Linux. Please see the README.txt file in trunk for further instructions.
If any problems with the tool please feel free to get in touch via email with Frank Zeyda.
The TransMSafe tool is used to check for possible memory-safety violations inside Level 1 SCJ programs. Given a valid SCJ program according to the SCJ specification, the tool uses static analysis to identify statements that may break the memory-safety rules of SCJ. More specifically, if a statement changes a reference to point to an object that may reside in a memory area lower in the memory hierarchy, an error is raised.
To achieve this, the tool keeps a record of the necessary aliasing and reference information in a bespoke environment. A worst-case model of the program is stored in the environment, which is maintained and analysed throughout the program analysis. A more in-depth description of the technique employed by the TransMSafe tool can be found in the publication SCJ: Memory-Safety Checking without Annotations.
The tool can be downloaded here. The tool is based on the infrastructure defined in the hiJaC tool suite, which offers other facilities for SCJ such as the Circus model generator for SCJ.
The source code for the TransMSafe tool can be found in the src\java\hijac\tools\scjmsafe directory. Instructions on how to build and run the tool with the provided examples can be found in the README file in the root directory.
TightRope is a tool for automatically modelling SCJ Level 2 programs by translating them into Circus. It is a substantial extension of the original Model Translator provided above, although it reuses the infrastructure and some functionality from the Model Translator.
The output from TightRope differs greatly from that of the Model Translator. This is because we address the features of Level 2 and extend the Model Translators coverage of Level 1 by capturing: period and deadline overruns, exceptions, and synchronisation. TightRope requires that the input program compiles and that each class is in a separate file.
The prototype version of TightRope (v0.65) is available here. The archive contains a readme with instructions on how to run TightRope on the two example applications included.
Automotive Cruise Control System in SCJ
Collision Detections in SCJ (Level 1)
SCJ Producer-Consumer Example Application: FlatBuffer - Circus Model and Program Description (Level 2)
SCJ Level 2 Examples and Translations. Extra Material for Safety-Critical Java Level 2 Programs: Application, Modelling, and Verification, Matt Luckcuck
Leader Election in SCJ for LEGO® MINDSTORMS®: report and presentation
Department of Computer Science
Deramore Lane, University of York, Heslington, York, YO10 5GH, UK
Tel: 01904 325500 | Fax: 01904 325599
