ITR: Design Conformant Software

拟议的研究将调查用于基础设施软件的新软件工程技术和工具，以提高其可靠性、安全性和可预测性。关键思想是使用抽象的设计模型来驱动新的静态分析，以检查软件是否正确地实现了其设计（如果没有，则确定问题的来源）。为了确保我们的研究解决了开发人员在该领域面临的重要问题，我们将在空中交通管制系统组件开发的背景下进行研究。具体来说，研究将调查使用对象模型来表达重要的设计属性和新的指针分析算法，以验证代码正确地实现了对象模型。对象模型描述堆中的基本对象以及它们之间的关系；指针分析自动分析代码以提取有关对象如何相互引用的信息。本研究将探讨通过使用对象模型将分析集中在感兴趣的属性上来提高指针分析精度的技术。

The proposed research will investigate new software engineeringtechniques and tools for infrastructural software that will improveits reliability, safety, and predictability. The key idea is to useabstract design models to drive new static analyses that check thatthe software correctly implements its design (and if not, identify thesource of the problem). To ensure that our research addresses theimportant issues that developers face in the field, we will conductour research in the context of the development of an air trafficcontrol system component. Specifically, the research will investigatethe use of object models to express important design properties andnew pointer analysis algorithms to verify that the code correctlyimplements the object models. Object models describe essential objectin the heap and the relationships between them; pointer analysisautomatically analyzes code to extract information about how objectsrefer to each other. The research will investigate techniques thatimprove the precision of the pointer analysis by using the objectmodel to focus the analysis on the properties of interest.