SHF: Small: Collaborative Research: Specification and Verification of Safety Critical Java

软件在飞机、宇宙飞船、汽车和医疗设备中越来越重要，这些都是安全关键。随着软件的大小和复杂性的增加，产生具有潜在灾难性后果的缺陷的可能性也在增加。本研究旨在通过支持使用C作为驱动程序代码的安全关键Java(SCJ+C)，来同时提高安全关键系统的保证级别和抽象级别。该项目将实施和评估SCJ+C，并为其提供模块化规范技术和验证工具。面向对象的实时编程工具很少，因此几乎没有对实时安全关键编程的技术和工具进行批判性评估。由于方法的时序依赖于它调用的所有方法，有关时序约束的模块化推理是一个已知的难题。该项目将利用Java建模语言(JML)作为规范工具来构建一组实用的基于JML的工具，用于SCJ+C程序的时序分析。这项研究将允许对实时关键系统的认证、正确性、错误查找和计时属性应用正式方法。通过允许程序员在适当的抽象级别上开发和推理他们的系统，这将有助于提高生产率。

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.