基于Z語言的電信服務系統的形式化規格

彭展

0 引言

形式化方法（Formal Method）是一種基于數學的軟件開發方法，它能夠精確地描述系統的需求和設計，有效地提高軟件質量[1]。這種方法被廣泛地應用到不同領域的軟件開發中，尤其是耗資巨大，對質量要求非常高的軟件系統，如電力系統、鐵路運輸調度系統、航空航天系統等。使用形式化方法開發系統能夠帶來幾大好處:（1）由于形式化方法是基于可靠的數學理論，其嚴格的語義規則能夠消除軟件開發過程中的歧義描述。（2）它可以引導我們在開發的過程中使用哪些輔助工具。（3）它能夠使開發人員精確地描述系統的各個功能，并且產生一份可靠的文檔，即使在測試和維護階段也能夠有很好的支持[2]。總的來說，形式化方法能夠大大地提高軟件系統的可靠性和準確性，并且能夠顯著地減少整個軟件開發過程的工作量。

形式化方法可具體為形式化規格與驗證[3]。形式化規格是通過具有明確數學定義的文法和語義的方法或語言對軟件的期望特征或者行為進行的精確、簡潔描述,而形式化驗證則是基于已建立的形式化規格,對軟件的相關特征進行評價的數學分析和證明[3]。

電信服務系統極其復雜，對穩定性要求高，而且不斷要進行新功能模塊的開發，對系統進行擴展。長期以來，如何提高電信服務系統的穩定性，防止系統內部的錯誤產生，降低開發成本一直都是軟件開發領域研究的課題。在本文中，提出了用形式化方法進行電信服務系統開發的思想，首先用形式化規格語言Z開發出完整的電信服務系統的形式化規格，接著用驗證軟件Z/EVES對形式化規格的嚴密性，正確性進行驗證。基于Z語言的形式化規格能夠解決電信服務系統開發過程中產生的如與實際需求不一致，定義混亂等問題，提高電信服務系統的穩定性和安全性。

1 Z語言的介紹

形式化方法產生了很多種與其相對應的形式規格語言（Formal Specification language），如CADP,LOTOS,mCRL2,RAISE,VDM和Z等，具有代表性的是VDM和Z[4]。在本文中，主要是討論Z語言（Z Notation）。Z語言是一種基于一階謂詞邏輯和集合論的形式規格說明語言,它采用了嚴格的數學理論,可以產生簡明、精確、無歧義且可證明的規格說明[3]。Z語言的特點是“狀態-操作”表示方式[5],這兩種表示方式可以統一表示，如圖1所示:

圖1 Z語言的主要表示方式

SchemaName是模式的名字，Declarations 是模式的聲明部分，Predicate是模式的謂詞不變式。如果是狀態模式,聲明部分是狀態變量的聲明,謂詞不變式則是狀態變量應滿足的條件;如果是操作模式,聲明部分是狀態模式和輸入、輸出的聲明,謂詞不變式是操作應滿足的條件和該操作所引起的變化[5]。

2 基于Z語言的電信服務系統的形式化規格

電信服務系統由基本的POTS（模擬電話業務），再加上不斷增加的功能模塊構成，如電話會議、呼叫轉移、來電黑名單、呼叫黑名單、呼叫等待、空閑回撥、留言信箱、信用卡充值等，以使電信服務系統不斷得到完善，滿足人們日益增長的需求。

本文中，作者已經開發出完整的基于Z語言的電信服務系統的形式化規格，包含了電信服務系統的大部分功能，以下詳細介紹電話會議功能的形式化規格，其它功能可以從該功能的形式化規格中得到參考。

2.1 電話會議功能的形式化規格

電話會議功能的目的是讓用戶通過電話進行會議。組織者添加第三方用戶進入電話會議，一般情況下，系統最多只允許6個用戶進行會議討論。當組織者掛斷電話時，如果還有參與者在等待電話會議，則系統會自動重撥組織者的電話以作提醒。

2.1.1 電話會議功能所包含的操作的描述

電話會議功能（Conference Call）是對POTS（由于篇幅原因，POST的Z規格在本文中沒有列出來）的繼承，并且包含了6個操作。這六個操作都是電話會議功能中所涉及的操作，包括添加電話會議功能操作AddFeatureCC、刪除電話會議功能操作RemoveFeatureCC、添加用戶入電話會議操作AddAdditionalPerson、電話會議進行中操作ConferenceTalk、組織者掛斷電話操作OrganigerHangup以及參與者掛斷電話操作ParticipantHangup。

2.1.2 變量及變量約束條件模式Variable

在模式Variable中，主要是對變量及其約束條件的設定。電話會議功能包含了5個變量，分別是擁有電話會議功能的用戶變量subscriberCC、電話會議進行中變量inconference、參與人數變量peoplecount、等待接入狀態變量waiting、通話狀態變量talking。在謂詞不變式部分，是變量的約束條件。

2.1.3 變量的初始化模式INIT

在初始化模式中，所有變量都定義為空集

2.1.4 添加及刪除電話會議操作的模式

AddFeatureCC/RemoveFeatureCC

在系統為用戶添加電話會議功能時，這個用戶必須處于空閑狀態，并且不擁有該功能，刪除這個功能時也必須處于空閑狀態但必須擁有該功能。

2.1.5 添加用戶入電話會議操作的模式AddAdditionalPerson

添加一個用戶進入電話會議的過程如下:假設組織者x與y是處于連接狀態，x請求添加z進入電話會議，如果系統響應成功，則請求變量request釋放x,connected變量添加（x,z）映射以表示x,z處于連接中，接著waiting和talking變量分別添加（x,y）映射和（x,z）映射以表示（x,y）轉變為等待狀態，而（x,z）轉變為對話狀態，最后peoplecount變量累加1表示電話會議有一個新加入者。

2.1.6 電話會議進行中操作的模式ConferenceTalk

當電話會議開始后，變量waiting和talking將會刪除所有x用戶所映射的關系，之后用戶x以及所有與用戶x相連接的用戶都將會添加到變量inconference的集合當中以表示這些用戶進入電話會議中。

2.1.7 組織者掛斷電話操作的模式OrganigerHangup

當電話組織者進行掛斷電話這個操作時，如果仍有一些電話用戶在等待電話會議的狀態，電信服務系統會重撥該組織者的電話以作提醒。

當電話會議結束，并且組織者掛斷電話，則電話會議占用的所有資源都會被釋放。接著組織者將會進入到空閑狀態，并且人數重設為1。

組織者掛斷動作包含了掛斷但有其它人等待以及掛斷并且電話會議結束這兩種情況，所以其模式是由兩種對應的子模式組成。

2.1.8 參與人掛斷電話操作的模式ParticipantHangup

如果一個參與者在電話會議的過程中掛斷電話，則他的呼叫將會斷開并且從inconference集合中移除，電話會議的參與人數也會減1，并且該用戶也會返回空閑狀態。

2.1.9 對POTS中RemoveSubscriber操作的擴展

以下這個動作是對POTS中RemoveSubscriber這個動作的繼承，如果系統刪除一個用戶，電信服務系統仍需要從subscriberCC集合中刪除該用戶，以使電話會議功能的用戶列表中不在出現這個用戶的名字，以保證系統的一致性和完整性。

3 形式化規格的驗證

在完成系統形式化規格的開發后，為提高形式化規格的嚴密性和準確性，可以使用一些工具軟件對形式化規格進行驗證。在這里我們使用的是Z/EVES軟件，Z/EVES是一個能夠對Z語言的語法和類型進行檢查、模式擴展、前置條件計算、證明的工具軟件[6]。

在檢驗的過程中，只需要輸入所需要驗證的形式化規格，然后執行檢查的操作，如果通過了驗證，則在軟件左邊的Syntax和Proof欄目顯示‘Y’以表示通過了語法檢查和證明，否則顯示‘N’并做出相應的提示，在這種情況下，則需要對形式化規格進行修改，直到通過了驗證。使用Z/EVES對第3部分的電話會議功能的形式化規格進行驗證，如圖2所示:

圖2 Z/EVES軟件對形式化規格進行驗證

4 結束語

本文介紹了形式化方法和主流的形式化規格語言Z，接著用Z語言開發電信服務系統的形式化規格，并通過了Z/EVES軟件的驗證。這套形式化規格對電信服務系統的各個功能進行了準確、規范、無歧義的描述，為提高電信服務系統的可靠性、穩定性打下了堅實的基礎，同時也可應用于探測電信服務系統中存在的沖突和缺陷，推動了形式化方法和Z語言在國內電信領域的軟件系統的研究和應用。

[1]曾一,周欣,周吉.基于形式化規格說明的UML狀態圖提取[J].計算機應用研究，2011，2（5）:1767—1769.

[2]Monin J.F.,Fran?ois J..Understanding formal methods,Written and translated by Jean-Fran?ois.London:Springer,2003.

[3]閆仕宇.基于Z語言的互聯網登陸系統的形式化規格與驗證[J].南華大學學報（自然科學版），2009,23（4）:79-83.

[4]姚昱，毋國慶，吳懷廣，等.一種軟件需求描述語言的設計與實現[J].計算機工程與應用，2009,45（21）:185-188.

[5]何炎祥,宋強,黃謙.從過程描述語言到Z語言[J].小型微型計算機系統,2002,23（9）:1110-1113.

[6]Kallel S.,Kacem M.H.,Jmaiel M..Modeling and enforcing invariants of dynamic software architectures[J],Software and Systems Modeling.2012,11(1):127-149.