Z規格說明的推理與驗證

趙正旭，溫晉杰，趙衛華

Z規格說明的推理與驗證

趙正旭，溫晉杰，趙衛華

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

Z規格說明；推理；驗證；形式化；條件

0 引言

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

1 Z語言概述

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

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

圖1 總體框架圖

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

2 Z規約的推理

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

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

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

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

應用點規則對前置條件進行化簡。

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

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

RESPONSE：= Success|Error

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

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

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

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

表2 前置條件表

3 Z規約的驗證

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

操作模式 Addsuccess執行成功之后會導致電話薄中增加一位聯系人，即電話薄聯系人姓名集合變為原集合加上用戶輸入的聯系人姓名，聯系人電話號碼集合變為原集合加上用戶輸入的聯系人電話，利用邏輯表達式可表示如下：

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

操作模式 Deletesuccess執行成功之后會導致電話薄中減少一位聯系人，即電話薄聯系人姓名集合變為原集合減去用戶輸入的聯系人姓名，聯系人電話號碼集合變為原集合減去用戶輸入的聯系人電話，利用邏輯表達式可表示如下：

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

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

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

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

表3 后置條件表

4 總結

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

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

[1] 趙正旭, 溫晉杰, 趙衛華. Z規范及其使用方法[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] 趙曉峰. 虛擬制造環境的信息規范及其Z描述研究[D].濟南：山東大學. 2010.

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

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

[10] 左孝凌, 李為鑒, 劉永才. 離散數學[M]. 上海： 上海科學技術文獻出版社, 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-），男，石家莊鐵道大學，教授，長江學者，博士生導師，研究方向：虛擬現實，數據組織，石家莊 050043

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

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