基于Z語言的電信服務(wù)系統(tǒng)的形式化規(guī)格

彭展

0 引言

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

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

電信服務(wù)系統(tǒng)極其復(fù)雜，對穩(wěn)定性要求高，而且不斷要進(jìn)行新功能模塊的開發(fā)，對系統(tǒng)進(jìn)行擴(kuò)展。長期以來，如何提高電信服務(wù)系統(tǒng)的穩(wěn)定性，防止系統(tǒng)內(nèi)部的錯誤產(chǎn)生，降低開發(fā)成本一直都是軟件開發(fā)領(lǐng)域研究的課題。在本文中，提出了用形式化方法進(jìn)行電信服務(wù)系統(tǒng)開發(fā)的思想，首先用形式化規(guī)格語言Z開發(fā)出完整的電信服務(wù)系統(tǒng)的形式化規(guī)格，接著用驗證軟件Z/EVES對形式化規(guī)格的嚴(yán)密性，正確性進(jìn)行驗證?；赯語言的形式化規(guī)格能夠解決電信服務(wù)系統(tǒng)開發(fā)過程中產(chǎn)生的如與實際需求不一致，定義混亂等問題，提高電信服務(wù)系統(tǒng)的穩(wěn)定性和安全性。

1 Z語言的介紹

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

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

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

2 基于Z語言的電信服務(wù)系統(tǒng)的形式化規(guī)格

電信服務(wù)系統(tǒng)由基本的POTS（模擬電話業(yè)務(wù)），再加上不斷增加的功能模塊構(gòu)成，如電話會議、呼叫轉(zhuǎn)移、來電黑名單、呼叫黑名單、呼叫等待、空閑回?fù)堋⒘粞孕畔?、信用卡充值等，以使電信服?wù)系統(tǒng)不斷得到完善，滿足人們?nèi)找嬖鲩L的需求。

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

2.1 電話會議功能的形式化規(guī)格

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

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

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

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

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

2.1.3 變量的初始化模式INIT

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

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

AddFeatureCC/RemoveFeatureCC

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

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

添加一個用戶進(jìn)入電話會議的過程如下:假設(shè)組織者x與y是處于連接狀態(tài)，x請求添加z進(jìn)入電話會議，如果系統(tǒng)響應(yīng)成功，則請求變量request釋放x,connected變量添加（x,z）映射以表示x,z處于連接中，接著waiting和talking變量分別添加（x,y）映射和（x,z）映射以表示（x,y）轉(zhuǎn)變?yōu)榈却隣顟B(tài)，而（x,z）轉(zhuǎn)變?yōu)閷υ挔顟B(tài)，最后peoplecount變量累加1表示電話會議有一個新加入者。

2.1.6 電話會議進(jìn)行中操作的模式ConferenceTalk

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

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

當(dāng)電話組織者進(jìn)行掛斷電話這個操作時，如果仍有一些電話用戶在等待電話會議的狀態(tài)，電信服務(wù)系統(tǒng)會重?fù)茉摻M織者的電話以作提醒。

當(dāng)電話會議結(jié)束，并且組織者掛斷電話，則電話會議占用的所有資源都會被釋放。接著組織者將會進(jìn)入到空閑狀態(tài)，并且人數(shù)重設(shè)為1。

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

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

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

2.1.9 對POTS中RemoveSubscriber操作的擴(kuò)展

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

3 形式化規(guī)格的驗證

在完成系統(tǒng)形式化規(guī)格的開發(fā)后，為提高形式化規(guī)格的嚴(yán)密性和準(zhǔn)確性，可以使用一些工具軟件對形式化規(guī)格進(jìn)行驗證。在這里我們使用的是Z/EVES軟件，Z/EVES是一個能夠?qū)語言的語法和類型進(jìn)行檢查、模式擴(kuò)展、前置條件計算、證明的工具軟件[6]。

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

圖2 Z/EVES軟件對形式化規(guī)格進(jìn)行驗證

4 結(jié)束語

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

[1]曾一,周欣,周吉.基于形式化規(guī)格說明的UML狀態(tài)圖提取[J].計算機(jī)應(yīng)用研究，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語言的互聯(lián)網(wǎng)登陸系統(tǒng)的形式化規(guī)格與驗證[J].南華大學(xué)學(xué)報（自然科學(xué)版），2009,23（4）:79-83.

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

[5]何炎祥,宋強(qiáng),黃謙.從過程描述語言到Z語言[J].小型微型計算機(jī)系統(tǒng),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.