Software is increasingly important in aircraft, spacecraft, cars, and medical devices, which are all safety-critical. As the size and complexity of the software increases, so does the likelihood for defects with potentially catastrophic consequences. This research aims to simultaneously increase the level of assurance and raise the level of abstraction in safety critical systems, by supporting Safety Critical Java that uses C for driver code (SCJ+C). The project will implement and evaluate SCJ+C and provide modular specification techniques and verification tools for it. Few such tools exist for object-oriented real-time programs, and thus there has been little critical evaluation of techniques and tools for real-time safety-critical programming. Modular reasoning about timing constraints is a known hard problem, due to the dependence of a method's timing on all methods it calls.
The project will leverage the Java Modeling Language (JML) as a specification tool to build a set of practical JML-based tools for the timing analysis of SCJ+C programs. The research will allow the application of formal methods for certification, correctness, bug-finding, and timing properties for real-time critical systems. This will help productivity, by allowing programmers to develop and reason about their systems at an appropriate level of abstraction.
