章昱++鄒成武

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

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

1 形式化方法介紹

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

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

2 Z語言介紹

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

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

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

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

3 軟件分析

3.1 問題簡介

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

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

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

（3）通過軟件查詢設(shè)備相關(guān)信息：編號，品牌，型號，名稱，位置等；

（4）查詢設(shè)備使用信息，用戶使用設(shè)備的情況；

（5）查詢設(shè)備的最后使用人。

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

3.2 定義類型和枚舉類型

規(guī)格說明使用了以下給定類型：

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

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

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

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

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

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

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

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

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

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

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

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

3.4 操作模式

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

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

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

設(shè)備事務(wù)包括設(shè)備使用事務(wù)和使用解除事務(wù)，設(shè)備添加和移除事務(wù)，這些事務(wù)都與設(shè)備編號有關(guān)，且不影響用戶軟件。設(shè)備使用事務(wù)中的設(shè)備初始狀態(tài)為可用，用戶為注冊用戶，該事務(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è)備編號標(biāo)志equIdentify？，并提供設(shè)備的名稱、品牌、編號。顯然equIdentify？事先并不在實(shí)驗(yàn)中，加入到實(shí)驗(yàn)后馬上就可以使用，因此equ_info和available都應(yīng)修改。某設(shè)備的equIdentify？所對應(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è)備模式描述了該操作。

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

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

用戶事務(wù)：

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

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

[DESC]

I_Match：DESC←→EquIdentify

T_Match：DESC←→EquType

B_Match：DESC←→EquBrand

N_Match：DESC←→EquName

L_Match：DESC←→Location

圖13顯示了用戶根據(jù)設(shè)備編號、型號、品牌、名稱、位置查詢設(shè)備操作模式：

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

3.5 模式的前置條件

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

3.6 操作完整性和出錯處理

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

4 小結(jié)

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

參考文獻(xiàn)

[1]繆淮扣.軟件形式規(guī)格說明語言-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/.

作者簡介

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

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

作者單位

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

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