Local Symmetry: Compositional Reasoning For Modular Designs

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

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

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