CAREER: Computer-Aided Verification of Reactive Systems

职业：反应系统的计算机辅助验证

• 批准号: 9734115
• 负责人: Rajeev Alur
• 金额: $ 20万
• 依托单位: University of Pennsylvania
• 依托单位国家: 美国
• 项目类别: Continuing Grant
• 财政年份: 1998
• 资助国家: 美国
• 起止时间: 1998-07-01 至 2003-06-30
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=9734115&HistoricalAwards=false
• 关键词: CAREER; Computer; Aided; Verification; Reactive

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.***

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