形式化方法在软件工程中的应用研究

苗德成，冯黎波

（1．韶关学院数学与信息科学学院，广东韶关 512000；2．河北科技大学理学院，河北石家庄 050018）

形式化方法在软件工程中的应用研究

苗德成1，冯黎波2

（1．韶关学院数学与信息科学学院，广东韶关 512000；2．河北科技大学理学院，河北石家庄 050018）

探讨了形式化方法的基本概念，重点研究了形式化方法的数学理论基础和其在软件工程各阶段的应用情况，分析了形式化方法在理论研究和工程实践上的优势和局限性及其原因，并指出了形式化方法发展的几个方向，最后对形式化方法在软件工程中的应用做了评价。

形式化方法；软件规约形式语言；软件工程；形式系统；规约

基于软件工程方法论，软件工程是将客观世界实际问题抽象成认识世界概念模型，再将认识世界概念模型转换为程序世界可执行程序集合的活动，前者是认知领域符号推演与系统论证过程，而后者则是工程领域理论实践与计算转换过程。在软件工程活动中成功运用形式化方法将实际问题认知模型转换为软件规约［1］（software specification）可缩短软件开发周期并减少项目研制成本，软件规约既是系统分析师、设计师、程序员与用户之间的协议，也是系统模块与程序部分的界面，只要保证软件规约对实际问题描述的可靠性与协调性，就能确保软件系统实现的完备性与一致性。

1 形式化方法

软件工程活动中形式化方法虽然被广泛使用，但形式语言、形式系统等相关基本概念并未有精确定义。形式语言（formal language）是按一定语法规则构成的公式或符号串的有限或无限集［2］。一阶语言（firstorder language），Ada，Fortran，Java等都是形式语言［3］。形式系统是建立在形式语言基础上的一个逻辑演绎系统以完成特定符号推演过程。从形式系统和实际问题复杂性分析，形式化方法是具有坚实数学基础，使用形式语言构建形式系统全面描述和系统分析现实世界复杂问题的一种有效工具。形式化方法基本含义是用数学方法解决计算机科学理论研究和软件工程实践相关问题的工具，集合论、数理逻辑、代数理论、程序设计语言理论、构造类型论（constructive type theory）等数学理论构成了形式化方法坚实的理论基础。

对于形式化方法在软件工程中的具体应用，集合论（含可解决罗素悖论问题的直觉集合论）各种算子、序关系（如点态序［5］、基于Egli－Milner偏序与Smyth偏序的幂域理论等）适于描述软件系统状态转换，而数理逻辑是形式化方法最重要的理论工具，软件系统的业务逻辑可用形式理论［3］及相关演算完成，业务逻辑的服务用形式理论闭包（formal theory closures）描述，通过修正演算形成软件版本的演变，而软件版本序列的可交换性保证实际软件功能具有较好的可扩展性。形式化方法坚实的理论基础在于其内在的数学结构，从数学理论角度分析，任何复杂的数学结构均可建于集合、逻辑等基本数学概念上，因此，集合论和数理逻辑这2种数学工具构成了形式化方法最为重要的数学理论基础，如图1所示。

类别代数（sorted algebras）尤其是∑－代数等多类别代数是抽象数据类型（abstract data type）的理论基础，基于∑－代数的等式理论（equation theories）与项重写系统（term rewriting systems）拓展了自动定理证明领域，很好地解决程序终止性问题、完备性算法与统一性算法（unification algorithms）等问题［5］。范畴论在计算机科学中有广泛应用，其许多技术成为形式化方法重要工具，双笛卡尔闭范畴（bicartesian closed categories）等形式系统的范畴分析非常适合于描述客观世界复杂问题，而范畴论与组合逻辑结合为函数型语言的编译程序提供新方法，进程代数、共代数、界程演算等理论推进了形式化方法进一步发展。程序设计语言理论分析程序设计语言的语法性质、操作特性和语义形式，描述所开发软件系统结构、组成、有穷自动机［4］（finite automata）及与软件工程各阶段对应的形式模型，其中，递归计算是程序设计语言理论有效处理程序循环结构的一项核心技术，而泛函分析的不动点理论（fixed point theory）是设计程序指称语义时高效处理递归计算的重要工具。构造类型论为软件系统设计与研发提供一个新框架［5］，数理逻辑与程序设计语言理论在这个新的框架内有机结合，在一个形式系统内同时描述软件规约与程序设计，自动生成软件并进行程序验证。形式化方法以图1的数学理论为基础，形成了应用于软件生命周期不同阶段不同的软件规约形式语言SSFL（software specification formal language）。

图1 形式化方法的数学基础Fig．1 Mathematical foundation of formal methods

2 软件工程各阶段的规约描述

按照软件工程“自顶向下、逐步求精”的原则将软件开发生命周期分为6个阶段：可行性分析、需求分析、体系结构设计、详细设计、编码、测试发布，形式化方法贯穿软件工程整个生命周期。SSFL是形式化方法重要外延，SSFL的衡量标准是抽象表达的准确性与清晰性、概念运用的标准性与无二义性、形式化处理能力的支持性与可解释性等。SSFL类型较多，每种SSFL数学基础不同，其应用侧重点也不同。SSFL总体上分为3类：非形式化、半形式化和形式化［6］。非形式化SSFL描述框架性内容，以图形或自然语言辅助说明主体信息；半形式化SSFL用BNF描述语法，不进行形式化语义定义而用伪码设计接口和模块；形式化SSFL基于参数化的类别代数等数学理论形式化表述语法和定义语义。

2．1 可行性分析

可行性分析是软件生命周期的第1阶段，运用大量数据资料对影响软件系统开发各种因素全面、系统地论证待开发系统项目是否可行，提出综合分析评价，指出项目可行性、风险预测和建议为项目决策提供依据。本阶段将客观世界实际问题从初始概念转换为可行性研究报告，文档准确分析市场需求，合理确定投资方案，规定具体采纳的软件标准或规范，定义专业术语并列出缩写词原文，说明待开发软件系统输入／输出、基本数据流程和处理流程、软硬运行环境、开发环境条件和限制及软件投入使用的最迟时间等技术、功能或性能指标。

当前极少有专门定位于可行性分析的形式化方法，其主要原因在于难以将自然语言表达能力与形式化方法符号演算系统很好地结合起来，达到普通用户既可理解形式系统的描述，同时又可保持形式化方法精确、可推演等优势的终极目标目前看来还需要许多工作要做。Z语言基于模式演算［7］，是一种运算功能强大但不可执行的半形式化语言，Z语言的最大优点是采用非形式化的英语对软件规约解释，短小且易于阅读。

2．2 需求分析

需求分析以可行性分析报告作为输入，分信息预处理和信息处理2个子阶段，前者要求SSFL可读性好、易修改、可维护，后者要求SSFL精确无二义性并可进行完整性检查和一致性证明。将可行性分析非形式化处理部分与本阶段形式化处理部分联系起来是需求分析难点，需求规格说明书是与用户交流的主要物质基础。

VDM（vienna development method）元语言是一种形式化语言［8］，基于谓词演算和集合论的证明规则，采用“面向模型”方法给出抽象机状态确定模型，生成文档可读性好，程序员易于掌握和实现原型。从形式化处理角度上分析，指称语义的设计是需求分析阶段主要工作之一，VDM写指称语义基本步骤是构建语法域与语义域，建立语义解释函数并定义一些辅助函数，然后利用语义方程解释语法单位的语义，其中域的构造是重点，VDM由原始域（数值域、字符域、真值域等）经并、积、幂、子等算子和投影（projection）、注入（injection）、检查（inspection）等原子操作构造所需各种域。但是VDM在需求分析阶段的使用存在明显缺陷，第一，它缺乏模块性；第二，VDM不能处理并发的情况，而RAISE（Rigorous approach to industrial software engineering）语言弥补了VDM的不足［9］。RAISE使用的代数法与VDM基于模型的方法存在明显不同，即如何描述规约和对规约语言赋予语义，VDM没有明确解决怎样将这不同结合起来，而RAISE很好地做到了这一点。RAISE是一种光谱语言，既可以在需求分析阶段书写初级抽象规约，也可以在详细设计阶段描述自动转换为编码阶段所需的程序设计语言的具体规约，RAISE提供一系列工具和转换技术，形成处理需求分析阶段全过程的严格方法。

SXL（state transition language）语言是可执行的SSFL，在需求分析阶段从可行性分析报告描述的实际问题中导出E－R框架，根据E－R框架给出SXL语言的对象和事实，SXL语言的执行有助于开发团队交流和理解［10］。VDM元语言、RAISE语言和SXL语言都是软件工程需求分析阶段普遍应用的形式化方法。

2．3 体系结构设计

体系结构设计是软件设计第1阶段，该阶段根本目的是将需求规格说明书转换为计算机可以实现的目标系统，对上阶段各种备选方案综合分析比较，选出最佳方案与用户达成共识后为软件确定数据结构并设计数据库，提交体系结构设计说明书参加评审。体系结构设计侧重描述软件系统的接口、功能和结构，使用过程代数等形式化工具利用输入、输出间关系描述系统行为，将软件规约模块化而减少设计自由度。

TLG（two level grammar）语言适合软件工程体系结构设计阶段仅需说明做什么而不强调如何做的特点而在本阶段得到普遍应用，TLG在表示形式上与Prolog相似，针对软件系统形式化规约说明将自然语言嵌入严格的数学函数和逻辑程序设计范型中，书写简单，易于论证用户需求的一致性［11］。

基于图形用户界面和可用形式化方法描述图形界面程序设计环境的考虑，GLIDE也是本阶段可用的一种半形式化的SSFL，其主体部分为图形程序设计环境数据结构的产品集、简单查询、描述转换和转换不变式（transform invariant）的谓词集［12］。GLIDE优点是抽象级别高，应用范围广，使用局限在于相应的软件规约必须予以适当修改和扩充。

2．4 详细设计

详细设计是软件设计第2阶段，本阶段基本要求是与上阶段软件系统形式化描述保持一致。在体系结构设计基础上，为软件系统各模块确定相应算法及内部数据结构，获得目标系统具体实现的精确描述，文档详细设计说明书为下阶段编码工作做好准备。

Larch语言基于一阶谓词逻辑用于说明程序序列功能，接口部分描述数据操作效果，核心部分描述独立于计算模型固有特性，对Larch适当扩充可增强详细设计阶段软件系统描述及处理能力［13］。形式化的Trace语言也是软件工程详细设计阶段一种广泛应用的形式化工具，用迹断言（trace assertion）方法说明每个模块接口需求，将模块实现的抽象数据对象作为有穷自动机，其外部所有可见行为都是由对象的迹完全决定［14］。Trace语言不同于其他SSFL的突出特点是其定义抽象对象的方程式集作为一个等式系统可用项重写模拟，将迹断言规则视为迹重写规则（trace rewriting rule）可形式化地得到迹重写系统（trace rewriting system），从而在同一形式系统内同时进行程序的自动生成与验证。

在软件工程详细设计阶段，半形式化的Larch语言也可由项重写实现，进一步增强规约描述的可读性。详细设计阶段传统的SSFL主要用于顺序系统，但也有许多形式化技术支持并发系统，如Modula，Gypsy，Mesa等［15］。

2．5 编 码

本阶段将详细设计阶段成果用计算机程序设计语言描述出来，得到可在计算机上执行的程序。编码阶段程序设计语言的选择、编码风格的把握和编程技巧的运用直接影响程序可靠性、可读性、可测试性和可维护性。

本阶段有较多的SSFL进行形式处理工作，LOTOS（language of temporal ordering specification）语言是一种精确定义且可执行、可证明的形式化语言［15］，LOTOS由2部分构成，基于CCS（calculus of communication systems）和CSP（communicating sequential processes）的进程代数和基于代数语言ACT One／Two的抽象代数［16］，前者用于表示系统的时序行为，后者根据数据类型、操作函数等描述编码阶段的具体数据，LOTOS已成为OSI形式描述技术的事实标准且适用于分布式系统。

ADTS（algebraic data type specification）语言基于严格的多类别代数对软件规约进行形式化推理［17］，支持可构造性、模块化、参数化和异常处理，在ADTS可执行原型环境中以类似项重写的方式可转换为Pascal程序设计语言，在软件工程编码阶段单元模块设计中非常有用。

近年来一些程序构造的形式系统被引入软件工程活动中，基于Martin－löf构造类型论的SSFL技术在软件工程编码阶段得到了广泛的应用。许多Martin－löf构造类型论的形式化方法将程序与软件规约形式说明对应起来，这些形式化方法不再使用Tarski真值语义，而是利用命题和集合之间Curry－Howard同态的Brouwer－Heyting－Kolmogorov直觉语义解释Ξ，Π等逻辑常数，把集合转换为解决实际问题的软件规约，用集合内元素构造满足该软件规约的程序，当前已经开发出许多以构造类型论为基础的形式系统（如LCF，ALF，Coq等）可完成程序开发、验证及形式化证明。

2．6 测试发布

测试发布是软件工程活动最后阶段，本阶段在软件投入运行前对软件生命周期各阶段文档和程序源代码进行查错和纠错，从用户角度精心设计一批测试用例运行程序，暴露软件中潜在错误、缺陷及风险，验证软件是否满足用户要求。

长期理论研究和工程实践积累了丰富的形式化测试和发布技术，分布式网络系统的并发度、不确定性、分布控制和安全性及可靠性等问题是当前软件工程测试发布阶段SSFL研究的重点，其中，形式验证和测试集成方法是新兴的研究热点［18］。形式化测试序列和测试覆盖标准基于控制流或数据流，从EFA（extended finite automata）或Petri网可达图中产生测试序列。OBJ语言是一种形式化的宽域语言，以独立于实现的方式描述数据结构，其可执行性使得可按源代码测试方式验证软件规约［19］。OBJEX是一个形式化测试工具，基于重写规则执行软件规约形式说明完成语法和类型检查。

3 形式化方法的简要评价

形式化方法在软件工程各阶段的广泛应用有效地改进软件质量［20］，提高开发效率，减少开发费用，形式化方法作为一种有效的交流形式易于在软件规约上取得一致，软件工程各阶段的文档既是开发团队与用户交流的重要依据，又是软件开发的起点。形式化方法在软件开发中的优势主要在于问题抽象、语法定义准确、语义清晰可操纵、表达无二义性、描述简洁规范，形式化方法独特优势还体现在软件系统非功能特性的证明上，保密性、安全性和结构性要求等非功能特性难以用传统的测试技术核查，形式化方法利用数学工具求解确定的近似解可进行有效地核查。

形式化方法在软件工程各阶段取得很大成功，但在理论研究和工程实践上仍存在一些局限性，尤其是由于缺乏有效工具而在实际工业项目中应用相对较少，形式化方法的工业标准更是少见，例如在形式系统中受当前程序验证工具能力影响，有些问题（如程序停机的不可判定性）即便是简单却也无法证明。形式化方法局限性源于其庞大的数学基础体系，首先是软件规约选用的数学工具未必绝对有效，其次是形式化规约在数学意义上的解决不具备唯一性，甚至有些理论在当前工程实践活动中还找不到正确的数学解释，再次不同工程领域、不同应用背景下软件规约存在十分突出的相容性问题。

由于缺少定理证明机制支持，程序功能正确性难以证明，因此，将不同的形式化分析方法组合起来，形成一种混合方法，把形式化证明与实用的测试、容错和运行时检查等技术相结合是形式化方法未来发展的一个研究方向。形式化方法虽然在软件工程活动中有许多优势，但对数学基础要求较高，软件开发团队特别是程序员难以理解，将形式化的表达方式简化，尽最大努力自然语言化，增强软件规约的可读性则会得到更大的发展空间，这也是形式化方法应该努力的一个方向。

4 结 语

形式化方法在软件工程中的应用褒贬不一，支持者认为形式化方法极大地推进了软件开发的进程［21］，而反对者几乎持完全反对的态度［22］，形式化方法40多年的研究与应用取得大量成果说明其并非一无是处，但也应清醒地认识到形式化方法理论研究特别是工业应用中的困难和缺陷。

［1］ 陈火旺，罗朝晖，马庆鸣．程序设计方法学基础［M］．长沙：湖南科学技术出版社，1987．

［2］ 陆汝钤．计算机语言的形式语义［M］．北京：科学出版社，1992．

［3］ 李 未．数理逻辑基本原理与形式推演［M］．北京：科学出版社，2007．

［4］ 陈意云．程序设计语言理论［M］．北京：高等教育出版社，2004．

［5］ 屈延文．形式语义学基础与形式说明［M］．北京：科学出版社，2010．

［6］ HARTMUT E，FERNANDO O，BENJAMIN B，et．al．A component framework for system modeling based on high－level replacement systems［J］．Software and Systems Modeling，2004，3（2）：114－135．

［7］ NICOLAS W，ANDREW S．Towards formally template relational database representations in Z［J］．Abstract State Machines，2010，5 977：363－376．

［8］ FITZGERALD J，LARSEN P G，SAHARA S，et al．VDMTools：Advances in support for formal modeling in VDM［J］．Newsletter of ACM SIGPLAN Notices，2008，43（2）：3－11．

［9］ NARAYAN D，OSCAR T，GERMAN M，et al．Rigorous definition／specification in RAISE specification language of a framework for web services about geographic information systems［A］．IEEE Seventh International Conference on Information Technology［C］．Los Alamitos：IEEE Computer Society，2010．76－81．

［10］ LEE S，SLUIZER S．An executable language for modeling simple behavior［J］．IEEE Trans on SE，1991，17（6）：527－543．

［11］ SEUK B L，WU Xiao－qing，CAO Fei，et al．T－Clipse：An integrated development environment for two－level grammar［A］．ACM Proceedings of the 2003 OOPSLA Workshop on Eclipse Technology eXchange［C］．New York：［s．n．］，2003．89－93．

［12］ KLEYN M K，BROWNE J C．A high level language for specifying graph based languages and their programming environments［J］．IEEE Proc of 15th Intl Conf on SE，1993，20（5）：324－335．

［13］ JOHN V G，JAMES J H，JEANNETTE M W．The larch family of specification language［J］．IEEE Software，1985（1）：24－36．

［14］ MARKUS L．Confluence problems for trace rewriting systems［J］．Information and Computation，2001，170（1）：1－25．

［15］ GWEN S，ANDREA F，ANTONELLA C．Negotiation among web services using LOTOS／CADP［J］．Web Services，Lecture Notes in Computer Science，2004，3 250：198－212．

［16］ AMMAR A．An environment based on rewriting logic for parallel systems formal specification and prototyping［J］．Journal of Systems Architecture，1997，44（2）：79－105．

［17］ LUC J，LUC D，WILLY V P．An algebraic data type specification language and its rapid prototyping environment［A］．ACM Proceedings of the 11th International Conference on Software Engineering［C］．New York：［s．n．］，1989．74－84．

［18］ CONSTANT C，JERON T，MARCHAND H，et al．Integrating formal verification and conformance，testing for reactive systems［J］．IEEE Trans on SE，2007，33（8）：558－574．

［19］ 郑红军，张乃孝．软件开发中的形式化方法［J］．计算机科学（Journal of Computer Science ＆Technology），1997，24（6）：90－96．

［20］ 朱 冰，梅 宏，杨芙清．软件开发过程中的形式化方法［J］．计算机科学（Journal of Computer Science ＆Technology），1995，22（1）：31－36．

［21］ JIM W，PETER G L，JUAN B，et al．Formal methods：Practice and experience［J］．Journal of ACM Computing Surveys，2009，41（4）：1－40．

［22］ BOWEN J P，HINCHEY M G．Ten commandments of formal methods…ten years later［J］．IEEE Journals of Computer，2006，39（1）：40－48．

Application of formal methods to software engineering

MIAO De－cheng1，FENG Li－bo2
（1．College of Mathematics and Information Science，Shaoguan University，Shaoguan Guangdong 512000，China；2．College of Sciences，Hebei University of Science and Technology，Shijiazhuang Hebei 050018，China）

This paper discusses briefly some basic concepts of formal method，and studies mainly its mathematical theory foundation and its application in each stage of software engineering．The paper also analyzes advantages，limitations of formal method as well as their respective reasons in theoretical research and engineering practice，then points out some future developing directions of formal method，and finally makes a brief evaluation of applying formal method to software engineering．

formal method；software specification formal language；software engineering；formal system；specification

TP301

A

1008－1542（2011）06－0575－05

2011－08－29；责任编辑：张 军

广东省科技计划资助项目（2009B050700008）；韶关学院科研资助项目（2010－207－04）

苗德成（1979－），男，黑龙江伊春人，讲师，博士，主要从事软件系统形式化理论、形式语义学方面的研究。