章昱++鄒成武

摘 要針對(duì)常規(guī)的軟件描述方法不夠嚴(yán)謹(jǐn)，本文介紹了軟件形式化方法的特點(diǎn)和技術(shù)類(lèi)別，介紹了Z語(yǔ)言的表達(dá)方式及其各自的特點(diǎn)。然后本文使用Z語(yǔ)言分析了實(shí)驗(yàn)設(shè)備管理軟件，給出了部分形式化分析結(jié)果。結(jié)果表明，Z語(yǔ)言能夠?qū)?shù)理邏輯完備用于的描述軟件的功能，有效避免描述的模糊性。

【關(guān)鍵詞】軟件形式化 Z語(yǔ)言 設(shè)備管理

1 形式化方法介紹

軟件工程中形式化方法是一種基于數(shù)學(xué)的研究計(jì)算機(jī)科學(xué)有關(guān)的問(wèn)題的方法，它可應(yīng)用于軟件工程的各個(gè)階段，用形式化方法開(kāi)發(fā)軟件可提高軟件的正確性和可靠性，是可信軟件開(kāi)發(fā)的重要方法。軟件形式化主要通過(guò)形式化、規(guī)范化的數(shù)學(xué)理論，對(duì)軟件建立數(shù)學(xué)模型，研究和提供一種基于數(shù)學(xué)的或形式語(yǔ)義學(xué)的規(guī)格說(shuō)明語(yǔ)言，用這種語(yǔ)言嚴(yán)格地描述所開(kāi)發(fā)的軟件功能，并可通過(guò)推理驗(yàn)證來(lái)保證軟件正確性和可靠性。

形式化方法包含兩種技術(shù)，即形式規(guī)格說(shuō)明技術(shù)和形式驗(yàn)證技術(shù)。這兩種技術(shù)都是基于數(shù)學(xué)基礎(chǔ)，例如集合論、邏輯和代數(shù)理論等。該方法優(yōu)越之處在于它具有嚴(yán)格的數(shù)學(xué)基礎(chǔ)和可描述性，因此，形式規(guī)格說(shuō)明是精確，簡(jiǎn)潔和緊湊的。掌握了形式化方法的軟件分析員、設(shè)計(jì)與編程人員、測(cè)試與驗(yàn)收人員間不會(huì)對(duì)形式規(guī)格說(shuō)明產(chǎn)生誤解，目標(biāo)軟件各方面的特性也能得到確切的說(shuō)明。由于形式化方法基于數(shù)學(xué)理論，能很好的刻畫(huà)數(shù)據(jù)和過(guò)程抽象性，但難以表示客觀世界的動(dòng)態(tài)行為，所以未能在軟件工業(yè)界得到廣泛的應(yīng)用。

2 Z語(yǔ)言介紹

Z語(yǔ)言是一種形式化軟件規(guī)范說(shuō)明語(yǔ)言，其基于一階謂詞邏輯和集合論的規(guī)范，采用嚴(yán)格的數(shù)學(xué)基礎(chǔ)理論，常用于狀態(tài)空間和數(shù)據(jù)結(jié)構(gòu)的描述。在軟件建模過(guò)程中使用Z語(yǔ)言可以描述軟件的需求和功能等形式規(guī)格說(shuō)明問(wèn)題，而形式規(guī)格說(shuō)明方法在軟件工程中起著重要的作用，因而Z語(yǔ)言為也稱(chēng)為軟件工程語(yǔ)言。

Z的表示分為模式語(yǔ)言和數(shù)學(xué)語(yǔ)言，這兩種語(yǔ)言互為補(bǔ)充。

Z的數(shù)學(xué)語(yǔ)言包括一階邏輯、集合論、類(lèi)型、關(guān)系、函數(shù)、序列和包等數(shù)據(jù)概念，使用狀態(tài)模式和操作模式對(duì)目標(biāo)軟件的狀態(tài)和操作進(jìn)行說(shuō)明，使描述具有簡(jiǎn)明和精確的特點(diǎn)。

模式語(yǔ)言包括公理定義、模式、通用式模式等，能夠把一個(gè)規(guī)格說(shuō)明中的共同部分抽取出來(lái)，并區(qū)別類(lèi)似的結(jié)構(gòu)間的差別，使一個(gè)規(guī)格說(shuō)明中已存在的部分可以得到重用，并且使用戶(hù)能夠在軟件開(kāi)發(fā)的每一個(gè)階段共享各種描述。Z的模式語(yǔ)言可以構(gòu)造軟件的文檔的形式規(guī)格說(shuō)明，能使用盡可能簡(jiǎn)單的上下文來(lái)描述規(guī)格說(shuō)明中各個(gè)小部分，然后將其組合起來(lái)構(gòu)成一個(gè)完整的規(guī)格說(shuō)明，使軟件變得更加全面和完整。

3 軟件分析

3.1 問(wèn)題簡(jiǎn)介

實(shí)驗(yàn)設(shè)備管理軟件通常需要處理以下幾個(gè)事務(wù)：

（1）設(shè)備的使用與使用解除；

（2）從實(shí)驗(yàn)中添加或移除設(shè)備；

（3）通過(guò)軟件查詢(xún)?cè)O(shè)備相關(guān)信息：編號(hào)，品牌，型號(hào)，名稱(chēng)，位置等；

（4）查詢(xún)?cè)O(shè)備使用信息，用戶(hù)使用設(shè)備的情況；

（5）查詢(xún)?cè)O(shè)備的最后使用人。

實(shí)驗(yàn)設(shè)備管理軟件中有兩類(lèi)用戶(hù)：實(shí)驗(yàn)管理人員和設(shè)備使用者。實(shí)驗(yàn)管理人員可以進(jìn)行以上所有事務(wù)的操作，設(shè)備使用者可以進(jìn)行事務(wù)（1）的操作以及通過(guò)事務(wù)（3）（4）（5）查詢(xún)?cè)O(shè)備信息與使用信息。

3.2 定義類(lèi)型和枚舉類(lèi)型

規(guī)格說(shuō)明使用了以下給定類(lèi)型：

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

Person：設(shè)備管理人員和使用人員集合；

EquIdentify：設(shè)備編號(hào)集合；

EquType：設(shè)備型號(hào)集合；

EquBrand： 設(shè)備品牌集合；

EquName：設(shè)備名稱(chēng)集合；

Location：設(shè)備的位置集合。

3.3 軟件抽象規(guī)格說(shuō)明

可利用Z語(yǔ)言的模式語(yǔ)言來(lái)描述該軟件的抽象狀態(tài)。將設(shè)備（Equipment），用戶(hù)（User）、實(shí)驗(yàn)信息（Lab）以及用戶(hù)與實(shí)驗(yàn)信息的關(guān)聯(lián)（Rel）等四個(gè)部分用Z語(yǔ)言的模式語(yǔ)言抽象的表示出來(lái)，如圖1所示的設(shè)備信息模式定義了設(shè)備信息：設(shè)備具有編號(hào)、型號(hào)、品牌、名稱(chēng)、位置等屬性。

實(shí)驗(yàn)設(shè)備管理軟件的用戶(hù)Person分為實(shí)驗(yàn)管理人員admin和使用者users兩類(lèi)，可用圖2的用戶(hù)狀態(tài)模式表示。

實(shí)驗(yàn)狀態(tài)模式用于描述設(shè)備使用信息的數(shù)據(jù)庫(kù)狀態(tài)。實(shí)驗(yàn)（Lab）中的所有設(shè)備都可以使用或已在使用，identify表示設(shè)備集合對(duì)應(yīng)的編號(hào)，available表示當(dāng)前實(shí)驗(yàn)中可使用的設(shè)備集合；used表示設(shè)備正在被用戶(hù)使用，該項(xiàng)可以用從設(shè)備到用戶(hù)的部分函數(shù)形式表示；last_used是使用某ID設(shè)備的人員信息的記錄，該項(xiàng)信息可用于事件5的查詢(xún)；equ_info是設(shè)備編號(hào)對(duì)應(yīng)設(shè)備的有關(guān)信息，該項(xiàng)可以用從設(shè)備編號(hào)到設(shè)備的部分函數(shù)形式表示。圖3表示了實(shí)驗(yàn)狀態(tài)模式。

用戶(hù)與實(shí)驗(yàn)關(guān)聯(lián)模式Rel是由User和Lab組成的狀態(tài)模式，圖4表示設(shè)備管理人員admin和設(shè)備使用者users兩類(lèi)用戶(hù)能夠在實(shí)驗(yàn)使用設(shè)備，ran used表示某編號(hào)設(shè)備的當(dāng)前使用者。

3.4 操作模式

用戶(hù)需求中的所有事務(wù)可以分成兩種：設(shè)備管理人員事務(wù)和用戶(hù)事務(wù)。

所有設(shè)備管理人員事務(wù)需要輸入管理人員的id登錄，該操作不影響用戶(hù)軟件。所以首先定義如圖5所示的模式Admin_trans。

設(shè)備管理人員事務(wù)包括設(shè)備事務(wù)和查詢(xún)事務(wù)。

設(shè)備事務(wù)包括設(shè)備使用事務(wù)和使用解除事務(wù)，設(shè)備添加和移除事務(wù)，這些事務(wù)都與設(shè)備編號(hào)有關(guān)，且不影響用戶(hù)軟件。設(shè)備使用事務(wù)中的設(shè)備初始狀態(tài)為可用，用戶(hù)為注冊(cè)用戶(hù)，該事務(wù)更新used記錄和last_used記錄，可用設(shè)備集合中從移除該設(shè)備，available表示更新的可用設(shè)備集合，used表示更新的設(shè)備使用記錄，狀態(tài)變化如圖6所示。endprint

設(shè)備使用解除事務(wù)中的設(shè)備為使用狀態(tài)，解除事務(wù)更新可用設(shè)備集合和已占用設(shè)備集合的狀態(tài)，狀態(tài)變化如圖7所示。

設(shè)備添加事務(wù)需給定設(shè)備編號(hào)標(biāo)志equIdentify？，并提供設(shè)備的名稱(chēng)、品牌、編號(hào)。顯然equIdentify？事先并不在實(shí)驗(yàn)中，加入到實(shí)驗(yàn)后馬上就可以使用，因此equ_info和available都應(yīng)修改。某設(shè)備的equIdentify？所對(duì)應(yīng)的設(shè)備信息equ_info以新輸入的equName？、equBrand？、equType？和equLocation？更新。圖8顯示了向?qū)嶒?yàn)添加設(shè)備模式。

在進(jìn)行設(shè)備移除時(shí)，先要確定設(shè)備在實(shí)驗(yàn)中，該事務(wù)需更改available記錄和last_used記錄以及equ_info。圖9所示的從實(shí)驗(yàn)中移除實(shí)驗(yàn)設(shè)備模式描述了該操作。

描述查詢(xún)事務(wù)可分為查找某位用戶(hù)對(duì)設(shè)備的在用信息和查詢(xún)特定設(shè)備現(xiàn)在被哪位用戶(hù)使用，這些事務(wù)不影響設(shè)備使用及設(shè)備記錄的狀態(tài)。

查詢(xún)事務(wù)包括分為：根據(jù)用戶(hù)信息查詢(xún)指定用戶(hù)的設(shè)備使用記錄，如圖10所示；根據(jù)設(shè)備信息查詢(xún)?cè)O(shè)備使用歷史記錄，如圖11所示。

用戶(hù)事務(wù)：

用戶(hù)事務(wù)在本實(shí)例中指用戶(hù)輸入本人的信息查詢(xún)自己當(dāng)前設(shè)備的使用情況以及通過(guò)輸入設(shè)備相關(guān)信息查詢(xún)某設(shè)備的狀態(tài)信息。設(shè)備管理員和普通用戶(hù)可以通過(guò)設(shè)備的信息描述查詢(xún)?cè)O(shè)備，普通用戶(hù)也可以查詢(xún)本人在用的設(shè)備，這些事務(wù)均不影響設(shè)備信息記錄和使用記錄。為了描述有關(guān)的查詢(xún)操作，定義圖12所示的用戶(hù)事務(wù)模式Users_trans。

引入給定描述集合類(lèi)型[DESC]與各種信息的對(duì)應(yīng)關(guān)系：I_Match，T_Match，B_Match，N_Match，L_match。d？表示根據(jù)用戶(hù)輸入的信息描述。

[DESC]

I_Match：DESC←→EquIdentify

T_Match：DESC←→EquType

B_Match：DESC←→EquBrand

N_Match：DESC←→EquName

L_Match：DESC←→Location

圖13顯示了用戶(hù)根據(jù)設(shè)備編號(hào)、型號(hào)、品牌、名稱(chēng)、位置查詢(xún)?cè)O(shè)備操作模式：

用戶(hù)可以查詢(xún)本人所使用的設(shè)備信息，圖14模式表示了用戶(hù)查詢(xún)自己當(dāng)前設(shè)備使用記錄。Self_used_list的輸入為所包含的模型Users_trans中的用戶(hù)標(biāo)識(shí)符id？，輸出list為id？代表的用戶(hù)使用的設(shè)備集合。

3.5 模式的前置條件

操作模式的前置條件是指某一操作模式能夠成功執(zhí)行的條件，它實(shí)際上是對(duì)操作正確執(zhí)行的條件驗(yàn)證。對(duì)前置條件的規(guī)約說(shuō)明描述了各種事務(wù)操作模式成功執(zhí)行的條件。

3.6 操作完整性和出錯(cuò)處理

操作的完整性描述是由該操作的前置條件成立時(shí)的成功操作和不成立時(shí)的出錯(cuò)處理組成。在管理員或者用戶(hù)正確使用軟件的情況下，軟件將給出一個(gè)操作成功執(zhí)行的報(bào)告；同時(shí)為了描述完整的操作，需要設(shè)計(jì)在不滿(mǎn)足該操作的前置條件時(shí)的處理情況，給出一個(gè)基本的關(guān)于操作模式無(wú)法執(zhí)行或出錯(cuò)描述。

4 小結(jié)

基于形式化方法的軟件建模思想是使用形式化規(guī)約語(yǔ)言精確地描述軟件狀態(tài)及其行為模式，刻畫(huà)了軟件的功能，是提高軟件質(zhì)量和可靠性的一種途徑。實(shí)例展示了Z語(yǔ)言的形式化描述方式。由于Z規(guī)格說(shuō)明包含了大量的數(shù)學(xué)符號(hào)和邏輯符號(hào)操作，因此直接撰寫(xiě)Z規(guī)格說(shuō)明無(wú)疑是一個(gè)挑戰(zhàn)，于是人們嘗試創(chuàng)建了各種Z語(yǔ)言的輔助描述工具，比較著名的有上海大學(xué)開(kāi)發(fā)的ZUsersStudio，Oxford大學(xué)開(kāi)發(fā)的Fuzz、York大學(xué)開(kāi)發(fā)的CADiZ等。將形式化方法和形式化工具結(jié)合使用，將能有效提升形式化方法的應(yīng)用空間。

參考文獻(xiàn)

[1]繆淮扣.軟件形式規(guī)格說(shuō)明語(yǔ)言-Z[M]. 北京：清華大學(xué)出版社，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/.

作者簡(jiǎn)介

章昱（1981-），男，江西師范大學(xué)計(jì)算機(jī)學(xué)院初級(jí)實(shí)驗(yàn)師，博士研究生。

鄒成武（1980-），男，江西師范大學(xué)理電學(xué)院中級(jí)實(shí)驗(yàn)師。

作者單位

1.江西師范大學(xué) 江西省南昌市 330022

2.上海大學(xué) 上海市 200444endprint