形式化方法在软件开发中的应用

来源:用户上传      作者: 曹斌,刘栓

　　摘 要：形式化方法是把概念、判断、推理转化成特定的形式符号后，对形式符号表达系统进行研究的方法。是用具有精确语义的形式语言书写的程序功能描述，它是设计和编制程序的出发点，也是验证程序是否正确的依据。形式化方法就是用符号化的数学变换把需求分析给准确的表述出来，这样可以确保和需求的一致性，并能用于分析和验证应用程序。
　　关键词：形式化方法；软件开发
　　中图分类号：TP311.52
　　众所周知，软件开发过程中系统安全是至关重要的，任何一个小的错误都可能导致不可逆的灾难性后果，因此这就要求我们在开发应用程序时设计和实现必须保证100%的正确，不能出现任何错误。例如：飞行导航系统、卫星系统、机器人控制等。我们如何才能确保尽量少出现或者不出现问题呢？大家都知道，软件开发必经的几个阶段（需求分析，概要设计，详细设计，实现），越在后面阶段发现问题，我们付出的成本和风险就会越高，我们必须在需求分析阶段明确并准确的描述问题并且保证问题描述的一致性，而且必须以设计为基础对问题加以深入的分析。这就要求我们使用符号化的方法来表述需求，即形式化描述。
　　1 形式化方法
　　1.1 形式化方法的概念
　　形式化方法是把概念、判断、推理转化成特定的形式符号后，对形式符号表达系统进行研究的方法。是用具有精确语义的形式语言书写的程序功能描述，它是设计和编制程序的出发点，也是验证程序是否正确的依据。形式化方法就是用符号化的数学变换把需求分析给准确的表述出来，这样可以确保和需求的一致性，并能用于分析和验证应用程序。毕竟，一个程序本身就是一个正式的规范化语言。
　　1.2 形式化方法的使用
　　形式化方法虽然能够准确、精确地规范和验证开发的软件系统，但是形式化方法也不是万能的，并不是普遍适用于所有的软件项目，一些应用程序是很好理解的，直接实现就好，也有一些应用程序很小，又很好理解，应用形式化方法就是浪费时间。例如：简单的计算器的实现，电话簿的实现根本不需要用形式化方法。当然也不是说复杂的程序必须应用形式化方法，也要视情况而定。针对一个较复杂的程序，形式化方法也可以只对一个部分进行描述，因为部分可能是分析和评估的关键。比如，图形用户界面设计（GUI）通常是不用形式化方法的。也可以不用的部分使用不同的形式化方法，这必须要考虑兼容性问题和整合问题。
　　2 形式化方法的选择
　　针对不同的系统，并不是所有形式化方法都是可用的，每一种形式化方法都有不同的数学定义，通过类型分析决定应用程序采用何种形式化方法；一是面向对象的形式化方法，通过定义状态和操作进行建模，比如：Z语言、VDM、B、Object-Z等方法。二是面向属性的形式化方法，比如：OBJ3、Larch等方法。三是基于并发性的形式化方法，比如CCS、ACP、CSP、LOTOS等方法。四是基于实时性的形式化方法，比如TRIO、RTOZ等方法。
　　3 形式化方法的应用
　　3.1 Z语言的介绍
　　Z语言产生于牛津大学，经过多年的演化其语法和语义与最初版本发生了很大的变化，目前标准由国际标准化组织所统一，它是一种很受欢迎的语言，因为它很简单，它允许非正式和正式的描述混合在一起使用，并被广泛的文献和工具所支持。Z语言是一种基于模型的（描述状态和操作），使用集合概念和逻辑判断，操作表述为使用前置条件和后置条件对程序进行定义。牛津大学曾获得两次Queen’s Award 展示了Z语言在工业上得应用，加拿大的安大略（Ontario Hydro）是另一个展示Z语言在工业上的应用。其竞争对手主要为VDM-SL（Vienna Development Method-Specification Language）和B，VDM是一种广泛应用于工业界的形式化开发方法，数学的精确性使它能够有效地保证系统的设计和开发。基于Z语言又有一些面向对象的扩展，比如：Z++、ZEST、MOOZ、Object-Z。其中Zest（The Eclipse Visualization Toolkit）是在Eclipse 平台基础上开发的一套可视化图形构件集合；Object-Z语言产生于The University of Queens Land（澳大利亚），是Z语言的扩展版本，其语义也是Z语言语义的扩展版本，已被Software Verification Research Center （澳大利亚政府和很多企业资助的重要的研究中心）用在多个项目中。
　　3.2 形式化方法的简单应用
　　我们以Object-Z语言为例来说明形式化方法的应用，例如，一个小公司有两个部门，每个员工属于两个部门中的一个部门，而且每个员工有一个工号，姓名，地址和联系方式；（1）向部门1添加一个员工；（2）向部门2添加一个员工；（3）从部门1调到部门2一个员工以及从部门2调到部门1一个员工；（4）修改公司一个部门员工的地址；（5）报告在一个地址住得员工个数。
　　3.2.1 形式化描述
　　形式化描述是以需求和可设计为基础明确并准确的描述问题并且保证问题描述的一致性，对问题加以深入的分析。使用基于数学逻辑的形式化方法进行描述。首先，根据需求对公司和员工进行建模，然后采用根据功能性需求设定模型的方法。下面是基于形式化方法的具体实现。
　　注：其中，[STRING]是基类，然后创建一个Person类，包含四个属性（员工号、姓名、地址和联系方式）和两个方法（修改地址和修改联系方式）。
　　注：公司类有两个属性即部门1和部门2都为员工的集合，下面是约束条件，确保没有一个人既属于部门1又属于部门2；随后为初始化方法，即两个部门都为空；然后是公司的方法（向部门1添加一个员工，向部门2添加一个员工，从部门1调到部门2一个员工，从部门2调到部门1一个员工）；然后是改变公司员工的住址的方法；最后是报告具有相同地址的人数。
　　3.2.2 形式化描述的实现
　　对于实现，由于程序较为简单，我们可以采用直接生成代码，这样就简化了软件开发的过程，并且通过一致性验证减少了出错的可能性，对此我们可以节约很多资源。采用构造方法基于从低级规范直接导出程序将程序与它的形式描述对应起来，这样也能把构造与验证相统一。同时形式化方法也能自动生成测试用例，简化了测试。
　　4 结束语
　　形式化方法是以简化应用程序开发，用简化的规范化语言准确并精确地描述需求，并保证需求与程序的一致性，采用所支持的工具自动或办自动地生成程序代码，通过一致性验证保证程 序的正确性。
　　参考文献：
　　[1]屈延文.形式语义学基础与形式说明[M].北京：科学出版社，2010.
　　[2]虞慧群，许浩，刘冬梅等.一种基于Object-Z的面向方面建模方法[J].华东理工大学学报（自然科学版），2008.
　　[3]缪淮扣，李刚，朱关铭.软件工程语言-Z[M].上海：上海科学技术文献出版社，1999.
　　[4]JIM W，PETER G L，JUAN B，et al. Formal methods：Practice and experience [J].Journal of ACM Computing Surveys，2009.
　　[5]李莹，吴江琴.软件工程形式化方法与语言[M].杭州：浙江大学出版社，2010.
　　[6]缪淮扣，陈怡海.软件形式规格说明语言-Z[M].北京：清华大学出版社，2012.
　　作者简介：曹斌，男，助教，研究方向：软件工程、网络、iOS研究。
　　作者单位：黄淮学院信息工程学院，河南驻马店 463000
转载注明来源:https://www.xzbu.com/8/view-6157817.htm