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.