形式化方法导论

鉴于形式化方法对软件工程的重要性， 2004 年 ACM 和 IEEE-CS 联合制订的软件工程教程《SE2004》将“形式化方法”列为 软件工程专业的核心课程。本书主要由系统建模、形式规约和形式验证三部分构成，具体包括：顺序、并发和反应系统、转换系统、自动机、时序逻辑、演绎证明、模型检测、实时系统、混成系统等。