彭展

從類樹形流程圖到Z語言的形式化規(guī)格

彭展

在軟件工程中，使用Z語言形式化規(guī)格可以大大提高軟件開發(fā)質(zhì)量，提高穩(wěn)定性，降低開發(fā)成本，但要開發(fā)出高質(zhì)量的形式化規(guī)格并通過驗證，卻需要損耗較多的時間和精力。為使軟件開發(fā)人員能夠較快地并且高質(zhì)量地開發(fā)出基于Z語言的形式化規(guī)格，提出一種簡明的類樹形流程圖，并以電信服務(wù)系統(tǒng)中的呼叫轉(zhuǎn)移功能模塊為例子，詳細描述如何把類樹形流程圖應用到Z語言的形式化規(guī)格開發(fā)當中，以期為開發(fā)人員帶來便利，節(jié)省開發(fā)時間，提高形式化規(guī)格的質(zhì)量。

類樹形流程圖，Z語言，電信系統(tǒng)，形式化規(guī)格

0 引言

為了提高軟件的開發(fā)質(zhì)量，一種較為普遍的方法是采用形式化方法。形式化方法基于嚴格的數(shù)學理論, 能產(chǎn)生精確、無二義性的形式化規(guī)格說明, 對提高軟件的可靠性有著非常顯著的作用, 是當今軟件開發(fā)中最為嚴謹?shù)姆椒╗1]?；谛问交椒ǖ恼Z言稱為形式化規(guī)格語言，如VDM，LOTOS和Z等。Z語言[2]是一種非常有效的形式描述語言，它以一階謂詞邏輯和集合論作為形式語義基礎(chǔ)，借助于模式( Schema) 來表達系統(tǒng)結(jié)構(gòu)[3]。模式主要由兩部分組成:一是聲明,負責定義各種變量的類型;另一部分則為謂詞表達式.后者對于規(guī)格說明的功能描述是較重要的部分,通過這些謂詞表達式可以推理出所描述軟件的所有狀態(tài)行為[4]。

在使用Z語言開發(fā)形式化規(guī)格的過程中，需要考慮每個對象狀態(tài)的變換，不同的操作會

使對象產(chǎn)生許多不同的狀態(tài)，研究與開發(fā)人員需要對系統(tǒng)中所涉及的對象和各種操作，以及操作所帶來的各種狀態(tài)變化進行詳細的分析，所以需要花費大量的時間，并且容易產(chǎn)生錯誤，導致所開發(fā)出的Z語言的形式化規(guī)格缺乏嚴密性和一致性，并且不能通過相關(guān)軟件的測試，失去了開發(fā)形式化規(guī)格的意義。

在本文中，作者提出了使用類樹形流程圖的方法來分析研究的對象和外部的事件給對象帶來的狀態(tài)變化、產(chǎn)生的結(jié)果，以方便研究人員能夠快速地開發(fā)出高質(zhì)量的形式化規(guī)格。為了更好地闡述從類樹形流程圖到形式化規(guī)格的開發(fā)過程，本文以電信服務(wù)系統(tǒng)中的呼叫轉(zhuǎn)移功能為例子，首先，對忙時呼叫轉(zhuǎn)移和一直呼叫這兩個功能模塊進行描述，接著描繪出這兩個功能模塊的類樹形流程圖，然后，分析如何得出Z語言的形式化規(guī)格，最后是對使用該方法的效率的討論。

1 功能描述

呼叫轉(zhuǎn)移是電信服務(wù)系統(tǒng)中一個常見功能，具體可分為忙時呼叫轉(zhuǎn)移模塊和一直呼叫轉(zhuǎn)移模塊。忙時呼叫轉(zhuǎn)移是指當用戶x呼叫用戶y, 用戶y處于繁忙狀態(tài)并且已設(shè)置呼叫轉(zhuǎn)移到z，則系統(tǒng)會自動把呼叫轉(zhuǎn)移給用戶z。一直呼叫轉(zhuǎn)移是指當用戶x 呼叫用戶y,用戶y已設(shè)置呼叫轉(zhuǎn)移到z,則無論y處于何種狀態(tài)，呼叫都會轉(zhuǎn)移給用戶z。兩種呼叫轉(zhuǎn)移的過程如圖1所示：

圖1，忙時呼叫轉(zhuǎn)移和一直呼叫轉(zhuǎn)移的示意圖

2 類樹形流程圖

為了能夠更加準確、詳細地對功能模塊進行描述，作者提出了類樹形流程圖的概念。在該種流程圖中表示流程開始表示流程結(jié)束表示流程的中間節(jié)點，圖中還包含了功能模塊中所涉及的動作、事件和狀態(tài)變化, 整個流程圖以樹形結(jié)構(gòu)展開，因此稱為類樹形流程圖。

由第1部分的功能描述，我們可以描繪出忙時呼叫轉(zhuǎn)移的類樹形流程圖如圖2所示：

圖2，忙時呼叫轉(zhuǎn)移的類樹形流程圖

在圖2中，lift the phone（x）表示用戶x提起電話，Dial（x）用戶x撥打電話，hang up（x）表示用戶x掛斷電話，request（x，y）表示用戶x請求與y通話，busy表示用戶處于繁忙狀態(tài)，free表示用戶處于空閑狀態(tài)，connected（x，y）表示用戶x和y之間已建立連接，talking（x，y）表示用戶x, y處于對話狀態(tài)，disconnect（x，y）表示用戶x與y斷開連接。

從該類樹形流程圖中，由開始狀態(tài)到結(jié)束狀態(tài)，可以得到9條不同的鏈路，這9條不同的鏈路表示在忙時呼叫轉(zhuǎn)移這個功能模塊中，用戶x, y, z產(chǎn)生9種不同的組合，從而使電信服務(wù)系統(tǒng)產(chǎn)生9種不同的狀態(tài)變化過程。

同理，我們也可以得出一直呼叫轉(zhuǎn)移這個功能模塊的類樹形流程圖如圖3所示：

圖3，一直呼叫轉(zhuǎn)移的類樹形流程圖

在圖3中，由流程開始到流程結(jié)束，可以產(chǎn)生6條不同的鏈路，因此，電信服務(wù)系統(tǒng)產(chǎn)生6種不同的狀態(tài)變化過程。

3 由類樹形流程圖到Z語言的形式化規(guī)格

類樹形流程圖用圖形把功能模塊所涉及的事件、動作和狀態(tài)變化進行詳細的描述，并且不會產(chǎn)生歧義和不一致的地方。這既能夠讓研究與開發(fā)人員詳細地掌握功能模塊的每個細節(jié)，為開發(fā)形式化規(guī)格建立了堅實的基礎(chǔ)，又符合了形式化語言嚴謹、一致、無歧義的要求。

開發(fā)人員使用類樹形流程圖開發(fā)Z語言的形式化規(guī)格的算法如下：

（1）根據(jù)類樹形流程圖中出現(xiàn)的事件參與者設(shè)定模式（schema）聲明部分的變量和變量類型。

（2）由類樹形流程圖中出現(xiàn)的狀態(tài)變化情況設(shè)定相應的狀態(tài)變量。

（3）根據(jù)流程圖中較長的、有意義的路徑設(shè)定主要操作，并對操作的模式命名。

（4）根據(jù)操作的路徑所涉及的事件和狀態(tài)變化過程，用Z語言的語法和表達式進行代替和轉(zhuǎn)換，則可以生成模式的謂詞表達式部分。經(jīng)過這四步的算法，可以得出功能模塊主要操作的形式化規(guī)格。

3.1 忙時呼叫轉(zhuǎn)移功能模塊的形式化規(guī)格

由忙時呼叫轉(zhuǎn)移的類樹形流程圖(圖2)和上述的算法，忙時呼叫轉(zhuǎn)移的形式化規(guī)格產(chǎn)生過程如下：

（1）類樹形流程圖中出現(xiàn)了電話用戶x、y、z，因此定義PHONE為設(shè)定類型，代表所有的電話用戶的集合，x、y、z均為PHONE類型中的一個變量。

（2）類樹形流程圖中出現(xiàn)了4種狀態(tài)，request表示請求連接狀態(tài)，connected表示已連接狀態(tài),free表示用戶空閑狀態(tài)，busy表示用戶繁忙狀態(tài)，因此在形式化規(guī)格模式的聲明部分也相應地定義4個系統(tǒng)的狀態(tài)變量：request，connected，free和 busy。

（3）在類樹形流程圖的9條鏈路中，我們選取最長的、有意義的兩條鏈路: ○1用戶x, y 進行對話的鏈路talking( x, y )?！?用戶x, z 實現(xiàn)通話的鏈路talking(x ,z)。這兩條鏈路描述的是忙時呼叫轉(zhuǎn)移模塊中兩個主要的操作: 撥打電話操作，和忙時轉(zhuǎn)移操作。由于撥打電話操作是電信服務(wù)系統(tǒng)的基本操作，忙時轉(zhuǎn)移操作是忙時呼叫轉(zhuǎn)移功能模塊中的特有操作，因此在開發(fā)Z語言的形式化規(guī)格的時候，可以先開發(fā)出撥打電話這個基本操作的模式Dialx, 再繼承模式Dialx開發(fā)出忙時轉(zhuǎn)移操作的模式這也符合了Object-Z[5]的繼承思想。

（4）Z語言的形式化規(guī)格是用模式表示，模式分為聲明部分和謂詞表達式部分。由上述算法的（1）、（2）步可得出模式的聲明部分，再根據(jù)talking（x，y）鏈路的狀態(tài)變化過程，用Z語言進行轉(zhuǎn)換，可得出模式的謂詞表達式部分。因此，撥打電話操作Dialx的Z語言形式化規(guī)格如圖4所示：

圖4，撥打電話操作的形式化規(guī)格

該形式化規(guī)格的謂詞表達式部分描述了撥打電話這個操作的過程：用戶x最初處于空閑狀態(tài)，接著x請求與用戶y連接，y 也是空閑狀態(tài)，因此x 和y建立連接。同時用戶x 和y 都由空閑狀態(tài)free 轉(zhuǎn)到繁忙狀態(tài)busy。

在鏈路talking（x，y）中，描述的是忙時轉(zhuǎn)移這個核心操作，由Object-Z的繼承的思想，我們可以把忙時轉(zhuǎn)移操作對撥打電話操作Dialx進行繼承，在開發(fā)忙時轉(zhuǎn)移操作的形式化規(guī)格時，只需要開發(fā)與Dialx不同的部分，相同的事件和狀態(tài)變化可以進行繼承，忙時轉(zhuǎn)移操作的Z語言形式化規(guī)格如圖5所示：表示這個操作是對撥打電話操作Dialx的繼承，在模式的謂詞表達式部分，表示存在用戶z滿足下述的表達式，用戶x請求與用戶y通話，用戶y處于繁忙狀態(tài)并且把呼叫轉(zhuǎn)移給z，則這個請求轉(zhuǎn)到z。

圖5 忙時轉(zhuǎn)移操作的形式化規(guī)格

3.2 一直呼叫轉(zhuǎn)移功能模塊的形式化規(guī)格

同理，根據(jù)一直呼叫轉(zhuǎn)移的類樹形流程圖（圖3）和上述算法，一直呼叫轉(zhuǎn)移的形式化規(guī)格產(chǎn)生過程如下：

（1）、（2）步與上述忙時呼叫轉(zhuǎn)移功能的過程一致。

（3）從圖中選取最長的鏈路talking(x , y)，該鏈路描述的是一直呼叫轉(zhuǎn)移這個功能模塊最主要的操作一直呼叫轉(zhuǎn)移，我們可以設(shè)定該操作的模式名為CallForwardAlways。

（4）由算法的（1）、（2）步，我們可以得出模式的聲明部分，接著把talking（x，y）鏈路中所有的狀態(tài)變化過程用Z語言進行描述，即可以描述出一直呼叫轉(zhuǎn)移這個操作的形式化規(guī)格如圖6所示：

圖6，一直呼叫轉(zhuǎn)移操作的形式化規(guī)格

4 開發(fā)過程的效率性討論

類樹形流程圖的主要目標是提高Z語言的形式化規(guī)格的開發(fā)效率。由于類樹形圖的組成相對簡單，主要元素包含了開始、結(jié)束、中間節(jié)點和流程線，具有簡明易用的特點，因此，研發(fā)人員在使用類樹形流程圖的時候，不需要描述過于復雜的圖形，這樣，可以大大節(jié)省時間和精力，同時，類樹形流程圖也具有明確、無歧義的特點，符合了形式化規(guī)格嚴謹性和一致性的要求。為了測試用類樹形流程圖所開發(fā)的形式化規(guī)格的質(zhì)量，作者用常用的形式化規(guī)格驗證軟件Z/EVES軟件對進行了驗證，Z/EVES是一個帶有定理證明器的Z 支持工具, 具有交互式證明功能, 可以檢查、分析Z形式規(guī)格說明[6]，經(jīng)過分析與證明，由類樹形流程圖方法所開發(fā)的形式化規(guī)格具備很好的質(zhì)量和可靠性。

5 總結(jié)

本文提出類樹形流程圖的概念，并且詳細的講述了怎樣使用類樹形流程圖開發(fā)出基于Z語言的形式化規(guī)格。文章首先對電信系統(tǒng)中的兩個功能模塊進行描述和分析，接著在這基礎(chǔ)上描繪出該功能模塊的類樹形流程圖，然后依照轉(zhuǎn)換算法，把類樹形流程圖轉(zhuǎn)換成Z語言的形式化規(guī)格。最后，還對類樹形流程圖開發(fā)方法的效率性進行討論?？偟膩碚f，類樹形流程圖簡明、易用，所開發(fā)的形式化規(guī)格具有很好的質(zhì)量和可靠性，期望對軟件工程領(lǐng)域的研發(fā)人員帶來幫助，提高軟件開發(fā)的效率和質(zhì)量。

[1] 吳帥，繆麗君. 形式化方法與可視化模型的結(jié)合及其應用[J]. 計算機與現(xiàn)代化, 2011(3):44-46,56.

[2] 繆淮扣, 陳怡海．軟件形式規(guī)格說明語言—Z[M]．清華大學出版社，2012.

[3] 閆仕宇，胡義香，蔣輝等. 形式化方法在核事故評價系統(tǒng)中的應用[J]. 南華大學學報( 自然科學版), 2012，26(3):73-78.

[4] 許慶國,繆淮扣,曹曉夏等. Object-Z 規(guī)格說明測試用例的自動生成器[J]. 軟件學報,2011, 22(6)：1155-1168.

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

[6] 文志誠，賈峰，胡純?nèi)?一個Object-Z規(guī)格說明的證明責任產(chǎn)生器[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- )，男，廣東茂名人，廣東石油化工學院，碩士，研究方向：軟件開發(fā)形式化方法，廣東茂名，525000