第五章 软件工程中的形式化方法
从广义上讲，形式化方法（Formal Method）是指将离散数学的方法用于解决软件工程领域的问题，主要包括建立精确地数学模型以及对模型的分析活动。
狭义的讲，形式化方法是运用形式化语言，进行形式化的规格描述、模型推理和验证的方法。
将形式化方法运用于软件工程实践当中的主要目的是保证软件的正确性。
一.形式化方法基本概念
1.形式规约（Formal Specification）
2.形式证明与验证（Formal Verification and Validation）
3.程序求精（Program Refinement）
二.时态逻辑
模态（Modal）逻辑是经典命题逻辑和一阶谓词逻辑的扩展形式。模态逻辑通过引入”可能“和”必然“两个模态词，从而对可能世界中的命题进行描述和演算。
1.一阶线性时态逻辑
一阶线性时态逻辑（FOLTL）是一阶谓词逻辑的扩展。
2.计算树逻辑
计算树逻辑（CTL）是一种离散、分支时间、命题时态逻辑。
一般将CTL和CTL*统称为计算树逻辑。
三.模型检测
软件的计算树逻辑规格可以通过模型检验得到验证。模型检验就是在软件系统的Kripke结构模型下，对以CTL*公式给出的软件性质的正确性验证。
四.Z语言
Z语言是由牛津大学程序设计研究小组开发的一种形式语言，之后该小组与IBM的Hursley实验室合作，将Z语言用于IBM客户信息控制系统（Customer Information and Control System,CICS）的开发，使得最终的产品质量得到了全面提高，所监测出的错误数量大大减少，并且整体开发费用降低了9%。
Z语言的数学基础是集合论和一阶谓词演算。
五.Petri 网
1962年，联邦德国的Carl Adam Petri在他的博士论文”Kommunikation mit Automaten“《用自动机通信》中首次使用网状结构模拟通信系统。这种系统模型后来以Petri网为名流传。现在，Petri网一词既指这种模型，又指以这种模型为基础发展起来的理论。