形式模型

形式模型（formal model），理学-计算机科学技术-计算机软件-软件基础理论-形式模型，用于描述计算的数学模型。形式模型用于对计算机系统进行形式建模，是对计算机系统的行为进行形式验证的基础。形式模型的研究贯穿计算机科学的发展历程。计算机科学起源于对通用计算进行建模的形式模型（即图灵机）的提出。图灵机已被证明同λ演算、一般递归函数是等价的，它给了直观计算概念一个严格的数学定义。形式模型包括自动机模型、重写系统、进程代数等。在自动机形式模型中除了图灵机之外，还包括下推自动机、有限自动机等。人们对形式模型的理论性质进行了深入研究，包括表达能力和算法性质（可判定性、复杂性、判定算法等）。比如，下推自动机和有限自动机的表达能力比图灵机要弱，但是具有更好的算法性质，其状态可达性问题是可判定的。形式模型的一个主要用途是支持对计算机系统行为的形式建模和验证。研究人员已经基于形式模型开发了各种分析验证工具。例如：基于有限自动机的模型检测工具Spin和SMV及其变种已经广泛应用于计算机硬件和协议的验证；基于重写系统的Maude系统已经广泛应用于密码协议和网络协议的验证。