Local Symmetry: Compositional Reasoning For Modular Designs

局部对称：模块化设计的组合推理

• 批准号: RGPIN-2019-04234
• 负责人: Trefler, Richard
• 金额: $ 1.68万
• 依托单位: University of Waterloo
• 依托单位国家: 加拿大
• 项目类别: Discovery Grants Program - Individual
• 财政年份: 2019
• 资助国家: 加拿大
• 起止时间: 2019-01-01 至 2020-12-31
• 项目状态: 已结题
• 来源: https://www.nserc-crsng.gc.ca/ase-oro/Details-Detailles_eng.asp?id=679310
• 关键词: Local; Symmetry; Compositional; Reasoning; Modular

Our world is increasingly dependent on interconnected, complex and dynamic software systems. Each system may well be too complex to debug by hand and this only gets worse in the context of dynamically changing and interconnected systems. How can we be sure that systems perform as intended in all circumstances, even unforeseen ones? ******My research program focuses on model checking, bringing together foundational concepts in formal logic with new methods for describing communicating systems containing many symmetric or similar components, and mathematically rigorous techniques for analyzing complex systems. Model checkers are automated analysis engines that take as input a program description of a hardware or software system, and a specification of correct behavior, and then check whether all the behaviors of the program satisfy the given specification. Moreover, they provide a crucial theoretical framework for understanding the logical structures underpinning computational systems, and are thus of great scientific interest. ******Distributed computer protocols consisting of many interacting components, are often safety or system critical. That is, their correct operation in any setting with any data input is a basic system requirement. Any single point of failure may bring the entire system down. However, building systems to such a high level of correct behavior is often challenging. My goal is to build automated reasoning engines that take advantage of the per component symmetries in the program descriptions of systems with many similar components. The intent is that, for systems with many symmetric components, only one of the many components need be analyzed while drawing conclusions about the behavior of all related components. Building upon 'local symmetry,' a novel conceptual framework I recently introduced, I seek to exploit local symmetries among components to build analysis engines capable of effectively and efficiently checking that large scale system descriptions do in fact satisfy their basic system safety requirements. Graduate students trained in the course of this research will acquire unique and extremely valuable skills in modeling and analyzing safety and system critical multi-component systems. They can apply these skills in industry, research and academia to answer current and future questions about the systems we depend on. ********

我们的世界越来越依赖于相互关联、复杂和动态的软件系统。每个系统都可能太复杂而无法手工调试，并且在动态变化和互连系统的上下文中，情况只会变得更糟。我们如何确保系统在所有情况下，甚至是不可预见的情况下都能按预期运行？** 我的研究计划侧重于模型检查，将形式逻辑中的基本概念与描述包含许多对称或类似组件的通信系统的新方法结合在一起，以及分析复杂系统的数学严格技术。模型检查器是自动分析引擎，其将硬件或软件系统的程序描述以及正确行为的规范作为输入，然后检查程序的所有行为是否满足给定规范。此外，它们为理解计算系统基础的逻辑结构提供了重要的理论框架，因此具有巨大的科学兴趣。** 分布式计算机协议由许多交互组件组成，通常是安全或系统关键的。也就是说，它们在任何设置中的任何数据输入的正确操作是基本的系统要求。任何一点故障都可能导致整个系统崩溃。然而，将系统构建到如此高水平的正确行为通常具有挑战性。我的目标是建立自动推理引擎，利用每个组件的对称性，在程序描述的系统与许多类似的组件。这样做的目的是，对于具有许多对称组件的系统，只需分析许多组件中的一个，同时得出有关所有相关组件行为的结论。基于“局部对称性”，我最近介绍了一种新的概念框架，我试图利用组件之间的局部对称性来构建能够有效和高效地检查大规模系统描述实际上满足其基本系统安全要求的分析引擎。在本研究过程中培训的研究生将获得建模和分析安全和系统关键多组件系统的独特和非常有价值的技能。他们可以将这些技能应用于工业，研究和学术界，以回答有关我们所依赖的系统的当前和未来问题。