Local Symmetry: Compositional Reasoning For Modular Designs

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

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.