形式化方法

软件中的形式化方法控制工程周帝2007073087形式化方法By周帝目录1.形式化方法2.软件中的形式化方法3.形式化方法的举例4.形式化方法语言2.1非形式化方法的缺点2.2形式化方法的优点形式化方法By周帝形式化方法定义形式化方法英文的名称是formalmethods。在逻辑科学中是指分析、研究思维形式结构的方法。它把各种具有不同内容的思维形式(主要是命题和推理)加以比较,找出其中各个部分相互联结的方式,如命题中包含概念彼此间的联结,推理中则是各个命题之间的联结,抽取出它们共同的形式结构;再引入表达形式结构的符号语言,用符号与符号之间的联系表达命题或推理的形式结构。形式化方法By周帝个人认为，这样下的定义太过于抽象，并且不好理解。举个易懂的例子，如果一个人长的与周帝相同，且内心想法与周帝一样那么他就是周帝；反之，他就不是周帝。那么我们就能写成为，如果a，且b，那么，则ZD；如果非a，或非b，则非ZD。我们不难看出这是一个逻辑式，ifaandb,thenc;ifnotaornotb,thennotc.形式化方法在古代就运用了,而在现代逻辑中又有了进一步的发展和完善。这种方法特别在数学、计算机科学、人工智能等领域得到广泛运用。它能精确地揭示各种逻辑规律,制定相应的逻辑规则,使各种理论体系更加严密。同时也能正确地训练思维、提高思维的抽象能力。形式化方法By周帝目录1.形式化方法2.软件中的形式化方法3.形式化方法的举例4.形式化方法语言2.1非形式化方法的缺点2.2形式化方法的优点形式化方法By周帝发展软件形式化方法最早可追溯到20世纪50年代后期对于程序设计语言编译技术的研究，即J.Backus提出BNF描述Algol60语言的语法，出现了各种语法分析程序自动生成器以及语法制导的编译方法，使得编译系统的开发从“手工艺制作方式”发展成具有牢固理论基础的系统方法。形式化方法的研究高潮始于20世纪60年代后期，针对当时所谓“软件危机”,人们提出种种解决方法,归纳起来有两类：一是采用工程方法来组织、管理软件的开发过程；二是深入探讨程序和程序开发过程的规律，建立严密的理论，以其用来指导软件开发实践。前者导致“软件工程”的出现和发展，后者则推动了形式化方法的深入研究。经过30多年的研究和应用，如今人们在形式化方法这一领域取得了大量、重要的成果，从早期最简单的形式化方法——一阶谓词演算方法到现在的应用于不同领域、不同阶段的基于逻辑、状态机、网络、进程代数、代数等众多形式化方法。形式化方法的发展趋势逐渐融入软件开发过程的各个阶段,从需求分析、功能描述(规约)、(体系结构/算法)设计、编程、测试直至维护。形式化方法By周帝形式化方法的定义用于开发计算机系统的形式化方法是描述系统性质的基于数学的技术，这样的形式化方法提供了一个框架，可以在框架中以系统的而不是特别的方式刻划、开发和验证系统。如果一个方法有良好的数学基础，那么它就是形式化的，典型地以形式化规约语言给出。这个基础提供一系列精确定义的概念，如：一致性和完整性，以及定义规范的实现和正确性。形式化方法的本质是基于数学的方法来描述目标软件系统属性的一种技术。形式化方法By周帝形式化方法的分类根据说明目标软件系统的方式，形式化方法可以分为两类：1）面向模型的形式化方法。面向模型的方法通过构造一个数学模型来说明系统的行为。2）面向属性的形式化方法。面向属性的方法通过描述目标软件系统的各种属性来间接定义系统行为。形式化方法By周帝形式化方法的分类根据表达能力，形式化方法可以分为五类：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周帝目录1.形式化方法2.软件中的形式化方法3.形式化方法的举例4.形式化方法语言2.1非形式化方法的缺点2.2形式化方法的优点形式化方法By周帝非形式化的缺点用自然语言书写的系统规格说明书，可能存在矛盾、二义性、含糊性、不完整性及抽象层次混乱等问题。矛盾：指一组相互冲突的陈述。监控化学反应容器中的温度，监控在一定范围内的温度二义性：指读者可以用不同方式理解的陈述。操作员标识由操作员姓名和密码组成，密码由6位数字构成。当操作员登陆进系统时它被放在注册文件里含糊性：系统规格说明书庞大，易出现含糊性。不完整性：遗漏了客户的一些需求。例如，AVERAGE命令的功能是显示某个传感器在两个日期内获得的平均水深（每个数据保留6个月）抽象层次混乱：是指在非常抽象的陈述中混进了一些关于细节的低层次陈述。形式化方法By周帝目录1.形式化方法2.软件中的形式化方法3.形式化方法的举例4.形式化方法语言2.1非形式化方法的缺点2.2形式化方法的优点形式化方法By周帝形式化优点在我看来，形式化的方法更像是一种规则，基于数学的计数，描述了系统的性质。正因为它像是一种规则所以具有所以可以做到★简洁准确描述物理现象、对象或动作的结果★适合于表示状态，表示“做什么”★数学规格说明可以用数学方法验证严密统一简洁形式化方法By周帝应用形式化方法的准侧1.应该选用适当的表示方法（每种形式化语言都有各自的特点）2.应该形式化，但不要过分形式化3.应该估算成本4.应该有形式化方法顾问随时提供咨询5.不应该放弃传统的开发方法6.应该建立详尽的文档7.不应该放弃质量标准8.不应该盲目依赖形式化方法9.应该测试、测试再测试10.应该重用同时，应用形式化方法要遵守如下准则形式化方法By周帝目录1.形式化方法2.软件中的形式化方法3.形式化方法的举例4.形式化方法语言2.1非形式化方法的缺点2.2形式化方法的优点形式化方法By周帝形式化转换例子相信通过对比非形式化，我们能对形式化方法有一定的了解下面就想魏老师上课跟我们讲述事物用例那样一步一步的分析，如何讲一个日常的事情用形式化方法装换形式化方法By周帝事例在一幢M层楼的大厦里，用电梯内的和每个楼层的按钮来控制N部电梯的运动。当按下电梯按钮请求电梯在指定楼层停下时，按钮指示灯亮；当电梯到达指定楼层时，指示灯灭。除了大厦的最底层和最高层外，每层楼都有两个按钮分别指示电梯上行和下行。当这两个按钮之一被按下时相应的指示灯亮，当电梯到达此楼层时灯熄灭，电梯向要求的方向移动。当电梯无升降动作时，关门并停在当前楼层。相信大家看到了这个天天都发生在我们身边的例子都会比较晕，究竟应该如何将这个例子转换呢？下面我们来一步一步的分析形式化方法By周帝EB（e,f）：表示按下电梯e内的按钮，并请求到f层去。有两个状态：--EBON（e,f）：电梯按钮（e,f）打开--EBOFF（e,f）：电梯按钮（e,f）关闭两个事件：--EBP（e,f）：电梯按钮（e,f）被按下--EAF（e,f）：电梯e到达f层转换图形式化方法By周帝V（e,f）：电梯e停在f层EBOFF（e,f）+EBP（e,f）+notV（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周帝形式化转换规则S（d，e，f）：电梯e停在f层并且移动方向由d确定为向上（d=U）或向下（d=D）或待定（d=N）。FBOFF（d,f）+FBP（d,f）+notS（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周帝电梯的状态转换电梯的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周帝电梯的状态转换图最后我们能绘制出综合的电梯转换图形式化方法By周帝至此我们将一件事情彻底的用形式化的方法表示出来是不是觉得跟魏老师讲的用例图有几分相似呢？我个人认为，绘制用例图也应该属于将其形式化了，只是在规则上不太一样形式化方法By周帝目录1.形式化方法2.软件中的形式化方法3.形式化方法的举例4.形式化方法语言2.1非形式化方法的缺点2.2形式化方法的优点形式化方法By周帝不同的形式化方法的数学基础是不同的，有的以集合论和一阶谓词演算为基础（如Z和VDM），有的则以时态逻辑为基础。形式化方法需要形式化规约说明语言的支持。像刚才对电梯的分析就属于以时态逻辑为基础的形式化下面为大家简单介绍一下以集合论和一阶谓词演算为基础的Z语言形式化方法By周帝将事物的状态和行为用数学符号形式化表达的语言，为编写计算机程序和验证计算机程序的正确性提供依据，是软件工程中编码之前的规格说明语言。Z语言是由牛津大学程序设计研究小组开发的一种形式语言，之后该小组与IBM的Hursley实验室合作，将Z语言用于IBM客户信息控制系统(CustomerInformationandControlSystem,CICS)的开发，使得最终的产品质量得到了全面的提高，所监测出的错误数量大大减少，并且整体开发费用降低了9%。在ISO指导下的国际标准化Z工作与2002年完成。Z语言形式化方法By周帝Z语言是一种以一阶谓词演算为主要理论基础的规约语言,是一种功能性语言。形式化描述语言Z指的是著名数学家Zermelo，它是目前使用最广泛的一种形式化描述语言，在软件产业的一些大型项目中已经获得成功的应用，Z以带等词的一阶谓词逻辑ZF（Zermelo-Fraenkel，蔡梅罗-弗兰科尔）公理集合论为主要数学基础。在Z中有两种语言：数学语言和模式（Schema）语言。数学语言用来描述系统的各种特征：对象及其之间的关系。模式语言是一种半图形化的语言，它用来构造、组织形式化说明的描述、整理、封装信息块并对其命名以便可以重用这些信息块。通常，形式化说明的可读性都不太好，但由于Z采用半图形化的模式语言，能用一种比较直观、有条理的方式来表达形式化说明，这就改善了可读性。Z语言形式化方法By周帝Z语言1.给定的集合2.状态定义形式化方法By周帝Z格Button_State形式化方法By周帝3.初始状态4.操作操作Push_Button的Z规格说明形式化方法By周