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

SHF：小型：协作研究：安全关键 Java 的规范和验证

• 批准号: 0916350
• 负责人: Gary Leavens
• 金额: $ 25万
• 依托单位: The University of Central Florida Board of Trustees
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2009
• 资助国家: 美国
• 起止时间: 2009-07-15 至 2015-09-30
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=0916350&HistoricalAwards=false
• 关键词: SHF; Small; Collaborative; Research; Specification

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.

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