Model-Based Monitoring of Air-Traffic Control Software

基于模型的空中交通管制软件监控

• 批准号: 0341620
• 负责人: Martin Rinard
• 金额: $ 40万
• 依托单位: Massachusetts Institute of Technology
• 依托单位国家: 美国
• 项目类别: Continuing Grant
• 财政年份: 2003
• 资助国家: 美国
• 起止时间: 2003-09-15 至 2007-08-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=0341620&HistoricalAwards=false
• 关键词: Model; Based; Monitoring; Air; Traffic

0341620Model-Based Monitoring of Air-Traffic Control SoftwareMartin RinardThe research focuses on developing a new, model-based monitoringtechnique that will dynamically examine the data structures andvariable values in the executing computation to find and flag anyinconsistencies. During development, this technique will flaginconsistencies as soon as they arise, helping the developer tolocalize the error by eliminating the continued execution (and theassociated inconsistency propagation) that obscures the source of theerror. After deployment, the technique will alert users toinconsistencies as soon as they arise, eliminating the problem ofincorrect actions taken because of reliance on incorrect output from aprogram operating with inconsistent values or data structures. Keyresearch issues include the design and efficient implementation of thespecification and model construction languages and the evaluation ofhow well this approach works for two purposes: 1) in the context of anexisting system, to check key data structure consistency properties,to promote design extraction, and to ensure that the design remains upto date as the software is maintained, and 2) in the context of newdevelopment, to promote design development, support errorlocalization, and facilitate debugging. The potential benefits ofthis research include reduced software development effort, more reliablesoftware, and safer software. The research will be performed usingthe CTAS software system in the NASA testbed and the TSAFE softwaresystem currently under design at NASA.

0341620 基于模型的空中交通管制软件监控Martin Rinard 该研究的重点是开发一种新的基于模型的监控技术，该技术将动态检查执行计算中的数据结构和变量值，以发现并标记任何不一致之处。在开发过程中，这种技术会在不一致出现时立即对其进行标记，从而通过消除掩盖错误来源的持续执行（以及相关的不一致传播）来帮助开发人员定位错误。部署后，该技术将在出现不一致时立即向用户发出警报，从而消除由于依赖使用不一致的值或数据结构运行的程序的错误输出而采取错误操作的问题。主要研究问题包括规范和模型构建语言的设计和有效实现，以及评估该方法的工作效果，以达到两个目的：1）在现有系统的背景下，检查关键数据结构的一致性属性，促进设计提取，并确保设计在软件维护时保持最新状态；2）在新开发的背景下，促进设计开发，支持错误定位并促进调试。 这项研究的潜在好处包括减少软件开发工作、更可靠的软件和更安全的软件。该研究将使用 NASA 测试台中的 CTAS 软件系统和 NASA 目前正在设计的 TSAFE 软件系统进行。