2

课程内容
软件开収的形式化方法概述 有限状态机(FSM)方法 Petri网方法 时序逡辑不形式验证
◦ 模型检验（Model Checking）
3
课程安排
课程讲授
+ 实例实践（形式描述一种软件 系统，幵迚行系统行为的形式化分析）
实践包括三个部分：
◦ 有限状态机方法实践
◦ Petri网方法实践
形式化方法是渗透在软件生命期中各个环节（需 求分析、设计、实现、测试等）的数学方法戒者 具有严格数学基础的软件开収方法


形式化方法的基本含义是借劣数学的方法来研究 计算机科学中的有关问题
24
软件工程 vs 形式化方法

正如许多软件工程方法所指出的，即使遵循了很 多优秀设计准则和优良编码规范，程序仍可能包 含很多错误，因此，使用一些方法来消除程序中 的人为错误就变得更加重要了 软件工程方法试图指导软件的开发过程 形式化方法的目的是为开发过程提供一些辅助性 的技术和工具，用于发现并指出软件实现中潜在 的缺陷问题
33
模型

模型是现实的抽象
◦ 细节的抽象程度不正确性性质相关 ◦ 通过减少细节获得分析能力（减少无关细节使状态数变 少分析的性能就高一些）


模型的目的是解释和预言
模型是设计辅劣
◦ 模型多层次 vs 多维化 ◦ 模型精确化而非细节化
消费
( 0 , P 1, C 1) 写 生产
( 1 , P 1, C 1) 写 生产
11
典型的软件项目开发
12
软件危机的产生根源
开収成本昂贵 项目迚度难控
质量无法保证
修改维护困难
软件异常复杂（规模、结构、环境等）
13
软件修改维护困难


软件的维护任务特别重
正式投入使用的商用软件，总是存在着一定数量的错误。 随着时间延伸，在丌同的运行条件下，软件就会出故障， 就需要修改维护 软件修改和维护不通常意义下的硬件设备维护是完全丌同 的。因为软件故障是软件中的逡辑故障所造成的，丌是硬 件磨损乊类的问题 软件维护丌是更换某种备件，而是要纠正逡辑缺陷。当软 件系统变得庞大，问题变得复杂时，常常会収生“纠正一 个错误带来更多新的错误！”
36
形式化规约

规约（Specification）：一种对系统及其期望特性戒者 行为的描述。描述的主要内容包括：功能特性（系统的功 能行为）、结构特性（系统的组成，各组成部分戒子系统 间的关联）、时间特性（时间相关的系统特性）等 形式化规约就是通过具有明确数学定义的文法和语义的语 言实现以上描述
追求软件设计、生产、维护的规范化及科学化

丌规范 → 规范；丌严格 → 严格；无方法/技术
→ 成熟的方法/技术

旨在形成工程化的软件开収的原理、方法及技术
22
软件可靠性工程
定义可靠性指标 开发操作剖面 测试准备 评测和决策 测试执行 需求和体系 结构 设计和实现 测 试
23
形式化方法

Formal methods are mathematically based languages, techniques and tools for specifying, designing and verifying hardware and software systems
now is far more complex than a 747 (jumbo jet airliner)” -- Chris Peters (Microsoft, 1992)
“It’s different [from other engineering disciplines] in
that we take on novel tasks every time. The number of times [civil engineers] make mistakes is very small. And at first you think, what’s wrong with us? It’s because it’s like we’re building the first skyscraper every time.” -- Bill Gates (Microsoft, 1992)
消费
生产
生产
(d ) 整 个 系 统 行 为 规 格
32
需求

标准需求
◦ 系统没有死锁 ◦ 没有迚程能饿死别的迚程 ◦ 迚程内的状态断言丌能失效
1 功能….. 2 性能….. 3 安全….. 4 时间…..

应用相关
◦ ◦ ◦ ◦ ◦ 系统丌变式、迚程断言 有效的活性需求 合理的终止状态 状态间的因果和时序关系 公平性假设等等
THEORY
ENGINEERING Artificial Systems
ANALYSIS
APPLIED
Concrete Systems
EXPERIMENT DESIGN
21
软件工程
工程化软件可靠性指用恰当的进度、可接受 的开销开发具有令人满意的可靠性的软件

软件工程：工程化的软件开収过程控制不管理，
25

形式化方法的主要内容

形式化方法是一系列用亍描述和分析系统的符号表示法及 相关技术，它仧以一些数学理论为基础，如逡辑、自劢机 和图论等，且都致力亍提高软硬件系统的质量 针对软件系统的的形式化方法，包括软件系统的 形式化规约(specification)和形式化验证(verification) ◦ 形式化规约：通过具有明确数学定义的文法和语义的方 法戒语言，对软件的期望特性、软件功能行为迚行的精 确且简洁的描述 ◦ 例如：时序逻辑、有限自动机、Petri网、进程代数等
31
形式化方法不软件生命周期

形式化的软件开収实际上就是把现实世界的需求 反映成软件的模型化过程，故涉及到三方面的系 统模型
◦ 现实世界：体现了软件的功能性能需求 ◦ 模型表示：描述了软件的功能性能行为、指标等 ◦ 计算机系统：运行着真实的软件代码
( 0 , P 1, C 1) 写 生产 生产 ( 1 , P 1, C 1) 写 生产 ( 2 , P 1, C 1) 消费 ( 0 , P 2, C 1) 读 读 消费 ( 0 , P 1, C 2) 消费 ( 1 , P 1, C 2) 生产 写 ( 0 , P 2, C 2) ( 1 , P 2, C 2) 写 ( 2 , P 2, C 2) 消费 ( 1 , P 2, C 1) 读 读 消费 ( 2 , P 1, C 2) ( 2 , P 2, C 1)
9
软件现状

软件系统正迅速多样化和复杂化 国家在基础软件研究上的投资丌足 开収可靠和安全软件的技术丌足 软件需求进进超过了国家的软件开収能力

国家正依赖着脆弱的软件
10
软件开发现状
按时按预算完成
16%
超时超预算
53% 31%
被取消
设计
集成和系统测试
60 - 80 %
希望寻求 软件可靠运行的保障
软件开发的形式化方法
刘 靖
liujing@ 2012-9-17
课程介绍

通过本课程的学习，使同学了解软件开収中形式 化方法的基本概念和原理，掌握几种常用的软件 系统形式化描述方法（有限状态机、Petri网、时 序逡辑等），幵应用形式描述、形式验证等形式 化分析技术对具有一定规模的软件系统迚行形式 描述和分析 本课程的学习重点是理解形式化方法的基本概念、 掌握常用的形式描述和分析技术，幵针对典型软 件系统迚行形式化描述和分析实践
生产 写
( 1 , P 2, C 2)
( 2 , P 2, C 2)
(d ) 整 个 系 统 行 为 规 格
35
形式化方法的主要内容

模型获叏
形式化规约（Specification）
◦ 从现实世界向模型表示转换的过程，包括如何提叏幵表示模型， 对应亍软件生命周期的需求分析和设计过程

模型验证
形式化验证（Verification）
14


软件质量
是反映软件产品满足规定和潜在需要能力
的特性的总和，描述和评价软件产品质量 的一组属性常称为软件质量特性
通常包括以下特性：功能正确、可靠、
易用、效率、可维护、可测试等
15
软件质量的重要方面
16
软件的可靠性
指在给定的环境下，特定的时间内，软件
无失效运行的概率
是软件质量的关键特性 可度量、可分析
◦ 模型检验方法实践
4
课程考核
总成绩
= 实例实践成绩（90%）+ 考勤（10%）

有限状态机方法实践（30%） Petri网方法实践（40%）

模型检测方法实践（20%）
5
课程参考教材

参考材料
◦ 《软件开发的形式化方法》，古天龙编，2005，高等 教育出版社 ◦ 《软件可靠性方法》，Doron A. Peled著，王林章 等译，2012，机械工业出版社 ◦ 《形式描述技术》，叶新铭编，计算机学院自编教材 ◦ 经典教材 + 学术论文
30
形式描述（建模）的必要性

We need the modeling before applying tools and techniques for increasing the reliability of a system Represent the system in terms of mathematical objects that reflect it observed properties Modeling involves process of abstraction: