形式化说明技术

第4章形式化说明技术北京科技大学经管学院崔建双1北京科技大学东凌经济管理学院2020/1/23软件开发的形式化方法起源针对软件危机人们提出种种解决方法，其一是以工程方法来组织、管理软件的开发过程，导致“软件工程”的出现和发展。其二是深入探讨程序开发过程的规律，建立严密的理论，用以指导软件开发实践，导致基于模型、基于逻辑、状态机、基于网络图形化、进程代数、代数等众多形式化方法的发展并逐渐融入从需求分析、功能描述(规约)、(体系结构/算法)设计、编程、测试直至维护的各个阶段。软件开发中的形式化方法如状态图形的有穷状态机（UML）等。非形式化方法：通过自然语言来描述事务的发生和发展。如用户需求陈述。半形式化方法：诸如软件开发中的数据流图或实体－联系图等。1.概述（1）非形式化方法的缺点自然语言书写的系统规格说明书有如下不足：因不同程序员撰写，出现“矛盾”描述；同理，“二义”；如：“操作员标识由操作员姓名和密码组成，密码由6位数字构成，当操作员登陆系统时它被存储在注册文件中。”“它”的含义二义。含糊；如“系统界面对用户应该是有好的”不完整；抽象层次混乱。（2）形式化方法的优点数学是理想的建模工具，适合于表示系统状态和描述系统需求；用数学表达的需求可在不同开发阶段平滑过渡。数学提供了高层确认的手段，可验证设计结果的正确性。（3）形式化方法的选用准则选择合适的形式化方法；应该形式化，但不要过分形式化；应该估算成本；应该有形式化方法顾问随时提供咨询；不应该放弃传统的开发方法；应该建立详尽的文档；不应该放弃质量标准；不应该盲目依赖形式化方法；应该测试、测试再测试；应该重用。（1）概念2.有限状态机法（FiniteStateMachine）现实中很多系统的行为可以用有限个状态来表达，如:红绿灯（红、绿、黄）、电话机（摘机、挂机、通话、忙等）。行为之间的转换就完成了系统的运行。软件系统的运行也都是由有限个状态所组成的，因不同的输入而衍生出各个状态。红绿灯的状态演变2020/1/23通信软件设计第9页有限状态机的几个基本术语–状态（State）对象在其生命周期中的一种状况，处于某个特定状态中的对象必然会满足某些条件、执行某些动作或者是等待某些事件的到来。–事件（Event）会引起状态变迁，促使从一种状态切换到另一种状态。–转换（Transition）对象在某个事件发生，同时某个特定条件满足时进入下一个状态的过程。–动作（Action）状态机可以执行的原子操作（运行中不可中断）。（2）举例锁有三个位置：1、2、3；转盘可向左（L）或右（R）；锁密码：1L、3R、2L，仅此行为才能解锁。总结：一个有穷状态机包括5部分：1）状态集J：{保险箱锁定，A，B，保险箱解锁，报警}2）输入集K：{1L,1R,2L,2R,3L,3R}3）转换函数T，如表4.14）初始态S：保险箱锁定5）终态集F：{保险箱解锁，报警}更形式化的术语：一个有穷状态机可表示一个为5元组（J,K,T,S,F）状态转换形式：当前状态【菜单】＋事件【所选择的项】＝下个状态计算机系统中每个菜单驱动的用户界面都是一个有穷状态机的实现。定义状态：（1）M(d,e,f)：电梯e正沿d方向移动，即将到达第f层楼。（2）S(d,e,f)：电梯e停在f层楼，将朝d方向移动（未关门）。（3）W(e,f)：电梯e在f层等待（已关门）。（4）DC(e,f)：电梯e在楼层f关上门。（5）ST(e,f)：电梯e靠近f层时触发传感器，电梯控制器决定在当前楼层是否停下。（6）RL：电梯按钮或楼层按钮被按下进入打开状态（3）电梯的状态转换例电梯状态转换规则：①S(U,e,f)+DC(e,f)=M(U,e,f+1);②S(D,e,f)+DC(e,f)=M(D,e,f-1);③S(N,e,f)+DC(e,f)=W(e,f)（4）评价有穷状态机（FSM）描述规格说明：当前状态＋事件＋谓词=下个状态易于书写、验证、转变成设计或程序代码。优点：比数据流图技术更精确，一样易于理解。缺点：不能处理定时需求。3.PETRI网（1）概念Petri网是一种网状信息流模型，在条件和事件为节点的有向二分图基础上添加表示状态信息的令牌分布，并按引发规则使得事件驱动状态演变，从而反映系统动态运行过程。Petri网可用于软件开发过程建模。控制系统的并发性。（2）例1Petri网包含4种元素：一组位置P、一组转换T、输入函数I以及输出函数O。Petri网包含4种元素：1）一组位置P，上例P＝{P1,P2,P3,P4}2）一组转换T，上例T＝{t1,t2}3）输入函数I，上例I（t1）={P2,P4}I（t2）={P2}4）输出函数O，上例O（t1）={P1}O（t2）={P3,P3}形式化的Petri网结构是一个4元组（P，T，I，O）权标向量（1，2，0，1）说明：当每个输入位置所拥有的权标数大于等于从该位置到转换的线数时，就允许转换。当t1被激发时，P2和P4上各有一个权标被移出，而P1上只能增加一个权标权标向量（2，1，0，0）权标向量（2，0，2，0）形式化表达：标记M：P{0,1,2,…}Petri网成为一个5元组（P，T，I，O，M）对Petri网的一个重要扩充是加入禁止线：说明：当每个输入线上至少有一个权标，而禁止线上没有权标的时候，相应的转换才是允许的（3）例2电梯按钮EBf电梯中楼层f的按钮；Fg楼层g；Ff楼层f。楼层按钮FBfu第f楼层向上按钮；FBfd第f楼层向下按钮；Z语言是一种以一阶谓词演算为主要理论基础的一种规约语言，是功能性语言。Z语言将事物的状态和行为用数学符号形式化表达，为编写计算机程序和验证计算机程序的正确性提供依据，是软件工程中编码之前的规格说明语言。4.Z语言（1）概念简介Z语言描述的最简单形式化规格说明含有下述4个部分：给定的集合、数据类型及常数。状态定义。初始状态。操作。给定的集合一个Z规格说明从一系列给定的初始化集合开始。所谓初始化集合就是不需要详细定义的集合，这种集合用带方括号的形式表示。对于电梯问题，给定的初始化集合称为Button，即所有按钮的集合，因此，Z规格说明开始于：〔Button〕状态定义一个Z规格说明由若干个“格(schema)”组成，每个格含有一组变量说明和一系列限定变量取值范围的谓词。例如，格S的格式如图4.12所示。图4.12Z格S的格式在电梯问题中，Button有4个子集，即floor_buttons(楼层按钮的集合)、elevator_buttons(电梯按钮的集合)、buttons(电梯问题中所有按钮的集合)以及pushed(所有被按的按钮的集合，即所有处于打开状态的按钮的集合)。图4.13描述了格Button_State，其中，符号P表示幂集(即给定集的所有子集)。约束条件声明，floor_buttons集与elevator_buttons集不相交，而且它们共同组成buttons集(在下面的讨论中并不需要floor_buttons集和elevator_buttons集，把它们放于图4.13中只是用来说明Z格包含的内容)。图4.13Z格Button_State初始状态抽象的初始状态是指系统第一次开启时的状态。对于电梯问题来说，抽象的初始状态为：Button_Init〔Button_State｜pushed=Φ〕上式表示，当系统首次开启时pushed集为空，即所有按钮都处于关闭状态。操作如果一个原来处于关闭状态的按钮被按下，则该按钮开启，这个按钮就被添加到pushed集中。图4.14定义了操作Push_Button(按按钮)。ˆ图4.14操作Push_Button的Z规格说明操作的谓词部分，包含了一组调用操作的前置条件，以及操作完全结束后的后置条件。如果前置条件成立，则操作执行完成后可得到后置条件。但是，如果在前置条件不成立的情况下调用该操作，则不能得到指定的结果(因此结果无法预测)。假设电梯到达了某楼层，如果相应的楼层按钮已经打开，则此时它会关闭；同样，如果相应的电梯按钮已经打开，则此时它也会关闭。也就是说，如果“button?”属于pushed集，则将它移出该集合，如图4.15所示(符号“＼”表示集合差运算)。图4.15操作Floor_Arrival的Z规格说明已经在许多软件开发项目中成功地运用了Z语言，目前，Z也许是应用得最广泛的形式化语言，尤其是在大型项目中Z语言的优势更加明显。Z语言之所以会获得如此多的成功，主要有以下几个原因：(1)可以比较容易地发现用Z写的规格说明的错误，特别是在自己审查规格说明，及根据形式化的规格说明来审查设计与代码时，情况更是如此。(2)用Z写规格说明时，要求作者十分精确地使用Z说明符。由于对精确性的要求很高，从而和非形式化规格说明相比，减少了模糊性、不一致性和遗漏。（2）评价(3)Z是一种形式化语言，在需要时开发者可以严格地验证规格说明的正确性。(4)虽然完全学会Z语言相当困难，但是，经验表明，只学过中学数学的软件开发人员仍然可以只用比较短的时间就学会编写Z规格说明，当然，这些人还没有能力证明规格说明的结果是否正确。(5)使用Z语言可以降低软件开发费用。虽然用Z写规格说明所需用的时间比使用非形式化技术要多，但开发过程所需要的总时间却减少了。(6)虽然用户无法理解用Z写的规格说明，但是，可以依据Z规格说明用自然语言重写规格说明。经验证明，这样得到的自然语言规格说明，比直接用自然语言写出的非形式化规格说明更清楚、更正确。使用形式化规格说明是全球的总趋势，过去，主要是欧洲习惯于使用形式化规格说明技术，现在越来越多的美国公司也开始使用形式化规格说明技术。小结基于数学的形式化说明技术，目前还没有在软件产业界广泛应用；把形式化方法与传统方法有机结合，可能是未来发展趋势。第3,4章练习题填空题：1、需求分析过程应该建立3种模型，它们分别是（）、（）和（）。2、按照形式化的程度，可以把软件工程使用的方法划分成（）、（）和（）等3类。3、验证软件需求应该从以下4个方面进行验证，即（）、（）、（）和（）。4、需求分析的任务包括系统综合要求、数据要求、导出逻辑模型和修正系统开发计划等。其中常见的接口需求有：用户接口需求、（）、（）和通信接口需求等等。4、需求分析的任务包括（）、（）、（）和修正系统开发计划等。5、需求分析的任务包括系统综合要求、数据要求、导出逻辑模型和修正系统开发计划等。其中设计约束或实现约束常见的有：（）、工具和语言约束、（）、应该使用的标准和应该使用的（）等。判断题：1、形式化方法有许多优点，因此在实际软件工作中应该依赖形式化方法来保证开发出的软件绝对正确和降低由于设计缺陷产生的维护代价。（）2、可以用形式化方法证明软件的需求和设计的正确性和合理性，因此，如果为了降低软件的测试成本和改正错误代价等，可以不用对软件进行测试，也可以保证软件的质量和降低开发成本等软件工程的目标。（）名词解释：1、实体-联系图（ER图）2、状态转换图3、IPO图4、Petri网简答题：1、简述需求分析的原则。2、简述形式化方法的准则。3、课后题P73，第1、2题；P89，第1、2题45北京科技大学东凌经济管理学院2020/1/23本讲结束