形式证明与验证(Formal Verification&Validation) ,定理证明：可以处理无限状态空间问题 -演绎验证(deductive verification) ·采用逻辑公式表示系统规约及其性质 -工具（定理证明器，Theorem Prover) ·用户引导自动推演工具：ACL2、LP、Eves ·证明检验器：HOL、LCF、LEGO ·符合证明器：PVS ·基于分离逻辑+交互式证明：Coq 模型检验model--checking:适用于有穷状态系统 -完全自动化，验证速度快 ·检验性质不满足时，给出反例。 ·状态空间爆炸 一工具 ·时态逻辑模型检验工具：SMV/NuSMV、SPIN、UPPAAL ·行为一致性检验工具：FDR、Cospan/Formal Checker ·复合检验工具：HSIS、METAFrame 8/112形式证明与验证(Formal Verification & Validation) • 定理证明：可以处理无限状态空间问题 – 演绎验证（deductive verification） • 采用逻辑公式表示系统规约及其性质 – 工具（定理证明器，Theorem Prover） • 用户引导自动推演工具：ACL2、LP、Eves • 证明检验器：HOL、LCF、LEGO • 符合证明器：PVS 8/112 • 符合证明器：PVS • 基于分离逻辑+交互式证明：Coq • 模型检验model-checking：适用于有穷状态系统 – 完全自动化，验证速度快 • 检验性质不满足时，给出反例。 • 状态空间爆炸 – 工具 • 时态逻辑模型检验工具：SMV/NuSMV、SPIN 、UPPAAL • 行为一致性检验工具：FDR、Cospan/Formal Checker • 复合检验工具：HSIS、METAFrame