实验设备管理软件形式化描述方法研究

章昱++邹成武

摘 要针对常规的软件描述方法不够严谨，本文介绍了软件形式化方法的特点和技术类别，介绍了Z语言的表达方式及其各自的特点。然后本文使用Z语言分析了实验设备管理软件，给出了部分形式化分析结果。结果表明，Z语言能够将数理逻辑完备用于的描述软件的功能，有效避免描述的模糊性。

【关键词】软件形式化 Z语言 设备管理

1 形式化方法介绍

软件工程中形式化方法是一种基于数学的研究计算机科学有关的问题的方法，它可应用于软件工程的各个阶段，用形式化方法开发软件可提高软件的正确性和可靠性，是可信软件开发的重要方法。软件形式化主要通过形式化、规范化的数学理论，对软件建立数学模型，研究和提供一种基于数学的或形式语义学的规格说明语言，用这种语言严格地描述所开发的软件功能，并可通过推理验证来保证软件正确性和可靠性。

形式化方法包含两种技术，即形式规格说明技术和形式验证技术。这两种技术都是基于数学基础，例如集合论、逻辑和代数理论等。该方法优越之处在于它具有严格的数学基础和可描述性，因此，形式规格说明是精确，简洁和紧凑的。掌握了形式化方法的软件分析员、设计与编程人员、测试与验收人员间不会对形式规格说明产生误解，目标软件各方面的特性也能得到确切的说明。由于形式化方法基于数学理论，能很好的刻画数据和过程抽象性，但难以表示客观世界的动态行为，所以未能在软件工业界得到广泛的应用。

2 Z语言介绍

Z语言是一种形式化软件规范说明语言，其基于一阶谓词逻辑和集合论的规范，采用严格的数学基础理论，常用于状态空间和数据结构的描述。在软件建模过程中使用Z语言可以描述软件的需求和功能等形式规格说明问题，而形式规格说明方法在软件工程中起着重要的作用，因而Z语言为也称为软件工程语言。

Z的表示分为模式语言和数学语言，这两种语言互为补充。

Z的数学语言包括一阶逻辑、集合论、类型、关系、函数、序列和包等数据概念，使用状态模式和操作模式对目标软件的状态和操作进行说明，使描述具有简明和精确的特点。

模式语言包括公理定义、模式、通用式模式等，能够把一个规格说明中的共同部分抽取出来，并区别类似的结构间的差别，使一个规格说明中已存在的部分可以得到重用，并且使用户能够在软件开发的每一个阶段共享各种描述。Z的模式语言可以构造软件的文档的形式规格说明，能使用尽可能简单的上下文来描述规格说明中各个小部分，然后将其组合起来构成一个完整的规格说明，使软件变得更加全面和完整。

3 软件分析

3.1 问题简介

实验设备管理软件通常需要处理以下几个事务：

（1）设备的使用与使用解除；

（2）从实验中添加或移除设备；

（3）通过软件查询设备相关信息：编号，品牌，型号，名称，位置等；

（4）查询设备使用信息，用户使用设备的情况；

（5）查询设备的最后使用人。

实验设备管理软件中有两类用户：实验管理人员和设备使用者。实验管理人员可以进行以上所有事务的操作，设备使用者可以进行事务（1）的操作以及通过事务（3）（4）（5）查询设备信息与使用信息。

3.2 定义类型和枚举类型

规格说明使用了以下给定类型：

[Person， EquIdentify， EquType， EquBrand， EquName，Location]

Person：设备管理人员和使用人员集合；

EquIdentify：设备编号集合；

EquType：设备型号集合；

EquBrand： 设备品牌集合；

EquName：设备名称集合；

Location：设备的位置集合。

3.3 软件抽象规格说明

可利用Z语言的模式语言来描述该软件的抽象状态。将设备（Equipment），用户（User）、实验信息（Lab）以及用户与实验信息的关联（Rel）等四个部分用Z语言的模式语言抽象的表示出来，如图1所示的设备信息模式定义了设备信息：设备具有编号、型号、品牌、名称、位置等属性。

实验设备管理软件的用户Person分为实验管理人员admin和使用者users两类，可用图2的用户状态模式表示。

实验状态模式用于描述设备使用信息的数据库状态。实验（Lab）中的所有设备都可以使用或已在使用，identify表示设备集合对应的编号，available表示当前实验中可使用的设备集合；used表示设备正在被用户使用，该项可以用从设备到用户的部分函数形式表示；last_used是使用某ID設备的人员信息的记录，该项信息可用于事件5的查询；equ_info是设备编号对应设备的有关信息，该项可以用从设备编号到设备的部分函数形式表示。图3表示了实验状态模式。

用户与实验关联模式Rel是由User和Lab组成的状态模式，图4表示设备管理人员admin和设备使用者users两类用户能够在实验使用设备，ran used表示某编号设备的当前使用者。

3.4 操作模式

用户需求中的所有事务可以分成两种：设备管理人员事务和用户事务。

所有设备管理人员事务需要输入管理人员的id登录，该操作不影响用户软件。所以首先定义如图5所示的模式Admin_trans。

设备管理人员事务包括设备事务和查询事务。

设备事务包括设备使用事务和使用解除事务，设备添加和移除事务，这些事务都与设备编号有关，且不影响用户软件。设备使用事务中的设备初始状态为可用，用户为注册用户，该事务更新used记录和last_used记录，可用设备集合中从移除该设备，available表示更新的可用设备集合，used表示更新的设备使用记录，状态变化如图6所示。endprint

设备使用解除事务中的设备为使用状态，解除事务更新可用设备集合和已占用设备集合的状态，状态变化如图7所示。

设备添加事务需给定设备编号标志equIdentify？，并提供设备的名称、品牌、编号。显然equIdentify？事先并不在实验中，加入到实验后马上就可以使用，因此equ_info和available都应修改。某设备的equIdentify？所对应的设备信息equ_info以新输入的equName？、equBrand？、equType？和equLocation？更新。图8显示了向实验添加设备模式。

在进行设备移除时，先要确定设备在实验中，该事务需更改available记录和last_used记录以及equ_info。图9所示的从实验中移除实验设备模式描述了该操作。

描述查询事务可分为查找某位用户对设备的在用信息和查询特定设备现在被哪位用户使用，这些事务不影响设备使用及设备记录的状态。

查询事务包括分为：根据用户信息查询指定用户的设备使用记录，如图10所示；根据设备信息查询设备使用历史记录，如图11所示。

用户事务：

用户事务在本实例中指用户输入本人的信息查询自己当前设备的使用情况以及通过输入设备相关信息查询某设备的状态信息。设备管理员和普通用户可以通过设备的信息描述查询设备，普通用户也可以查询本人在用的设备，这些事务均不影响设备信息记录和使用记录。为了描述有关的查询操作，定义图12所示的用户事务模式Users_trans。

引入给定描述集合类型[DESC]与各种信息的对应关系：I_Match，T_Match，B_Match，N_Match，L_match。d？表示根据用户输入的信息描述。

[DESC]

I_Match：DESC←→EquIdentify

T_Match：DESC←→EquType

B_Match：DESC←→EquBrand

N_Match：DESC←→EquName

L_Match：DESC←→Location

图13显示了用户根据设备编号、型号、品牌、名称、位置查询设备操作模式：

用户可以查询本人所使用的设备信息，图14模式表示了用户查询自己当前设备使用记录。Self_used_list的输入为所包含的模型Users_trans中的用户标识符id？，输出list为id？代表的用户使用的设备集合。

3.5 模式的前置条件

操作模式的前置条件是指某一操作模式能够成功执行的条件，它实际上是对操作正确执行的条件验证。对前置条件的规约说明描述了各种事务操作模式成功执行的条件。

3.6 操作完整性和出错处理

操作的完整性描述是由该操作的前置条件成立时的成功操作和不成立时的出错处理组成。在管理员或者用户正确使用软件的情况下，软件将给出一个操作成功执行的报告；同时为了描述完整的操作，需要设计在不满足该操作的前置条件时的处理情况，给出一个基本的关于操作模式无法执行或出错描述。

4 小结

基于形式化方法的软件建模思想是使用形式化规约语言精确地描述软件状态及其行为模式，刻画了软件的功能，是提高软件质量和可靠性的一种途径。实例展示了Z语言的形式化描述方式。由于Z规格说明包含了大量的数学符号和逻辑符号操作，因此直接撰写Z规格说明无疑是一个挑战，于是人们尝试创建了各种Z语言的辅助描述工具，比较著名的有上海大学开发的ZUsersStudio，Oxford大学开发的Fuzz、York大学开发的CADiZ等。将形式化方法和形式化工具结合使用，将能有效提升形式化方法的应用空间。

参考文献

[1]缪淮扣.软件形式规格说明语言-Z[M]. 北京：清华大学出版社，2012.

[2]百度百科.形式化方法[EB/OL].http：//baike.baidu.com/view/1731679.htm.

[3]MiaoHuaikou，Liu Ling，Yu Chuanjiang，Ming Jijun，Lili.Z User Studio：An Integrated Support Tool for Z Specifications.The 8th Asia-Pacific Software Engineering Conference（APSEC 2001），December， 2001，Macau，P437-444.

[4]CADiZHomepage，http：//www.cs.york.ac.uk/hise/cadiz/.

作者簡介

章昱（1981-），男，江西师范大学计算机学院初级实验师，博士研究生。

邹成武（1980-），男，江西师范大学理电学院中级实验师。

作者单位

1.江西师范大学 江西省南昌市 330022

2.上海大学 上海市 200444endprint