Reactive Program Analysis From The Ground Up

全自动程序分析工具构成了软件工具的核心，用于确保当前和下一代硬件、软件和嵌入式系统满足其安全关键要求。然而，由于成本或时间要求，系统模型的巨大规模和复杂性往往使自动化分析变得不可行。本质上，系统规模的这种增长是考虑中的系统由许多相互关联的组件组成这一事实的副产品。即使单个组件具有可管理的大小，组合系统的大小也可能是巨大的。为了应对这种状态爆炸问题，重新审视分析中的基本要素是必要的。这包括用于构建新系统的组合模型；组件通过其共享信息的互连体系结构；用来代替正在验证的过大模型的抽象模型；用于将抽象模型与原始模型进行比较的等价性概念；以及用于描述预期系统行为的规范语言。有了新的要素，将设计全自动分析工具，这些工具要么能够分析以前无法进行全自动分析的系统，要么能够分析其分析成本过高的系统。特别是，进程之间的对称性和进程组成的新概念将用于分析通信协议的行为。因此，这项研究将是有价值的，因为它将使全自动安全保证工具能够应用于目前超出这些工具范围的关键系统，如通信协议或嵌入式控制器。这反过来将增加人们对这些系统运行的信心。

Fully automated program analysis tools form the core of software tools used to provide assurance that current and next-generation hardware, software, and embedded systems meet their safety-critical requirements. However, too often the sheer size and complexity of the system models makes automated analysis infeasible, either due to cost or time requirements. In essence, this growth in system size is a byproduct of the fact that the systems under consideration are comprised of many interconnected components. Even if the individual components are of manageable size, the size of the combined systems may be enormous. To cope with this state explosion problem, a reexamination of the basic elements in the analysis is in order. This includes the compositional models used to build new systems; the interconnection architectures by which the components share information; the abstraction models used in place of the too large models under verification; the notions of equivalence used to compare the abstract models to the originals; and the specification language used to describe expected system behaviour. With the new elements in hand, fully automated analysis tools will be designed that are either capable of analyzing systems that were previously not amenable to fully automated analysis, or for which the cost of analysis was prohibitive. In particular, new notions of symmetry amongst process and composition of processes will be used to analyze the behaviour of communication protocols. Therefore the research will be of value in that it will enable fully automated safety assurance tools to be applied to critical systems, such as communication protocols or embedded controllers, that are currently beyond the scope of these tools. This will in turn increase confidence in the operation of these systems.