CAREER: Computer-Aided Verification of Reactive Systems

9734115模型检测正在成为复杂反应系统自动调试的实用工具。在模型检查中，将系统的高级描述与逻辑正确性要求进行比较，以发现不一致。这项职业研究旨在通过追求研究和教育的三个目标来提高这一范式的适用性和效率。首先，为了使非专业人员更容易获得计算机辅助验证的结果，开发了一种称为“反应模块”的建模方法，作为一个统一的框架。此外，还将创建支持多种技术组合的分析工具、关于计算机辅助核查的标准教科书和关于计算机辅助核查的高级课程。其次，为了开发能够分析现有工具所达不到的系统的技术，研究了两个新的主题：开放系统和异质系统。开放系统是一个与未知环境相互作用的反应性系统，为了分析这类系统，我们研究了诸如交替时序逻辑等新的规范范型。为了分析由具有不同同步假设且用不同源语言描述的组件组成的系统，研究了反应式模块作为公共语义框架的效用。最后，为了将形式方法中的概念整合到宾夕法尼亚大学的本科教育中，建议对现有的理论和系统课程进行改革。

9734115 Model checking is emerging as a practical tool for automated debugging of complex reactive systems. In model checking, a high- level description of a system is compared against a logical correctness requirement to discover inconsistencies. This CAREER research aims to enhance applicability and efficiency of this paradigm by pursuing three objectives in research and education. First, to make results in computer-aided verification more accessible to nonspecialists, a modeling method called "reactive modules" is developed as a unified framework. In addition, an analysis tool that supports a combination of techniques, a standard textbook on computer-aided verification, and an advanced course on computer-aided verification will all be created. Second, to develop techniques that can analyze systems beyond the reach of existing tools, two new topics, open systems and heterogeneous systems, are investigated. An open system is a reactive system interacting with an unspecified environment, and for analysis of such systems, novel specification paradigms such as alternating-time temporal logics are studied. For analysis of systems consisting of components with different synchrony assumptions and described in different source languages, the utility of reactive modules as a common semantic framework is investigated. Finally, to integrate concepts in formal methods into undergraduate education at Penn, changes to existing courses in theory and systems are proposed.***