基于Z语言的电信服务系统的形式化规格

彭展

0 引言

形式化方法（Formal Method）是一种基于数学的软件开发方法，它能够精确地描述系统的需求和设计，有效地提高软件质量[1]。这种方法被广泛地应用到不同领域的软件开发中，尤其是耗资巨大，对质量要求非常高的软件系统，如电力系统、铁路运输调度系统、航空航天系统等。使用形式化方法开发系统能够带来几大好处:（1）由于形式化方法是基于可靠的数学理论，其严格的语义规则能够消除软件开发过程中的歧义描述。（2）它可以引导我们在开发的过程中使用哪些辅助工具。（3）它能够使开发人员精确地描述系统的各个功能，并且产生一份可靠的文档，即使在测试和维护阶段也能够有很好的支持[2]。总的来说，形式化方法能够大大地提高软件系统的可靠性和准确性，并且能够显著地减少整个软件开发过程的工作量。

形式化方法可具体为形式化规格与验证[3]。形式化规格是通过具有明确数学定义的文法和语义的方法或语言对软件的期望特征或者行为进行的精确、简洁描述,而形式化验证则是基于已建立的形式化规格,对软件的相关特征进行评价的数学分析和证明[3]。

电信服务系统极其复杂，对稳定性要求高，而且不断要进行新功能模块的开发，对系统进行扩展。长期以来，如何提高电信服务系统的稳定性，防止系统内部的错误产生，降低开发成本一直都是软件开发领域研究的课题。在本文中，提出了用形式化方法进行电信服务系统开发的思想，首先用形式化规格语言Z开发出完整的电信服务系统的形式化规格，接着用验证软件Z/EVES对形式化规格的严密性，正确性进行验证。基于Z语言的形式化规格能够解决电信服务系统开发过程中产生的如与实际需求不一致，定义混乱等问题，提高电信服务系统的稳定性和安全性。

1 Z语言的介绍

形式化方法产生了很多种与其相对应的形式规格语言（Formal Specification language），如CADP,LOTOS,mCRL2,RAISE,VDM和Z等，具有代表性的是VDM和Z[4]。在本文中，主要是讨论Z语言（Z Notation）。Z语言是一种基于一阶谓词逻辑和集合论的形式规格说明语言,它采用了严格的数学理论,可以产生简明、精确、无歧义且可证明的规格说明[3]。Z语言的特点是“状态-操作”表示方式[5],这两种表示方式可以统一表示，如图1所示:

图1 Z语言的主要表示方式

SchemaName是模式的名字，Declarations 是模式的声明部分，Predicate是模式的谓词不变式。如果是状态模式,声明部分是状态变量的声明,谓词不变式则是状态变量应满足的条件;如果是操作模式,声明部分是状态模式和输入、输出的声明,谓词不变式是操作应满足的条件和该操作所引起的变化[5]。

2 基于Z语言的电信服务系统的形式化规格

电信服务系统由基本的POTS（模拟电话业务），再加上不断增加的功能模块构成，如电话会议、呼叫转移、来电黑名单、呼叫黑名单、呼叫等待、空闲回拨、留言信箱、信用卡充值等，以使电信服务系统不断得到完善，满足人们日益增长的需求。

本文中，作者已经开发出完整的基于Z语言的电信服务系统的形式化规格，包含了电信服务系统的大部分功能，以下详细介绍电话会议功能的形式化规格，其它功能可以从该功能的形式化规格中得到参考。

2.1 电话会议功能的形式化规格

电话会议功能的目的是让用户通过电话进行会议。组织者添加第三方用户进入电话会议，一般情况下，系统最多只允许6个用户进行会议讨论。当组织者挂断电话时，如果还有参与者在等待电话会议，则系统会自动重拨组织者的电话以作提醒。

2.1.1 电话会议功能所包含的操作的描述

电话会议功能（Conference Call）是对POTS（由于篇幅原因，POST的Z规格在本文中没有列出来）的继承，并且包含了6个操作。这六个操作都是电话会议功能中所涉及的操作，包括添加电话会议功能操作AddFeatureCC、删除电话会议功能操作RemoveFeatureCC、添加用户入电话会议操作AddAdditionalPerson、电话会议进行中操作ConferenceTalk、组织者挂断电话操作OrganigerHangup以及参与者挂断电话操作ParticipantHangup。

2.1.2 变量及变量约束条件模式Variable

在模式Variable中，主要是对变量及其约束条件的设定。电话会议功能包含了5个变量，分别是拥有电话会议功能的用户变量subscriberCC、电话会议进行中变量inconference、参与人数变量peoplecount、等待接入状态变量waiting、通话状态变量talking。在谓词不变式部分，是变量的约束条件。

2.1.3 变量的初始化模式INIT

在初始化模式中，所有变量都定义为空集

2.1.4 添加及删除电话会议操作的模式

AddFeatureCC/RemoveFeatureCC

在系统为用户添加电话会议功能时，这个用户必须处于空闲状态，并且不拥有该功能，删除这个功能时也必须处于空闲状态但必须拥有该功能。

2.1.5 添加用户入电话会议操作的模式AddAdditionalPerson

添加一个用户进入电话会议的过程如下:假设组织者x与y是处于连接状态，x请求添加z进入电话会议，如果系统响应成功，则请求变量request释放x,connected变量添加（x,z）映射以表示x,z处于连接中，接着waiting和talking变量分别添加（x,y）映射和（x,z）映射以表示（x,y）转变为等待状态，而（x,z）转变为对话状态，最后peoplecount变量累加1表示电话会议有一个新加入者。

2.1.6 电话会议进行中操作的模式ConferenceTalk

当电话会议开始后，变量waiting和talking将会删除所有x用户所映射的关系，之后用户x以及所有与用户x相连接的用户都将会添加到变量inconference的集合当中以表示这些用户进入电话会议中。

2.1.7 组织者挂断电话操作的模式OrganigerHangup

当电话组织者进行挂断电话这个操作时，如果仍有一些电话用户在等待电话会议的状态，电信服务系统会重拨该组织者的电话以作提醒。

当电话会议结束，并且组织者挂断电话，则电话会议占用的所有资源都会被释放。接着组织者将会进入到空闲状态，并且人数重设为1。

组织者挂断动作包含了挂断但有其它人等待以及挂断并且电话会议结束这两种情况，所以其模式是由两种对应的子模式组成。

2.1.8 参与人挂断电话操作的模式ParticipantHangup

如果一个参与者在电话会议的过程中挂断电话，则他的呼叫将会断开并且从inconference集合中移除，电话会议的参与人数也会减1，并且该用户也会返回空闲状态。

2.1.9 对POTS中RemoveSubscriber操作的扩展

以下这个动作是对POTS中RemoveSubscriber这个动作的继承，如果系统删除一个用户，电信服务系统仍需要从subscriberCC集合中删除该用户，以使电话会议功能的用户列表中不在出现这个用户的名字，以保证系统的一致性和完整性。

3 形式化规格的验证

在完成系统形式化规格的开发后，为提高形式化规格的严密性和准确性，可以使用一些工具软件对形式化规格进行验证。在这里我们使用的是Z/EVES软件，Z/EVES是一个能够对Z语言的语法和类型进行检查、模式扩展、前置条件计算、证明的工具软件[6]。

在检验的过程中，只需要输入所需要验证的形式化规格，然后执行检查的操作，如果通过了验证，则在软件左边的Syntax和Proof栏目显示‘Y’以表示通过了语法检查和证明，否则显示‘N’并做出相应的提示，在这种情况下，则需要对形式化规格进行修改，直到通过了验证。使用Z/EVES对第3部分的电话会议功能的形式化规格进行验证，如图2所示:

图2 Z/EVES软件对形式化规格进行验证

4 结束语

本文介绍了形式化方法和主流的形式化规格语言Z，接着用Z语言开发电信服务系统的形式化规格，并通过了Z/EVES软件的验证。这套形式化规格对电信服务系统的各个功能进行了准确、规范、无歧义的描述，为提高电信服务系统的可靠性、稳定性打下了坚实的基础，同时也可应用于探测电信服务系统中存在的冲突和缺陷，推动了形式化方法和Z语言在国内电信领域的软件系统的研究和应用。

[1]曾一,周欣,周吉.基于形式化规格说明的UML状态图提取[J].计算机应用研究，2011，2（5）:1767—1769.

[2]Monin J.F.,François J..Understanding formal methods,Written and translated by Jean-François.London:Springer,2003.

[3]闫仕宇.基于Z语言的互联网登陆系统的形式化规格与验证[J].南华大学学报（自然科学版），2009,23（4）:79-83.

[4]姚昱，毋国庆，吴怀广，等.一种软件需求描述语言的设计与实现[J].计算机工程与应用，2009,45（21）:185-188.

[5]何炎祥,宋强,黄谦.从过程描述语言到Z语言[J].小型微型计算机系统,2002,23（9）:1110-1113.

[6]Kallel S.,Kacem M.H.,Jmaiel M..Modeling and enforcing invariants of dynamic software architectures[J],Software and Systems Modeling.2012,11(1):127-149.