摘要 形式化方法对提高软件的正确性、可靠性意义重大，可大幅度减少软件的后期维护费用，但由于设计周期和人员素质的限制，形式化方法未能得到广泛应用。本文介绍了一种新的软件开发方法——轻量级形式化方法，从理论的角度阐述了其成因和基本思想，并从实践的角度给出了轻量级形式化方法在MIS系统分析中的应用实例。
关键字 轻量级形式化方法 需求建模 软件工程
一 引言
随着软件系统复杂度的不断增长，特别是软件在尖端领域的应用，使得开发安全、可靠的软件成为一个非常重要的问题。传统的软件工程方法为软件系统开发制订了一系列的原则、标准及步骤，在不同方面和程度上提高了软件的生产率和质量。但软件系统需求一般采用自然语言和伪代码相结合作为描述语言，由于自然语言存在着二义性和不一致性等缺陷，而伪代码又过分关注实现细节，使得软件系统的描述和构造过程往往潜藏着大量的错误，而这些错误不能仅仅依靠测试来解决。对于那些要求高安全性和高可靠性的行业，如核电站、航空航天、铁路运输等，这个问题显得尤为重要，必须有一种系统的方法来解决。对一般的应用系统，安全性和可靠性也是不容忽视的。
形式化方法作为一种以数学为基础的方法，能够清晰、精确、抽象、简明地规范和验证软件系统及其性质，能够极大地提高软件的安全性和可靠性。许多形式化方法学家研究了形式化方法存在的问题及其发展趋势，指出形式化方法不是万能的，当前的形式化研究和实践水平还远远没有发挥出形式化方法应有的潜力[Hall 1990，Browen 1995]。
在学术界和工程界，对形式化方法的应用仍然存在相当多的困难，如较长的设计周期和较高的人员素质，这使得在目前阶段对整个开发过程进行完全形式化是不可行的。为了使形式化方法更实用、更经济，能够适合不同领域系统开发的要求，形式化研究工作者开始探讨一种新的软件形式化开发方法——轻量级形式化方法（Lightweight Formal Method），着重于在软件开发的某些阶段或某些部分中进行有选择地形式化。本文先对轻量级形式化方法的成因和基本思想作了一定的阐述，再用Radl（Recurrence_based Algorithm Design Language）语言给出了一个MIS系统中部分需求用例的轻量级形式化规范描述。
二 需求分析中的轻量级形式化方法
在形式化方法历史上，由于早期实践多集中在高安全性、高风险性的行业中，为了保证系统的安全和可靠，往往采用一套严格而复杂的过程。这造成了在构造一个完整的形式化系统模型时，需要较长的设计周期和较高的人员素质。实践证明，整个系统的完全形式化在现阶段是极其困难的。
为了使形式化方法更实用、更经济，形式化研究工作者开始探讨轻量级的形式化方法，目的是对资源有限、工期紧张、交流有限、迭代频繁、可靠性要求高的系统，在放弃部分规范验证机制的同时，又能够避免产生关键性缺陷。基本思想是对原有的“重型”形式化方法进行剪裁，将之应用于软件开发的某一阶段或某一部分，从而有效地平衡软件质量和生产率之间的矛盾。现阶段，轻量级形式化方法在航空航天、嵌入式开发、语音通讯、组件开发和其他工业应用中已经有了一些尝试[EasterBrook 1997、1998，Horl 2000、Matsumoto 2002、Murray 2001]。
Daniel Jackson[Jackson 1996]认为轻量级形式化方法侧重于从不同角度观察问题，有选择地应用形式化技术。在规范语言上，传统的形式化方法中往往含有大量的数学符号，片面地把规范语言看作是一般数学表示法，在描述问题时有较浓的数学味，这妨碍了形式化方法在一般系统开发中的应用，轻量级形式化方法主张语言及其辅助工具并重。在测试和证明的关系上，轻量级形式化方法放弃了正确性证明，认为测试的根本问题不在于不能说明系统无错，而在于找不到那些错误，通过穷举状态空间查错的Model Checking在部分领域的成功应用就是较好的例子。轻量级形式化方法还主张对大型系统有选择地采用形式化，再在一致性的基础上把不同的部分规范组合在一起。在具体实施上，也有一些成果出现，如在需求规约的构建中，Steve Easterbrook[EasterBrook 1997]总结了在NASA项目中应用轻量级形式化方法的研究成果，把形成需求规范的过程分成了四个步骤：
(1) 以清晰、精确、无二义的方式描述需求。
(2) 确认和修正规范内部的不一致性。
(3) 根据系统预期行为来测试需求。
(4) 将测试结果反馈给需求的作者。
目前的软件系统常常极为复杂，理解和描述问题的本质也很困难。在需求过程中，往往会潜伏很多不一致和二义性的错误，而错误发现得越晚，修复错误的费用越高[Zhou 2001]。形式化描述具有精确的语义和推理能力，通过无二义性描述、一致性检查、类型检查、有效性检查、行为检测、求精验证等手段，能够提高需求规范的清晰性和精确性，及早发现需求中隐藏的规范和设计缺陷，在系统构建的初期杜绝大部分错误的产生。因此，借鉴轻量级形式化方法的思想，本文对在MIS系统开发的需求建模阶段引入形式化方法作了尝试。
三 轻量级形式化方法在MIS系统中的运用
轻量级形式化方法目前主要的实践领域还停留在高可靠性、高安全性的行业中。作为一种尝试，我们应用轻量级形式化方法，以Radl为描述语言，对一个MIS系统的系统需求进行了规范描述。
3.1 Radl简介
Radl语言是薛锦云教授为实现算法程序形式化和半自动开发的PAR方法而定义的一种基于递归关系的算法设计语言，是PAR方法的重要组成部分。目前PAR方法及其Radl语言主要适用于高可靠（safety-critical）软件部件的开发。[Xue 1998]
Radl语言的初衷是针对计算机程序设计中的算法程序开发而设计的。但作为一种严格定义的形式化语言，Radl同样思考了软件系统设计的各个方面，如：描述软件系统及其行为模式，刻画软件系统的性质，语言之间的应用、比较和转换，软件工具的开发。因此，可以把Radl语言看作是一种广谱的描述语言，它既适用于刻划底层设计，又能够描述描述高层抽象。对Radl语言来说，高层描述实际上就是建立软件系统的数学模型。
所以，我们采用Radl语言作为描述语言对一个MIS系统——省自然科学基金项目管理系统（NSFPM，Natural Science Finance Project Management System）——进行了需求建模。
3.2 功能描述
首先给出NSFPM的问题描述，即需求（Requirement）。
NSFPM是一个MIS系统。首先，项目申请人将申请书电子文档提交到基金项目管理办公室。然后，项目管理员将申请书电子文档中的元数据（记录了申请书中与管理相关的关键信息）导入系统。接着，项目管理员为申请项目选择相应学科领域的专家进行评审。专家返回评审项目的意见，项目管理员根据意见给申请项目评分。最后，项目管理员按照专家总评分对所有项目进行统一评估，评估结果提交到基金项目管理委员会。项目管理员将基金项目管理委员会的最终意见提交到NSFPM系统中。平时，项目管理员还要维护专家的信息。
3.3 系统建模
3.3.1 域建模
首先对NSFPM域建模，即分析（Analysis）。
分析中的第一步是指出系统能被用来做什么，谁将去使用它。所有的用例（Use Case）必须始于角色（Actor），而且有些用例也结束于角色。角色是位于工作系统外部的人或其他系统。[Cockburn 2001]
本系统参与的角色包括项目管理员、项目申请者、专家。项目申请者不直接和系统交互，提交申请项目的功能由项目管理员代为执行。专家也不直接和系统交互，为申请项目评分的功能由项目管理员代为执行。
因此，本系统以管理为核心工作，以项目管理员为主角色，得到简明用例：
项目管理（Project Management）包括导入项目、编辑项目（选定审查专家、录入专家评分、变更项目状态）、评估项目。
项目维护（Project Maintenance）包括删除项目、检索项目、查看项目、浏览文档、修改文档。
专家维护（Expert Maintenance）包括注册专家、注销专家、修改专家、查看专家、增加专家、删除专家。
NSFPM系统分析的结果表现在UML用例图中，如图1所示。
图1：NSFPM系统的角色和用例。
3.3.2 系统建模
然后，从域建模转移到系统建模。以下是系统关键类模型的简明UML类图。需要说明的是，为了描述问题方便，在这里我们没有采用实现中的get()方法来保证数据隐藏，而是将类的属性设为公有属性，以便直接访问。
图2：NSFPM系统的简明类图。
根据以上对用例图和类图的讨论，我们引入以下缩略语，对同一类型采用相同的描述方法和变量（如果需要，可以用x1、x2……），以简化模型的描述。
类型
变量
Project（项目）
P
ProjectBase（项目库）
Pb
Expert（专家）
E
ExpertBasr（专家库）
eb
Edoc（电子申请书）
ed
Project_Expert(项目和专家的关联)
pe
3.4 形式化描述
我们对需求模型中的状态定义和行为规范进行形式化定义。以下是部分例子。
3.4.1 形式化的状态定义
对每一个带有状态模型的类型，我们必须能够区分类型不同属性的状态（实践中，状态定义的过程引导我们细化状态模型，特别是类似属性这样的细节）。本文以项目（Project）状态中的“申请”（onApplying）和“在评”（onJudging）两个状态作为例子进行形式化定义。
申请
//项目处于申请状态，意味着//
p.status = onApplying implies
BEGIN
//存在项目代码//
p.pid ≠ null
//申请人在研项目不得超过两项//
and ∑(p1: p1∈pb ∧ p1.aid=p.aid ∧ p1.status =onStudying :1) ≤ 2
//申请人没有应结题而未结题的项目//
and p1∈pb ∧ p1.aid=p.aid ∧ p1.status=onStudying ∧ p1.whenFinished < now()
END
在评
//项目处于在研状态，意味着//
p.status = onStudying implies
BEGIN
//存在项目评分//
p.score ≠ null
//项目评分在本学科排名在前十位//
and ∑(p1: p1∈pb ∧ p1.sid=p.sid ∧p1.score >p.score :1) < 10
END
3.4.2 形式化的行为规范
以下是一些行为规范。每个行为有一个标识符、前置断言和后置断言。本文以NSFPM中的“导入项目”（importProject）和“选择专家”（selectExpert）两个用例作为例子进行形式化定义。
导入项目
//将电子申请书导入项目//
NSFPM::ImportProject(ed: Edoc)
AQ:
//项目库中没有与电子申请书内容相同的项目//
ed.key=p.key ∧ ～pb.search(p)
AR:
//生成项目代码//
p.pid ≠ null
//项目状态为“申请”或“淘汰”//
and p.status=onApplying ∨ p.status=onLost
选择专家
//为项目选择评审专家//
NSFPM::selectExpert(p:Project, e:Expert)
AQ:
//项目存在，项目状态为“申请”//
pb.search(p) ∧ p.status = onApplying
//专家存在，专家状态为“注册”//
and eb.search(e) ∧ e.status = onLogin
//项目学科和专家学科一致//
and p.sid = e.sid
//该项目已有专家小于5//
and pe.pid=p.pid ∧ pe.getNumberofExpert()＜5
//辅助变量X，记录当前项目所属专家数//
and AUX X = pe.getNumberofExpert()
AR:
//项目所属专家增1//
pe.getNumberofExpert() = X+1
//项目专家关联中出现增加的专家//
and pe.search(e.id)
以上定义的规范作为对程序状态和行为的描述，正应用在我们的NSPFM系统开发中，用来判断系统是否运行正常。这进一步保证了系统的清晰性、正确性和可靠性。
四 总结及讨论
在对上述MIS系统构造形式化规范的过程中，我们着眼于系统开发的关键步骤——需求分析，将形式化方法应用于需求建模，而不追求完全形式化，以达到轻量化的目标，同时保证了系统的清晰性、正确性和可靠性，并降低了系统的开发成本。
系统开发的各个阶段应用轻量级形式化方法仍有待进一步研究。在对需求建模作了形式规范后，如何在后续的阶段中更有效地演化和精化已有的规范就成为进一步研究的目标。
最后，用Dianel Jackson的一句话作结束语。比起传统的形式化方法，轻量级形式化方法在表达能力和应用领域上都还有差距，就象医疗上使用的激光，比起普通灯管来，它的能量更弱，覆盖面更小，但其使用效率更高，效果更显著。
主要参考文献
[Beck 2001] Kent Beck。解析极限编程——拥抱变化。唐东铭译。人民邮电出版社。
[Boggs 2002] Wendy Boggs & Michael Boggs。Mastering UML with Rational Rose 2002。
邱仲潘译。电子工业出版社。
[Boiten 1992] E.A.Boiten et al。How to Produce Correct Software — An Introduce
to Formal Specification and Program Development by Transformation。The
Computer Journal，Vol.35，No.6。
[Brooks 1995] Frederick Brooks。The Mythical Man-Month。汪颖译。Addison Wesley 1995。
[Browen 1995] Jonathan P. Browen。Seven More Myths of Formal Methods。IEEE Computer，
July。
[Cockburn 2001] Alistair Cockburn。编写有效用例。王雷、张莉译。机械工业出版社。
[Craigen 1995] D. Craigen et al.。Formal Methods Reality Check: Industrial Usage。IEEE
Trans. Soft. Engi.，Vol.21，No.2。
[EasterBrook 1997] Steve EasterBrook et al。Formal Methods for Verification and Validation of
Partial Specifications。NASA-IVV，No.10。
[EasterBrook 1998] Steve EasterBrook et al。Experiences Using LightWeight Formal Methods for
Requirement Modeling。IEEE Trans. Soft. Engi.，Vol.24，No.1。
[Fowler 2000] Martin Fowler、Kendall Scott。UML精粹。徐家福译。Addison Wesley 2000。
[Hall 1990] J.A.Hall。Seven Myths of Formal Methods。IEEE Software，September。
[Horl 2000] Johann Horl et al。Validating Voice Communication Requirements Using
Lightweight Formal Methods。IEEE Software，Vol.17，No.3。
[Jackson 1996] Daniel Jackson & Jeannette Wing。Lightweight Formal Methods。
[Jacobson 2000] Ivar Jacobson et al。统一软件开发方法。周伯生等译。
[Mitchell] Rechard Mitchell。根据合同进行分析——录像店案例研究。Zhen lei译。
[Matsumoto 2002] Michihiro Matsumoto。Lightweight Formal Methods for Component-based
Software Development。
[Morgan 1998] Carroll Morgan。Programming from Specification。裘宗燕译。机械工业出
版社。
[Murray 2001] Leesa Murray。Lightweight Formal Methods for Embedded Software。
[Rational 2001] Rational。Rational Unified Process 2000。Rational Software Corporation 2001。
[Sobel 2002] Kelley Sobel et al。Formal Methods Application: An Empirical Tale of
Software Development。IEEE Trans. Soft. Engi.，Vol.28，No32。
[Wampler 2000] Bruce E. Wampler。Java与UML面向对象程序设计。王海鹏译。人民邮电出版社。
[Xu 2002] 徐正文。如何调研和分析系统需求。中国计算机报，8月。
[Xue 1998] Xue Jinyun(薛锦云)。Formal Derivationof Graph Algorithmic Programs
Using Partition-and-Recur。J.of Comput. Sci.&Technol , Vol.13 No.6.
[Zheng 2002] 郑红军、张乃孝。软件开发中的形式化方法。
[Zhou 2001] 周子英。现代软件工程（中）。科学出版社，2001。
本文地址：http://com.8s8s.com/it/it37524.htm