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

彭展

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

彭展

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

類樹形流程圖，Z語言，電信系統，形式化規格

0 引言

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

在使用Z語言開發形式化規格的過程中，需要考慮每個對象狀態的變換，不同的操作會

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

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

1 功能描述

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

圖1，忙時呼叫轉移和一直呼叫轉移的示意圖

2 類樹形流程圖

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

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

圖2，忙時呼叫轉移的類樹形流程圖

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

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

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

圖3，一直呼叫轉移的類樹形流程圖

在圖3中，由流程開始到流程結束，可以產生6條不同的鏈路，因此，電信服務系統產生6種不同的狀態變化過程。

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

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

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

（1）根據類樹形流程圖中出現的事件參與者設定模式（schema）聲明部分的變量和變量類型。

（2）由類樹形流程圖中出現的狀態變化情況設定相應的狀態變量。

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

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

3.1 忙時呼叫轉移功能模塊的形式化規格

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

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

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

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

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

圖4，撥打電話操作的形式化規格

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

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

圖5 忙時轉移操作的形式化規格

3.2 一直呼叫轉移功能模塊的形式化規格

同理，根據一直呼叫轉移的類樹形流程圖（圖3）和上述算法，一直呼叫轉移的形式化規格產生過程如下：

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

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

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

圖6，一直呼叫轉移操作的形式化規格

4 開發過程的效率性討論

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

5 總結

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

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

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

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

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

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

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