Reactive Program Analysis From The Ground Up

从头开始的反应式程序分析

• 批准号: 262076-2012
• 负责人: Trefler, Richard
• 金额: $ 1.24万
• 依托单位: University of Waterloo
• 依托单位国家: 加拿大
• 项目类别: Discovery Grants Program - Individual
• 财政年份: 2018
• 资助国家: 加拿大
• 起止时间: 2018-01-01 至 2019-12-31
• 项目状态: 已结题
• 来源: https://www.nserc-crsng.gc.ca/ase-oro/Details-Detailles_eng.asp?id=667046
• 关键词: Reactive; Program; Analysis; 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.********

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