Automated Formal Methods

9804736迫切需要有效的正式方法来编制正确的计算机程序。这一需求对于与许多安全关键或经济关键应用相关联的反应性系统来说变得至关重要，例如计算机网络通信协议或空中交通管制系统。一种有希望的方法是围绕时态逻辑的使用，时态逻辑是一种描述随时间变化的逻辑形式主义。对于大规模的反应性系统来说，纯粹的人工时间推理似乎是不可行的。这项研究的目标是使反应系统的验证尽可能自动化。自动验证比人工验证更可靠。它也更有可能具有工业用途，因为它可以提供完全自动化的按钮验证和调试工具。其基本思想是，与(命题)时态逻辑相关的某些问题是可判定的，在某些情况下是有效的。其中包括模型检查问题(程序的全局状态图是时态逻辑规范的模型吗？)本文研究了以下关键技术问题：(I)模型检测中状态爆炸问题的改进；(Ii)多个同构过程的推理；(Iii)模块化研究模型检查器的开发；(Vi)高效的程序综合。

9804736 There is a serious need for effective formal methods to construct correct computer programs. This need becomes crucial for reactive systems associated with many safety critical or economically vital applications, such as computer network communication protocols or air traffic control systems. One promising approach centers around the use of Temporal Logic, a logical formalism for describing change over time. Purely manual temporal reasoning seems infeasible for large-scale reactive systems. The goal of this research is to make verification of reactive systems as automated as possible. Automated verification is more reliable than manual verification. It is also more likely to be of industrial utility, as it is possible to offer fully automated push-button verification and debugging tools. The basic idea is that certain problems associated with (propositional) Temporal Logic are decidable, in some cases efficiently. These include the model checking problem (Is a program's global state graph a model of Temporal Logic specification ?). This research investigates, the following key technical issues: (i) Amelioration of the state explosion problem in model checking; (ii) Reasoning about many homogeneous processes; (iii) Development of a modular Research Model Checker; and (vi) Efficient program synthesis.***