从类树形流程图到Z语言的形式化规格

彭展

从类树形流程图到Z语言的形式化规格

彭展

在软件工程中，使用Z语言形式化规格可以大大提高软件开发质量，提高稳定性，降低开发成本，但要开发出高质量的形式化规格并通过验证，却需要损耗较多的时间和精力。为使软件开发人员能够较快地并且高质量地开发出基于Z语言的形式化规格，提出一种简明的类树形流程图，并以电信服务系统中的呼叫转移功能模块为例子，详细描述如何把类树形流程图应用到Z语言的形式化规格开发当中，以期为开发人员带来便利，节省开发时间，提高形式化规格的质量。

类树形流程图，Z语言，电信系统，形式化规格

0 引言

为了提高软件的开发质量，一种较为普遍的方法是采用形式化方法。形式化方法基于严格的数学理论, 能产生精确、无二义性的形式化规格说明, 对提高软件的可靠性有着非常显著的作用, 是当今软件开发中最为严谨的方法[1]。基于形式化方法的语言称为形式化规格语言，如VDM，LOTOS和Z等。Z语言[2]是一种非常有效的形式描述语言，它以一阶谓词逻辑和集合论作为形式语义基础，借助于模式( Schema) 来表达系统结构[3]。模式主要由两部分组成:一是声明,负责定义各种变量的类型;另一部分则为谓词表达式.后者对于规格说明的功能描述是较重要的部分,通过这些谓词表达式可以推理出所描述软件的所有状态行为[4]。

在使用Z语言开发形式化规格的过程中，需要考虑每个对象状态的变换，不同的操作会

使对象产生许多不同的状态，研究与开发人员需要对系统中所涉及的对象和各种操作，以及操作所带来的各种状态变化进行详细的分析，所以需要花费大量的时间，并且容易产生错误，导致所开发出的Z语言的形式化规格缺乏严密性和一致性，并且不能通过相关软件的测试，失去了开发形式化规格的意义。

在本文中，作者提出了使用类树形流程图的方法来分析研究的对象和外部的事件给对象带来的状态变化、产生的结果，以方便研究人员能够快速地开发出高质量的形式化规格。为了更好地阐述从类树形流程图到形式化规格的开发过程，本文以电信服务系统中的呼叫转移功能为例子，首先，对忙时呼叫转移和一直呼叫这两个功能模块进行描述，接着描绘出这两个功能模块的类树形流程图，然后，分析如何得出Z语言的形式化规格，最后是对使用该方法的效率的讨论。

1 功能描述

呼叫转移是电信服务系统中一个常见功能，具体可分为忙时呼叫转移模块和一直呼叫转移模块。忙时呼叫转移是指当用户x呼叫用户y, 用户y处于繁忙状态并且已设置呼叫转移到z，则系统会自动把呼叫转移给用户z。一直呼叫转移是指当用户x 呼叫用户y,用户y已设置呼叫转移到z,则无论y处于何种状态，呼叫都会转移给用户z。两种呼叫转移的过程如图1所示：

图1，忙时呼叫转移和一直呼叫转移的示意图

2 类树形流程图

为了能够更加准确、详细地对功能模块进行描述，作者提出了类树形流程图的概念。在该种流程图中表示流程开始表示流程结束表示流程的中间节点，图中还包含了功能模块中所涉及的动作、事件和状态变化, 整个流程图以树形结构展开，因此称为类树形流程图。

由第1部分的功能描述，我们可以描绘出忙时呼叫转移的类树形流程图如图2所示：

图2，忙时呼叫转移的类树形流程图

在图2中，lift the phone（x）表示用户x提起电话，Dial（x）用户x拨打电话，hang up（x）表示用户x挂断电话，request（x，y）表示用户x请求与y通话，busy表示用户处于繁忙状态，free表示用户处于空闲状态，connected（x，y）表示用户x和y之间已建立连接，talking（x，y）表示用户x, y处于对话状态，disconnect（x，y）表示用户x与y断开连接。

从该类树形流程图中，由开始状态到结束状态，可以得到9条不同的链路，这9条不同的链路表示在忙时呼叫转移这个功能模块中，用户x, y, z产生9种不同的组合，从而使电信服务系统产生9种不同的状态变化过程。

同理，我们也可以得出一直呼叫转移这个功能模块的类树形流程图如图3所示：

图3，一直呼叫转移的类树形流程图

在图3中，由流程开始到流程结束，可以产生6条不同的链路，因此，电信服务系统产生6种不同的状态变化过程。

3 由类树形流程图到Z语言的形式化规格

类树形流程图用图形把功能模块所涉及的事件、动作和状态变化进行详细的描述，并且不会产生歧义和不一致的地方。这既能够让研究与开发人员详细地掌握功能模块的每个细节，为开发形式化规格建立了坚实的基础，又符合了形式化语言严谨、一致、无歧义的要求。

开发人员使用类树形流程图开发Z语言的形式化规格的算法如下：

（1）根据类树形流程图中出现的事件参与者设定模式（schema）声明部分的变量和变量类型。

（2）由类树形流程图中出现的状态变化情况设定相应的状态变量。

（3）根据流程图中较长的、有意义的路径设定主要操作，并对操作的模式命名。

（4）根据操作的路径所涉及的事件和状态变化过程，用Z语言的语法和表达式进行代替和转换，则可以生成模式的谓词表达式部分。经过这四步的算法，可以得出功能模块主要操作的形式化规格。

3.1 忙时呼叫转移功能模块的形式化规格

由忙时呼叫转移的类树形流程图(图2)和上述的算法，忙时呼叫转移的形式化规格产生过程如下：

（1）类树形流程图中出现了电话用户x、y、z，因此定义PHONE为设定类型，代表所有的电话用户的集合，x、y、z均为PHONE类型中的一个变量。

（2）类树形流程图中出现了4种状态，request表示请求连接状态，connected表示已连接状态,free表示用户空闲状态，busy表示用户繁忙状态，因此在形式化规格模式的声明部分也相应地定义4个系统的状态变量：request，connected，free和 busy。

（3）在类树形流程图的9条链路中，我们选取最长的、有意义的两条链路: ○1用户x, y 进行对话的链路talking( x, y )。○2用户x, z 实现通话的链路talking(x ,z)。这两条链路描述的是忙时呼叫转移模块中两个主要的操作: 拨打电话操作，和忙时转移操作。由于拨打电话操作是电信服务系统的基本操作，忙时转移操作是忙时呼叫转移功能模块中的特有操作，因此在开发Z语言的形式化规格的时候，可以先开发出拨打电话这个基本操作的模式Dialx, 再继承模式Dialx开发出忙时转移操作的模式这也符合了Object-Z[5]的继承思想。

（4）Z语言的形式化规格是用模式表示，模式分为声明部分和谓词表达式部分。由上述算法的（1）、（2）步可得出模式的声明部分，再根据talking（x，y）链路的状态变化过程，用Z语言进行转换，可得出模式的谓词表达式部分。因此，拨打电话操作Dialx的Z语言形式化规格如图4所示：

图4，拨打电话操作的形式化规格

该形式化规格的谓词表达式部分描述了拨打电话这个操作的过程：用户x最初处于空闲状态，接着x请求与用户y连接，y 也是空闲状态，因此x 和y建立连接。同时用户x 和y 都由空闲状态free 转到繁忙状态busy。

在链路talking（x，y）中，描述的是忙时转移这个核心操作，由Object-Z的继承的思想，我们可以把忙时转移操作对拨打电话操作Dialx进行继承，在开发忙时转移操作的形式化规格时，只需要开发与Dialx不同的部分，相同的事件和状态变化可以进行继承，忙时转移操作的Z语言形式化规格如图5所示：表示这个操作是对拨打电话操作Dialx的继承，在模式的谓词表达式部分，表示存在用户z满足下述的表达式，用户x请求与用户y通话，用户y处于繁忙状态并且把呼叫转移给z，则这个请求转到z。

图5 忙时转移操作的形式化规格

3.2 一直呼叫转移功能模块的形式化规格

同理，根据一直呼叫转移的类树形流程图（图3）和上述算法，一直呼叫转移的形式化规格产生过程如下：

（1）、（2）步与上述忙时呼叫转移功能的过程一致。

（3）从图中选取最长的链路talking(x , y)，该链路描述的是一直呼叫转移这个功能模块最主要的操作一直呼叫转移，我们可以设定该操作的模式名为CallForwardAlways。

（4）由算法的（1）、（2）步，我们可以得出模式的声明部分，接着把talking（x，y）链路中所有的状态变化过程用Z语言进行描述，即可以描述出一直呼叫转移这个操作的形式化规格如图6所示：

图6，一直呼叫转移操作的形式化规格

4 开发过程的效率性讨论

类树形流程图的主要目标是提高Z语言的形式化规格的开发效率。由于类树形图的组成相对简单，主要元素包含了开始、结束、中间节点和流程线，具有简明易用的特点，因此，研发人员在使用类树形流程图的时候，不需要描述过于复杂的图形，这样，可以大大节省时间和精力，同时，类树形流程图也具有明确、无歧义的特点，符合了形式化规格严谨性和一致性的要求。为了测试用类树形流程图所开发的形式化规格的质量，作者用常用的形式化规格验证软件Z/EVES软件对进行了验证，Z/EVES是一个带有定理证明器的Z 支持工具, 具有交互式证明功能, 可以检查、分析Z形式规格说明[6]，经过分析与证明，由类树形流程图方法所开发的形式化规格具备很好的质量和可靠性。

5 总结

本文提出类树形流程图的概念，并且详细的讲述了怎样使用类树形流程图开发出基于Z语言的形式化规格。文章首先对电信系统中的两个功能模块进行描述和分析，接着在这基础上描绘出该功能模块的类树形流程图，然后依照转换算法，把类树形流程图转换成Z语言的形式化规格。最后，还对类树形流程图开发方法的效率性进行讨论。总的来说，类树形流程图简明、易用，所开发的形式化规格具有很好的质量和可靠性，期望对软件工程领域的研发人员带来帮助，提高软件开发的效率和质量。

[1] 吴帅，缪丽君. 形式化方法与可视化模型的结合及其应用[J]. 计算机与现代化, 2011(3):44-46,56.

[2] 缪淮扣, 陈怡海．软件形式规格说明语言—Z[M]．清华大学出版社，2012.

[3] 闫仕宇，胡义香，蒋辉等. 形式化方法在核事故评价系统中的应用[J]. 南华大学学报( 自然科学版), 2012，26(3):73-78.

[4] 许庆国,缪淮扣,曹晓夏等. Object-Z 规格说明测试用例的自动生成器[J]. 软件学报,2011, 22(6)：1155-1168.

[5] Graeme Smith. The Object-Z Specification Language [M].Springer US, 2000.

[6] 文志诚，贾峰，胡纯蓉.一个Object-Z规格说明的证明责任产生器[J]. 计算机应用与软件，2010.27（5）：34-37.

From the Tree Liked Flowchart to Formal Specification Based on Z Language

Peng Zhan
(Department of Experimental Teaching, Guangdong University of Petrochemical Technology, Maoming525000, China)

In software engineering, the use of formal specification language Z can greatly improve the quality of software development, improving stability, and reducing development costs.But to develop high-quality formal specification and through the validation, it needs more time and energy. In order to enable software developers to develop high quality formal specification which based on Z language quickly, it presents a concise tree liked flowchart and give the telecommunications services system call forwarding function module as an example, describing how the tree liked flowchart applied to the development of formal specification using Z language, hoping that it could bring convenience for developers, saving development time and improve the quality of formal specifications.

Tree Liked Flowchart; Z Language; Telecommunication System; Formal Specification

TP311

A

1007-757X(2014)01-0028-03

2013.12.18)

广东石油化工学院青年自然科学项目（513023）

彭展，(1985- )，男，广东茂名人，广东石油化工学院，硕士，研究方向：软件开发形式化方法，广东茂名，525000