本章主要介绍了形式化方法的基本概念包括形式规约（即软件规格说明，是软件系对象作用的方法，自己对象行为的描述）形式证明与验证（技术包括：检测，定理定理证明），程序求精，逻辑时态的一阶线性时态逻辑、计算树逻辑。模型检测临就是在Kripk模型下，对以CTL*公式给出的软件性质得正确性验证、计算树逻辑。模型检测Z语言的概述Z语言的表示（集合关系以及函数、队列和包、自由类型和模式）、Z语言实例（停车场管理系统、图书管理系统的实例），petri网的基本定义petri规格实例～信号灯
原文：http://www.cnblogs.com/xizhenghe/p/4308255.html