软件工程——理论、方法与实践 之 软件工程中的形式化方法

从广义上讲，形式化方法是指将离散数学的方法用于解决软件工程领域的问题，主要包括建立精确的数学模型以及对模型的分析活动。狭义的讲，形式化方法是运用形式化语言，进行形式化的规格描述、模型推理和验证的方法。形式化方法运用于软件工程实践当中主要目的是保证软件的正确性。软件开发实际上就是把现实世界的需求映射成软件额模型化过程。该过程包括:形式规约、形式证明我与检验、程序求精三方面的活动。

形式化规格说明是对软件系统对象，对象的操作方法，以及对象行为的描述。当规格说明用非形式化方法描述时，可称为“规格说明”，当规格说明用形式化方法描述时，可称为“形式规约”。形式检测与证明技术主要包括模型检测与定理证明。模型检测是一种基于有限状态模型并检测该模型的性质的技术。定理证明采用逻辑公式来表示系统规约及其性质，其中的逻辑由一个具有公理和推理的形式化系统给出，进行定理证明的过程就是应用这些公理或推测规则来证明系统具有某些性质。程序求精是将自动推理和形式化方法相结合，从抽象形式规约推演出具体的面相计算机的程序代码的全过程。目前应用比较广泛的3种形式化方法包括:基于时态逻辑的方法、Z语言及其分析方法、Petri网方法。

模态逻辑是经典命题逻辑和一阶谓词的扩展形式。模态逻辑通过引入“可能”和“必然”两个模态词，从而对可能世界中的命题进行描述和演算。Z语言为系统建立基于状态的模型。模型的三个主要组成部分是输入、输出和状态，它们均有相应的数学概念来描述。Z语言形式规约由数学语言描述和自然语言注释两部分组成。其中数学语言描述部分是核心，它是精确、简练地描述系统性质和自动推理的保证。自然注释部分则用于解释说明数学部分的内容。Petri网一词既指这种模型，又指以这种模型为基础发展起来的理论。有时又把Petri网称作网论。Petri网分为位置/迁移Petri网和高级Petri网两类。