Model-Based Monitoring of Air-Traffic Control Software

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

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.