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