University | Computer Science  

    Circus Family hiJaC  

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:


Project Partners:

  • AWE Plc
  • Praxis Systems Ltd
  • Sun Microsystems Ltd




       Department of Computer Science

       University of York, Deramore Lane, York, YO10 3TA, UK

       Tel: 01904 325500 | Fax:01904 325599                                                                                                 Last updated on 17 November 2014