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

Z規(guī)格說明的推理與驗證

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

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

Z規(guī)格說明；推理；驗證；形式化；條件

0 引言

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

1 Z語言概述

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

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

圖1 總體框架圖

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

2 Z規(guī)約的推理

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

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

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

在謂詞部分中對這些變量用存在量詞進行約束；

應用點規(guī)則對前置條件進行化簡。

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

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

RESPONSE：= Success|Error

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

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

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

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

表2 前置條件表

3 Z規(guī)約的驗證

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

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

對操作模式 Addsuccess驗證就是利用操作模式中聲明的狀態(tài)變量和操作關系推導出上述三條結論。首先，證明

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

對操作模式 Deletesuccess驗證就是利用操作模式中聲明的狀態(tài)變量和操作關系推導出上述兩條結論。首先，證明

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

對操作模式Modifysuccess驗證就是利用操作模式中聲

明的狀態(tài)變量和操作關系推導出上述3條結論。首先，證明

表3 后置條件表

4 總結

形式化方法主要分為形式化規(guī)約和形式化驗證兩個方面。形式化規(guī)約是通過具有明確數(shù)學定義的文法和語義的方法或者語言對軟件的期望特性及行為進行的精確描述。形式化驗證是基于已建立的形式化規(guī)格對軟件的相關特性進行評價的數(shù)學分析和證明。

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

[1] 趙正旭, 溫晉杰, 趙衛(wèi)華. Z規(guī)范及其使用方法[M]. 北京：科學出版社, 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].濟南：山東大學. 2010.

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

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

[10] 左孝凌, 李為鑒, 劉永才. 離散數(shù)學[M]. 上海： 上?？茖W技術文獻出版社, 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）

河北省高等學校高層次人才科學研究項目（GCC2014010）；

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

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

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