Z規(guī)格說(shuō)明的推理與驗(yàn)證

趙正旭，溫晉杰，趙衛(wèi)華

Z規(guī)格說(shuō)明的推理與驗(yàn)證

趙正旭，溫晉杰，趙衛(wèi)華

Z規(guī)格說(shuō)明具有非形式規(guī)約不可比擬的嚴(yán)謹(jǐn)性、清晰性。這種描述對(duì)于系統(tǒng)內(nèi)對(duì)象的狀態(tài)描述、行為描述是非常有用的原始參照物。但是，形式化描述不可避免的可能會(huì)含有錯(cuò)誤或者是矛盾，這些問(wèn)題在后期必定會(huì)導(dǎo)致前期的形式化設(shè)計(jì)不能付諸實(shí)踐。因此，有必要做一些形式化的推理與驗(yàn)證來(lái)確保Z規(guī)約的實(shí)施。形式化推理是基于Z規(guī)格說(shuō)明對(duì)一個(gè)操作模式求其前置條件，即求一個(gè)操作成功執(zhí)行的必要條件，然后對(duì)比客觀條件是否滿足必要條件；形式化驗(yàn)證是一個(gè)操作模式求其后置條件，從集合的角度出發(fā)驗(yàn)證一個(gè)操作成功執(zhí)行之后所導(dǎo)致的狀態(tài)量變化是否與操作模式描述一致。

Z規(guī)格說(shuō)明；推理；驗(yàn)證；形式化；條件

0 引言

在軟件研發(fā)的過(guò)程中，面對(duì)需求越來(lái)越多變，系統(tǒng)越來(lái)越復(fù)雜的現(xiàn)狀，軟件需求規(guī)格說(shuō)明書在軟件生命周期中占有舉足輕重的地位，是所有軟件研發(fā)參與人員的一個(gè)可靠參照物。如何確保撰寫的規(guī)格說(shuō)明具有客戶所要求的性質(zhì)？如何確保參照該規(guī)格說(shuō)明編寫出的軟件與規(guī)格說(shuō)明書所描述的相吻合？如何保證研發(fā)人員編寫出的程序的可靠性、功能性、效率性等各項(xiàng)質(zhì)量指標(biāo)呢[1]？形式化推理是驗(yàn)證軟件正確性的重要方法之一，它通過(guò)嚴(yán)格的數(shù)學(xué)方法來(lái)評(píng)價(jià)一個(gè)程序是否達(dá)到了需求規(guī)格說(shuō)明書所描述的功能，也就是說(shuō)，對(duì)于一組允許輸入的信息X，嚴(yán)格的證明程序能否正確執(zhí)行以及能否得到正確的輸出信息Z。程序正確性證明的研究早在20世紀(jì)50年代就為圖靈等人所注意。一份合格的Z規(guī)格說(shuō)明需要清晰準(zhǔn)確的描述“做什么”，還必須要保證參照該規(guī)格說(shuō)明編寫出的軟件與規(guī)格說(shuō)明書所描述的各項(xiàng)特性相匹配。2014年在新加坡舉行的第19屆形式化方法國(guó)際研討會(huì)上，有兩個(gè)來(lái)自中國(guó)的團(tuán)隊(duì)進(jìn)行了匯報(bào)，恰巧他們匯報(bào)的題目都與玉兔月球車相關(guān)，一個(gè)與月球軟著陸控制器相關(guān)，另一個(gè)與玉兔月球車控制系統(tǒng)相關(guān)。其中用形式化方法驗(yàn)證玉兔控制系統(tǒng)切實(shí)體現(xiàn)了形式化方法的強(qiáng)大與復(fù)雜[2,3]。2015年國(guó)外一個(gè)技術(shù)團(tuán)隊(duì)利用形式化方法驗(yàn)證 Java中一些排序算法的正確性，在驗(yàn)證Timsort排序算法時(shí)發(fā)現(xiàn)了Bug。利用自動(dòng)生成的測(cè)試用例集很難生成一個(gè)可以觸發(fā)該 Bug的Array，所以，通過(guò)形式化推理來(lái)證明程序的正確性的時(shí)候發(fā)現(xiàn)了這個(gè)錯(cuò)誤[4]。

1 Z語(yǔ)言概述

Z語(yǔ)言是一種用“數(shù)學(xué)文字”或“數(shù)學(xué)符號(hào)”來(lái)描述計(jì)算機(jī)系統(tǒng)的規(guī)范化語(yǔ)言，它不但能應(yīng)用于計(jì)算機(jī)硬件系統(tǒng)，而且也特別適用于計(jì)算機(jī)軟件系統(tǒng)。Z語(yǔ)言描述“做什么”而不涉及“怎么做”，只對(duì)目標(biāo)軟件系統(tǒng)進(jìn)行功能描述。本質(zhì)來(lái)講，Z語(yǔ)言僅僅是一套規(guī)定的數(shù)學(xué)符號(hào)，使用Z語(yǔ)言所

寫的“程序”是對(duì)計(jì)算機(jī)軟件或硬件系統(tǒng)的一種抽象化設(shè)計(jì)。所以，利用Z語(yǔ)言寫出來(lái)的內(nèi)容不是計(jì)算機(jī)程序，更不是可以編譯而生成能夠在計(jì)算機(jī)上運(yùn)行的代碼。利用Z語(yǔ)言寫出來(lái)的內(nèi)容不是讓計(jì)算機(jī)運(yùn)行的，而是供人理解和分析的。用戶可以通過(guò)這些內(nèi)容去理解計(jì)算機(jī)系統(tǒng)的模塊、數(shù)據(jù)類型、過(guò)程、函數(shù)、對(duì)象、類等，進(jìn)而對(duì)計(jì)算機(jī)系統(tǒng)的行為、結(jié)構(gòu)、邏輯進(jìn)行分析、驗(yàn)證、改進(jìn)、測(cè)試等。通俗地講，Z語(yǔ)言用數(shù)學(xué)邏輯和理論模型對(duì)計(jì)算機(jī)系統(tǒng)進(jìn)行嚴(yán)格的描述，形成一種抽象的設(shè)計(jì)。通常把這種設(shè)計(jì)的內(nèi)容叫做計(jì)算機(jī)系統(tǒng)的需求規(guī)格說(shuō)明，即形式化描述。與其他非形式化方法相比，Z規(guī)格說(shuō)明具有以下特點(diǎn)。首先，Z語(yǔ)言不是計(jì)算機(jī)程序編制工具或編程系統(tǒng)，Z語(yǔ)言是設(shè)計(jì)規(guī)范，采用了包括集合、序列、包、關(guān)系、函數(shù)、類型、對(duì)象等抽象的數(shù)學(xué)理論。所以，Z語(yǔ)言是一種數(shù)學(xué)語(yǔ)言。其次，Z語(yǔ)言形成的規(guī)格說(shuō)明的形式不是完全類似于ASCII碼的文字和字符串，而是包括了規(guī)范化的數(shù)學(xué)符號(hào)和演算圖形。Z語(yǔ)言形成的規(guī)格說(shuō)明的內(nèi)容不是能編譯和運(yùn)行的程序編碼，而是用來(lái)進(jìn)行邏輯推理和數(shù)學(xué)演算的。另外，Z語(yǔ)言沒(méi)有完全使用數(shù)學(xué)符號(hào)來(lái)形成規(guī)格說(shuō)明，它也使用了自然語(yǔ)言來(lái)定義變量和添加批注。所以，由Z語(yǔ)言生成的規(guī)格說(shuō)明易于讀寫和解析。最后，由Z語(yǔ)言所形成的規(guī)格說(shuō)明不僅嚴(yán)謹(jǐn)、清晰、無(wú)二義，而且可以通過(guò)形式化方法軟件（如類似于Z/EVES的輔助工具）對(duì)其進(jìn)行驗(yàn)證和推理。以下兩個(gè)小節(jié)分別給出了Z規(guī)約的推理與驗(yàn)證方法，總體框架如圖1所示：

圖1 總體框架圖

Z規(guī)格說(shuō)明與其他方法的本質(zhì)區(qū)別在于嚴(yán)謹(jǐn)以及無(wú)二義，能夠最大限度保證系統(tǒng)的安全性。其主要研究?jī)?nèi)容為形式化的軟件工程方法，貫穿于整個(gè)軟件工程生命周期，包括形式化描述、形式化驗(yàn)證、形式化推理、形式化求精等。

2 Z規(guī)約的推理

Z語(yǔ)言所形成的規(guī)格說(shuō)明具有非形式規(guī)約不可比擬的嚴(yán)謹(jǐn)性、清晰性，這種描述對(duì)于系統(tǒng)對(duì)象的狀態(tài)描述、行為描述無(wú)疑是非常有用的原始參照物。但是，形式化描述也不可避免的可能會(huì)含有錯(cuò)誤或者是矛盾，也有不滿足前置條件的操作行為，這些問(wèn)題在后期必定會(huì)導(dǎo)致前期的形式化設(shè)計(jì)不能付諸實(shí)踐。另外，在操作構(gòu)型內(nèi)，可能有隱含的假設(shè)會(huì)導(dǎo)致那些不能解釋操作效果的情況，也可能會(huì)出現(xiàn)死鎖等不能容忍的狀態(tài)。因此，有必要做一些形式化的推理與驗(yàn)證，對(duì)Z規(guī)格說(shuō)明進(jìn)行進(jìn)一步的分析研究。形式化驗(yàn)證并不能完全確保系統(tǒng)的性能正確無(wú)誤，但是可以最大限度地理解和分析系統(tǒng)，并盡可能地發(fā)現(xiàn)其中的不一致性、模糊性、不完備性等錯(cuò)誤。Z規(guī)格說(shuō)明一個(gè)主要的特點(diǎn)就是可以進(jìn)行形式推理，這一屬性對(duì)于那些高安全性和可靠性的系統(tǒng)來(lái)說(shuō)是相當(dāng)有吸引力的。

形式化推理主要是對(duì)前置條件的證明，即證明操作能夠成功執(zhí)行的必要條件。一個(gè)操作可以成功執(zhí)行的起始狀態(tài)由該操作的前置條件給出[5]。Z語(yǔ)言形式化推理可分為以下3步：

從描述操作模式的說(shuō)明部分中刪除后狀態(tài)變量和輸出變量；

在謂詞部分中對(duì)這些變量用存在量詞進(jìn)行約束；

應(yīng)用點(diǎn)規(guī)則對(duì)前置條件進(jìn)行化簡(jiǎn)。

形式化推理與驗(yàn)證基于形式化規(guī)格說(shuō)明。所以，有必要先給出一份Z規(guī)格說(shuō)明書。手機(jī)通訊錄應(yīng)用程序是日常生活中非常熟悉的一個(gè)軟件，其中新建聯(lián)系人、刪除聯(lián)系人、修改聯(lián)系人信息操作是基本操作，以下是使用微軟Office Word 2007支持的Z Word Tools工具編寫的對(duì)應(yīng)的操作模式。

首先要確定這個(gè)應(yīng)用程序要涉及到的狀態(tài)變量并且對(duì)其進(jìn)行命名。在這個(gè)程序中,需要定義的變量包括聯(lián)系人姓名(PhoneName)和聯(lián)系人電話號(hào)碼(PhoneNumber)。其次，定義聯(lián)系人姓名和聯(lián)系人電話號(hào)碼的類型分別為姓名（Name）與號(hào)碼（Number）。接下來(lái)，要定義操作之后系統(tǒng)必須給出的提示信息。通過(guò)枚舉法枚舉如下：

RESPONSE：= Success|Error

利用 Z語(yǔ)言對(duì)一個(gè)客觀事物的形式化描述的第一步就是對(duì)事物進(jìn)行初始化，當(dāng)然也包括對(duì)涉及到的狀態(tài)變量和集合的初始化。

以下依次為初始化模式、新建聯(lián)系人操作模式、刪除聯(lián)系人操作模式、修改聯(lián)系人操作模式。

如果一個(gè)操作是有效的，那么必定存在一個(gè)正確的初始化模式。首先，對(duì)初始化模式進(jìn)行推理，觀察上述初始化模式，如果可以證明：

求解前置條件的一般過(guò)程如上，重復(fù)上述過(guò)程可以得到刪除聯(lián)系人與修改聯(lián)系人信息的前置條件，如表2所示：

表2 前置條件表

3 Z規(guī)約的驗(yàn)證

基于 Z規(guī)格說(shuō)明的形式化驗(yàn)證主要是對(duì)操作模式后置條件的驗(yàn)證，即基于離散數(shù)學(xué)的規(guī)則與概念，從集合的角度出發(fā)驗(yàn)證操作成功執(zhí)行之后，各狀態(tài)變量是否正確[6]。

操作模式 Addsuccess執(zhí)行成功之后會(huì)導(dǎo)致電話薄中增加一位聯(lián)系人，即電話薄聯(lián)系人姓名集合變?yōu)樵霞由嫌脩糨斎氲穆?lián)系人姓名，聯(lián)系人電話號(hào)碼集合變?yōu)樵霞由嫌脩糨斎氲穆?lián)系人電話，利用邏輯表達(dá)式可表示如下：

對(duì)操作模式 Addsuccess驗(yàn)證就是利用操作模式中聲明的狀態(tài)變量和操作關(guān)系推導(dǎo)出上述三條結(jié)論。首先，證明

操作模式 Deletesuccess執(zhí)行成功之后會(huì)導(dǎo)致電話薄中減少一位聯(lián)系人，即電話薄聯(lián)系人姓名集合變?yōu)樵蠝p去用戶輸入的聯(lián)系人姓名，聯(lián)系人電話號(hào)碼集合變?yōu)樵蠝p去用戶輸入的聯(lián)系人電話，利用邏輯表達(dá)式可表示如下：

對(duì)操作模式 Deletesuccess驗(yàn)證就是利用操作模式中聲明的狀態(tài)變量和操作關(guān)系推導(dǎo)出上述兩條結(jié)論。首先，證明

操作模式Modifysuccess執(zhí)行成功之后電話薄中聯(lián)系人數(shù)量不會(huì)發(fā)生變化，但是，對(duì)電話薄聯(lián)系人電話號(hào)碼集合進(jìn)行了更新，利用邏輯表達(dá)式可表示如下：

對(duì)操作模式Modifysuccess驗(yàn)證就是利用操作模式中聲

明的狀態(tài)變量和操作關(guān)系推導(dǎo)出上述3條結(jié)論。首先，證明

表3 后置條件表

4 總結(jié)

形式化方法主要分為形式化規(guī)約和形式化驗(yàn)證兩個(gè)方面。形式化規(guī)約是通過(guò)具有明確數(shù)學(xué)定義的文法和語(yǔ)義的方法或者語(yǔ)言對(duì)軟件的期望特性及行為進(jìn)行的精確描述。形式化驗(yàn)證是基于已建立的形式化規(guī)格對(duì)軟件的相關(guān)特性進(jìn)行評(píng)價(jià)的數(shù)學(xué)分析和證明。

程序求精是將自動(dòng)推理和形式化方法相結(jié)合而形成的一門新技術(shù)，它研究從抽象的形式規(guī)格推演出具體的面向計(jì)算機(jī)的程序代碼的全過(guò)程。用一個(gè)抽象程度低、過(guò)程性強(qiáng)的程序去代替一個(gè)抽象程度高、過(guò)程性弱的程序，并保持它們之間功能的一致。也就是說(shuō)如何將Z規(guī)約轉(zhuǎn)換成可執(zhí)行的代碼。目前。主要的策略是按照抽象程度劃分層次結(jié)構(gòu)，最高層為抽象程度最高的Z規(guī)約，最底層為抽象程度最低的可執(zhí)行代碼，中間為一系列的過(guò)度程序。對(duì)Z規(guī)約的求精或轉(zhuǎn)換是推廣形式化Z語(yǔ)言的必由環(huán)節(jié)，也是今后的一個(gè)研究重點(diǎn)與熱點(diǎn)。

[1] 趙正旭, 溫晉杰, 趙衛(wèi)華. Z規(guī)范及其使用方法[M]. 北京：科學(xué)出版社, 2015：18-100.

[2] Hengjun Zhao, Mengfei Yang, Naijun Zhan. Formal. Verification of a Descent Guidance Control Program of a Lunar Lander[A]. FM 2014： Formal Methods [C]. Switzerland： Springer International Publishing, 2014： 733-748.

[3] Lijun Shan. Formal. Verification of Lunar Rover Control Software Using UPPAAL[A]. FM 2014： Formal Methods[C]. Switzerland： Springer International Publishing, 2014： 718-732.

[4] 百度, 形式化方法的逆襲[EB/OL]. http：//bindog. github.io/blog/2015/03/30/use-formal-method-to-find-the -bug-in-timsort-and-lunar-rover/, 2015-10-14.

[5] Jim Woodcock, Jim Davies. Using Z Specification, Refinement and Proof[M]. Oxford ： University of Oxford, 1995：201-270.

[6] J. M.Spivey.The Z Notation：A Reference Manual(Second Edition). Programming Research Group[M]. Oxford：University of Oxford,1992：156-213.

[7] 趙曉峰. 虛擬制造環(huán)境的信息規(guī)范及其Z描述研究[D].濟(jì)南：山東大學(xué). 2010.

[8] 古天龍, 常亮. 離散數(shù)學(xué)[M]. 北京： 清華大學(xué)出版社, 2012：57-83.

[9] 古天龍. 軟件開(kāi)發(fā)的形式化方法[M]. 北京： 高等教育出版社, 2005：159-199.

[10] 左孝凌, 李為鑒, 劉永才. 離散數(shù)學(xué)[M]. 上海： 上海科學(xué)技術(shù)文獻(xiàn)出版社, 1982：77-95.

[11] A. Hall. Z Word Tools：Write, check, index and diagram Z specifications in Microsoft Word[EB/OL].http：//zwor dtools.sourceforge.net/, 2015-02-26.

Reasoning and Verifying of Z Specification

Zhao Zhengxu, Wen Jinjie, Zhao Weihua
(Shijiazhuang Tiedao University, Shijiazhuang 050043,China)

Compared with the informal specification, Z notion has incomparable rigorousness and clarity. The notion is an original reference for the state description and behavior description of objects in the system. However, Z notion may inevitably contain errors or contradictions, which will lead that the early formal design cannot be put into practice in the later. Therefore, it is necessary to do some formal reasoning and validation to ensure the implementation of Z notion. Formal reasoning is based on Z specification for an operator schema of its pre-condition, that is to infer the necessary conditions for the successful execution of an operation and calculates whether the objective conditions meet the necessary specifications. Formal verification is an operation mode for its post condition, from a set perspective, the verification of whether the change of the state variables caused by a successful operation is consistent with the description of the operator schema.

Z specification； Reasoning； Verification； Formalization； Conditions

TP393

A

1007-757X(2016)11-0012-05

2016.01.18）

河北省高等學(xué)校高層次人才科學(xué)研究項(xiàng)目（GCC2014010）；

趙正旭（1960-），男，石家莊鐵道大學(xué)，教授，長(zhǎng)江學(xué)者，博士生導(dǎo)師，研究方向：虛擬現(xiàn)實(shí)，數(shù)據(jù)組織，石家莊 050043

溫晉杰（1990-），男，石家莊鐵道大學(xué)，信息科學(xué)與技術(shù)學(xué)院，碩士研究生，研究方向：形式化軟件工程，石家莊 050043

趙衛(wèi)華（1961-），女，石家莊鐵道大學(xué)，信息科學(xué)與技術(shù)學(xué)院，副教授，研究方向：信息組織，石家莊 050043