章昱++鄒成武

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

【關鍵詞】軟件形式化 Z語言 設備管理

1 形式化方法介紹

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

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

2 Z語言介紹

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

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

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

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

3 軟件分析

3.1 問題簡介

實驗設備管理軟件通常需要處理以下幾個事務：

（1）設備的使用與使用解除；

（2）從實驗中添加或移除設備；

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

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

（5）查詢設備的最后使用人。

實驗設備管理軟件中有兩類用戶：實驗管理人員和設備使用者。實驗管理人員可以進行以上所有事務的操作，設備使用者可以進行事務（1）的操作以及通過事務（3）（4）（5）查詢設備信息與使用信息。

3.2 定義類型和枚舉類型

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

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

Person：設備管理人員和使用人員集合；

EquIdentify：設備編號集合；

EquType：設備型號集合；

EquBrand： 設備品牌集合；

EquName：設備名稱集合；

Location：設備的位置集合。

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

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

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

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

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

3.4 操作模式

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

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

設備管理人員事務包括設備事務和查詢事務。

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

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

設備添加事務需給定設備編號標志equIdentify？，并提供設備的名稱、品牌、編號。顯然equIdentify？事先并不在實驗中，加入到實驗后馬上就可以使用，因此equ_info和available都應修改。某設備的equIdentify？所對應的設備信息equ_info以新輸入的equName？、equBrand？、equType？和equLocation？更新。圖8顯示了向實驗添加設備模式。

在進行設備移除時，先要確定設備在實驗中，該事務需更改available記錄和last_used記錄以及equ_info。圖9所示的從實驗中移除實驗設備模式描述了該操作。

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

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

用戶事務：

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

引入給定描述集合類型[DESC]與各種信息的對應關系：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ù)設備編號、型號、品牌、名稱、位置查詢設備操作模式：

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

3.5 模式的前置條件

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

3.6 操作完整性和出錯處理

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

4 小結

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

參考文獻

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