形式化方法
By 周帝
形式化方法的定义
用于开发计算机系统的形式化方法是描述系统 性质的基于数学的技术，这样的形式化方法提供了 一个框架，可以在框架中以系统的而不是特别的方 式刻划、开发和验 证系统。 如果一个方法有良好 的数学基础，那么它就是形式化的，典型地以形式 化规约语言给出。这个基础提供一系列精确定义的 概念，如：一致性和完整性，以及定义规范 的实 现和正确性。 形式化方法的本质是基于数学的方 法来描述目标软件系统属性的一种技术。
形式化方法
By 周帝
目录
1.形式化方法 形式化方法 2.软件中的形式化方法 软件中的形式化方法 2.1非形式化方法的缺点 非形式化方法的缺点 2.2形式化方法的优点 形式化方法的优点 3.形式化方法的举例 形式化方法的举例 4.形式化方法语言 形式化方法语言
形式化方法
By 周帝
形式化转换例子
相信通过对比非形式化， 相信通过对比非形式化，我们能对形式化 方法有一定的了解 下面就想魏老师上课跟我们讲述事物用例 那样一步一步的分析， 那样一步一步的分析，如何讲一个日常的 事情用形式化方法装换
形式化方法
By 周帝
形式化方法的分类
根据说明目标软件系统的方式，形式化方法可 以分为两类： 1）面向模型的形式化方法。面向模型的方法 通过构造一个数学模型来说明系统的行为。 2）面向属性的形式化方法。面向属性的方法 通过描述目标软件系统的各种属性来间接定义 系统行为。
形式化方法
By 周帝
形式化方法的分类
形式化方法
By 周帝
个人认为，这样下的定义太过于抽象，并且不好理解。 举个易懂的例子，如果一个人长的与周帝相同，且内心 想法与周帝一样那么他就是周帝；反之，他就不是周帝。 那么我们就能写成为，如果a， 且b，那么，则ZD；如果非a， 或非b，则非ZD。 我们不难看出这是一个逻辑式，if a and b, then c; if not a or not b, then not c.
根据表达能力，形式化方法可以分为五类： 1）基于模型的方法：通过明确定义状态和操作来建立一个系统模型（使系统从一 个状态转换到另一个状态）。用这种方法虽可以表示非功能性需求（诸如时间 需求），但不能很好地表示并发性。如：Z语言，VDM，B方法等。 2）基于逻辑的方法：用逻辑描述系统预期的性能，包括底层规约、时序和可能性 行为。采用与所选逻辑相关的公理系统证明系统具有预期的性能。用具体的编 程构 造扩充逻辑从而得到一种广谱形式化方法，通过保持正确性的细化步骤集 来开发系统。如：ITL（区间时序逻辑），区段演算（DC），hoare 逻辑， WP演算，模态逻辑，时序逻辑，TAM（时序代理模型），RTTL（实时时序逻 辑）等。 3）代数方法：通过将未定义状态下不同的操作行为相联系，给出操作的显式定义。 与基于模型的方法相同的是，没有给出并发的显式表示。如：OBJ， Larch族 代数规约语言等； 4）过程代数方法：通过限制所有容许的可观察的过程间通信来表示系统行为。此 类方法允许并发过程的显式表示。如：通信顺序过程（CSP），通信系统演算 （CCS），通信过程代数（ACP），时序排序规约语言（LOTOS），计时 CSP(TCSP），通信系统计时可能性演算（TPCCS）等。 5）基于网络的方法：由于图形化表示法易于理解，而且非专业人员能够使用，因 此是一种通用的系统确定表示法。该方法采用具有形式语义的图形语言，为系 统开发和再工程带来特殊的好处。如 Petri图，计时Petri图，状态图等。
形式化方法
By 周帝
形式化转换规则 S（d，e，f）：电梯e停在f层并且移动方 向由d确定为向上（d=U）或向下（d=D） 或待定（d=N）。 FBOFF（d,f）+ FBP（d,f）+not S（d， 1……n，f） → FBON（d,f） FBON（d,f）+ EAF（1……n,f）+ S（d， 1……n，f） → FBOFF（d,f） 其中d=UorD
形式化方法
By 周帝
目录
1.形式化方法 形式化方法 2.软件中的形式化方法 软件中的形式化方法 2.1非形式化方法的缺点 非形式化方法的缺点 2.2形式化方法的优点 形式化方法的优点 3.形式化方法的举例 形式化方法的举例 4.形式化方法语言 形式化方法语言
形式化方法
By 周帝
形式化优点
在我看来，形式化的方法更像是一种规则， 基于数学的计数，描述了系统的性质。正 因为它像是一种规则所以具有
形式化方法
By 周帝
形式化方法定义
形式化方法英文的名称是formal methods。 在逻辑科学中是指分析、研究思维形式结构的方法。 它把各种具有不同内容的思维形式(主要是命题和 推理)加以比较,找出其中各个部分相互联结的方式, 如命题中包含概念彼此间的联结,推理中则是各个 命题之间的联结,抽取出它们共同的形式结构;再引 , ; 入表达形式结构的符号语言,用符号与符号之间的 联系表达命题或推理的形式结构。
严
统
简洁
所以可以做到 ★简洁准确描述物理现象、对象或动作的结果 ★适合于表示状态，表示“做什么” ★数学规格说明 可以用数学方法验证
形式化方法
By 周帝
应用形式化方法的准侧
同时，应用形式化方法要遵守如下准则 1.应该选用适当的表示方法（每种形式化语言 都有各自的特点） 2.应该形式化，但不要过分形式化 3.应该估算成本 4.应该有形式化方法顾问随时提供咨询 5.不应该放弃传统的开发方法 6.应该建立详尽的文档 7.不应该放弃质量标准 8.不应该盲目依赖形式化方法 9.应该测试、测试再测试 10.应该重用
软件中的形式化方法
控制工程
周帝
2007073087
形式化方法
By 周帝
目录
1.形式化方法 形式化方法 2.软件中的形式化方法 软件中的形式化方法 2.1非形式化方法的缺点 非形式化方法的缺点 2.2形式化方法的优点 形式化方法的优点 3.形式化方法的举例 形式化方法的举例 4.形式化方法语言 形式化方法语言
形式化方法
By 周帝
形式化转换规则 V（e,f）：电梯e停在f层 EBOFF（e,f）+EBP（e,f）+not V （e,f）→ EBON（e,f） EBON（e,f）+EAF（e,f）→ EBOFF（e,f）
形式化方法
By 周帝
楼层按钮的状态转换图
FB（d,f）：表示f层请求电梯向d方向运动的按钮。 有两个状态： --FBON（d,f）：楼层按钮（d,f）打开 --FBOFF（d,f）：楼层按钮（d,f）关闭 两个事件： -- FBP（d,f）：楼层按钮（d,f）被按下 -- EAF（1……n,f）：电梯1或……或n到达f层
形式化方法
By 周帝
电梯的状态转换图
最后我们能绘制出综合的电梯转换图
形式化方法
By 周帝
至此我们将一件事情彻底的用形式化的方 法表示出来 是不是觉得跟魏老师讲的用例图有几分相 似呢？ 似呢？ 我个人认为， 我个人认为，绘制用例图也应该属于将其 形式化了， 形式化了，只是在规则上不太一样
形式化方法
ቤተ መጻሕፍቲ ባይዱ
By 周帝
目录
1.形式化方法 形式化方法 2.软件中的形式化方法 软件中的形式化方法 2.1非形式化方法的缺点 非形式化方法的缺点 2.2形式化方法的优点 形式化方法的优点 3.形式化方法的举例 形式化方法的举例 4.形式化方法语言 形式化方法语言
形式化方法
By 周帝
不同的形式化方法的数学基础是不同的， 不同的形式化方法的数学基础是不同的， 为基础（ 有的以集合论和一阶谓词演算为基础（如Z ），有的则以 为基础。 和 VDM），有的则以时态逻辑为基础。形 ）， 形式化规约说明语言的支持 式化方法需要形式化规约说明语言的支持。 式化方法需要形式化规约说明语言的支持。 像刚才对电梯的分析就属于以时态逻辑为 基础的形式化 下面为大家简单介绍一下以集合论和一阶 谓词演算为基础的Z语言 谓词演算为基础的 语言
相信大家看到了这个天天都发生在我们身边的例子 都会比较晕，究竟应该如何将这个例子转换呢？ 都会比较晕，究竟应该如何将这个例子转换呢？ 下面我们来一步一步的分析
形式化方法
By 周帝
转换图
EB（e,f）：表示按下电梯e内的按钮，并请求到f层去。 有两个状态： --EBON（e,f）：电梯按钮（e,f）打开 --EBOFF（e,f）：电梯按钮（e,f）关闭 两个事件： --EBP（e,f）：电梯按钮（e,f）被按下 --EBP e,f e,f -- EAF（e,f）：电梯e到达f层
形式化方法
By 周帝
电梯的状态转换
电梯的3个状态： M（d，e，f）：电梯e沿着d方向移动，即将到达的 是第f层 S（d，e，f）：电梯e停在f层，将朝d方向移动（尚 未关门） W（e，f）：电梯e在f层等待（已关门） 电梯的3个事件： DC（e，f）：电梯e在楼层f关上门 ST （e，f）：电梯e靠近f层时触发传感器，电梯控 制器决定在当前楼层电梯是否停下 RL：电梯按钮或楼层按钮被按下进入打开状态
形式化方法
By 周帝
发展
软件形式化方法最早可追溯到20世纪50年代后期对于程序 设计语言编译技术的研究，即J.Backus提出BNF描述Algol60语 言的语法，出现了各 种语法分析程序自动生成器以及语法制导 的编译方法，使得编译系统的开发从“手工艺制作方式”发展成 具有牢固理论基础的系统方法。形式化方法的研究高潮始于 20 世纪60年代后期，针对当时所谓“软件危机”,人们提出种种解 决方法,归纳起来有两类：一是采用工程方法来组织、管理软件 的开发过程；二是深入探讨程 序和程序开发过程的规律，建立 严密的理论，以其用来指导软件开发实践。前者导致“软件工程” 的出现和发展，后者则推动了形式化方法的深入研究。经过30 多 年的研究和应用，如今人们在形式化方法这一领域取得了大 量、重要的成果，从早期最简单的形式化方法——一阶谓词演算 方法到现在的应用于不同领域、不同阶段 的基于逻辑、状态机、 网络、进程代数、代数等众多形式化方法。形式化方法的发展趋 势逐渐融入软件开发过程的各个阶段,从需求分析、功能描述(规 约)、(体 系结构/算法)设计、编程、测试直至维护。