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

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

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.