B方法在PVS中的應(yīng)用

劉 梅

（上海應(yīng)用技術(shù)學(xué)院計算機科學(xué)與信息工程學(xué)院，上海 201418）

B方法在PVS中的應(yīng)用

劉 梅

（上海應(yīng)用技術(shù)學(xué)院計算機科學(xué)與信息工程學(xué)院，上海 201418）

針對B方法和原型驗證系統(tǒng)（PVS）的特點，提出了將B方法引入到PVS中，即將一個用B方法描述的系統(tǒng)轉(zhuǎn)換為由PVS描述，以此來實現(xiàn)形式化的檢驗證明.B方法中的抽象機在PVS中轉(zhuǎn)換為一個方法，而B方法中的不變量不變式要轉(zhuǎn)換為PVS中的一個類型，由B方法描述的性質(zhì)則轉(zhuǎn)換為PVS中的推測、猜想，并借助于PVS自帶的證明器有效地完成相應(yīng)證明工作.最后，通過1個電梯控制系統(tǒng)來闡述上述轉(zhuǎn)換方法.

B方法；原形驗證系統(tǒng)；形式化方法；電梯系統(tǒng)控制器

隨著信息技術(shù)的不斷發(fā)展，以及越來越多軟硬件技術(shù)的結(jié)合，當(dāng)今項目系統(tǒng)設(shè)計的要求越來越高.伴隨著復(fù)雜的系統(tǒng)設(shè)計和高質(zhì)量安全需求，這一趨勢將在今后數(shù)年愈發(fā)明顯.然而，如果僅通過軟硬件測試，常常會因時間或財力等因素不能完全達(dá)到具體產(chǎn)品安全覆蓋的要求.長期以來，人們認(rèn)識到形式化方法［1］可以幫助設(shè)計人員發(fā)現(xiàn)和彌補一些疏漏，或者發(fā)現(xiàn)一些設(shè)計中有歧義的地方，以此來不斷提高項目設(shè)計質(zhì)量.本文集中關(guān)注B方法［2］和原型驗證系統(tǒng)（PVS）［3］這2個形式化方法，建立一個可以將B方法引入的PVS系統(tǒng)，通過該方法，不僅能提高建模的質(zhì)量，而且能利用一個強有力的定理證明器執(zhí)行全類型檢測.

1 E方法和PVS的概要介紹

1.1 E方法

一般而言，B方法是由一些抽象機組成，并在此基礎(chǔ)上不斷做出精化的過程，最后一步的精化相當(dāng)于實現(xiàn).在B方法中，一個模塊稱之為一個抽象機［4］，每一個抽象機都有其各自的業(yè)務(wù)，允許外部使用者調(diào)用或切換其當(dāng)前狀態(tài).根據(jù)B方法的句法規(guī)則，一個抽象機由決定其狀態(tài)和描述狀態(tài)性質(zhì)的一些子句所組成.子句包括集合、變量、不變量、初始化和操作等.在B方法中，變量描述的是內(nèi)部變化；不變量約束的是變量的變化范圍；初始化描述的是抽象機初始時所必需滿足的不變量以及初始狀態(tài)；由抽象機提供的方法稱之為操作.抽象機的描述可以通過不斷地精化直至最后的實現(xiàn)，且上述子句都將在精化中得以保留.

1.2 PVS

PVS的語言建立在高階邏輯上，而高階邏輯可以提供給模塊更多的參數(shù)理論和更為豐富多樣的類型系統(tǒng)，包括子類型的注釋和類型依賴.PVS描述［5］由許多理論部分組成，每一個理論都由一些必要的聲明組成：聲明包含類型、常量、變量、公理和公式，也可以通過引用其他理論獲得該理論中所用到的聲明.

當(dāng)一個模塊被描述成一個理論后，在PVS中的類型檢查必須執(zhí)行，以此來發(fā)現(xiàn)理論中不一致的類型聲明.當(dāng)對一個理論進行過類型檢查以及完成其所有猜測后，可認(rèn)為這一理論的所有工作就完成了.當(dāng)然，在PVS證明器中提供了許多不同概念的證明命令，如（induct“n“）是對于所證明公式中出現(xiàn)“n“時，運用數(shù)學(xué)歸納法進行自動推理證明；而（skolem?。┦怯脕硐鼺ORALL這一量詞的，等等.這些證明都是一步步通過人機交互式完成的，在證明過程中，證明器保留著所有證明的步驟，當(dāng)猜測證明完成后，會生成一棵類似樹一樣的證明過程圖，所有用到的命令都是其節(jié)點，所有的葉子部門，都認(rèn)為是正確的.

2 將E方法引入至PVS中

2.1 從E方法到PVS中的結(jié)構(gòu)轉(zhuǎn)換規(guī)則

為證明在B方法中所描述的性質(zhì)，由B方法所描述的系統(tǒng)必須轉(zhuǎn)換成PVS中的語言.轉(zhuǎn)換之間一一對應(yīng)的關(guān)系如表1所示.在這一轉(zhuǎn)換中，B方法中的MACHINE（抽象機）對應(yīng)PVS中的THEORY（理論）；INVARIANT（不變量）對應(yīng)TYPE（類型）；OPERATIONS（操作）轉(zhuǎn)換為PVS中的FUNCTIONS（函數(shù)）.B方法中的語義轉(zhuǎn)換為PVS中的語言.

2.2 轉(zhuǎn)換描述和實例

E方法

表1 E方法與PVS之間的轉(zhuǎn)換Tab.1 Conversion between E method and PVS

在PVS中，類型為t的元素所組成的集合以謂詞的方式出現(xiàn)，如一個由類型t至Boolean的函數(shù).集合給出的形式可以為［t！bool］，pred［t］，或setof［t］，給出的類型均是等價的.

舉例說明：

E方法 SETS BUS

E方法

此處將B方法中的性質(zhì)轉(zhuǎn)換成PVS中公理的形式.在使用公理前，必須進行證明，完成證明后，方可使用.

舉例說明：

E方法 PROPERTIES

此處可認(rèn)為1輛公共汽車中有乘客和司機.顯然，這兩類人都是自然數(shù)，且開在路上的公共汽車必須有司機.

此即為PVS所描述B方法中的性質(zhì).

E方法

在B方法中，不變量的使用是用來限制變量的.PVS中的類型聲明是引入一個新的類型［6］，且這一新類型將被后面的變量所用到.

舉例說明：

E方法

每一張票都有所對應(yīng)的價格，并且當(dāng)知道站數(shù)多少時，能夠得到相應(yīng)的PRICE（票價）即（ticket

在PVS中，首先定義TICKET這一類型，然后通過ticket這一變量使用它.

E方法

從某種意義上來講，OPERATIONS是一個抽象的概念，由使用者自己定義［7］，類似于在PVS中的函數(shù)，故決定在PVS中直接用函數(shù)去描述OPERATIONS.

上述為FUNCTIONS（函數(shù)）的3種基本形式，每一個ti都是一種類型描述［8］.但有時也用predicate（謂詞）定義FUNCTION（函數(shù)）.

舉例說明：

E方法

此處操作可以認(rèn)為，如果某一人上車后沒有買票，那么他必須買相應(yīng)的車票，之后集合has_ticket（記錄乘客與票價之間的集合）會記錄其行為.

在PVS中，has_ticket也是一個集合記錄乘客有沒有買票.而buy_ticket函數(shù)是判斷該乘客是否有買票的操作，如果乘客已經(jīng)買過票了，則has_ ticket集合保持不變，否則要求該乘客先行買票，之后將其加入已經(jīng)買過票的has_ticket集合中.

3 實例分析

以一個簡單的電梯控制系統(tǒng)為例，使用上述所提到的方法和理論.如在一棟有N部電梯的M層高的大樓里，每一部電梯都有一組按鈕來控制，按鈕與大樓的樓層相對應(yīng).電梯根據(jù)按鈕的操作執(zhí)行，只要對應(yīng)樓層的按鈕燈亮，電梯就往該層運行，當(dāng)運行至相應(yīng)樓層停靠后，按鈕燈滅.在大樓的樓道里，除底樓和最高樓層外，都有2個按鈕，對應(yīng)電梯往上和往下運行執(zhí)行請求.

3.1 E方法中的電梯控制系統(tǒng)描述

在電梯控制系統(tǒng)中有2個集合，分別用LIFT和DIERCTION（1個枚舉類型）描述電梯的集合以及表明電梯運行的方向.電梯控制系統(tǒng)中還包括2個常量，分別是top和ground表示頂層以及底樓.

VARIABLES和INVARIANT：

（1）變量moving表示運行中的電梯；

（2）對于每一部電梯l而言，如果l沒有在moving中，即l未處于運行狀態(tài)，都可以通過floor（l）得到其所處?？康南鄳?yīng)樓層；

（3）dir（l）表明的是電梯運行的方向，當(dāng)電梯運行時，dir（l）就是該電梯運行的方向，如果該電梯未運行，處于?？繝顟B(tài)，則dir（l）就是目標(biāo)方向或保留其最后狀態(tài)的方向；

（4）變量in是一個二元關(guān)系，對應(yīng)的是FLOOR（樓層）至DIRECTION（方向）的概念，當(dāng)（f，d）∈in，表明有人想從樓層f出發(fā)出往方向d執(zhí)行的請求；

（5）變量out也是一個二元關(guān)系，對應(yīng)的是LIFT（電梯）至FLOOR（樓層）的概念，當(dāng)（l，f）∈out時，表明有人想從LIFT（電梯）中到具體的FLOOR（樓層）的請求；

（6）不變量moving△（out∩floor）=，表明moving不會出現(xiàn)的情況是當(dāng)電梯l已經(jīng)停靠在具體樓層f時，還有人在電梯中，想要電梯l發(fā)出執(zhí)行至樓層f的請求，換言之，對于這樣的請求不予執(zhí)行；

（7）還要滿足一類情況是，雖然電梯已經(jīng)停靠在樓層f上了，但假使該電梯往上繼續(xù)執(zhí)行操作，這時樓道中的人按了往下執(zhí)行的請求，電梯不予理睬，而樓道中往下方向的按鈕燈不滅；對應(yīng)的B方法描述為：

OPERATIONS（操作）：電梯應(yīng)該有自己的操作方式，如有人在電梯l中按了去往f樓層的按鈕，定義為Request Floor（l，f）；當(dāng)然B方法中也有這樣的描述Request Lift（f，d），表明有人在樓層f，想要得到去往d方向的請求.

3.2 在PVS中抽象機的實現(xiàn)

在提到的轉(zhuǎn)換方法中，B方法中的電梯抽象機可以這樣被轉(zhuǎn)換引入到PVS的理論中，B方法中的SETS（集合）LIFT轉(zhuǎn)換成PVS中的SET（集合）.為了驗證某些性質(zhì)，稍對B方法進行一些精化.想證明以下2個重要的性質(zhì)概念：（Buttons）按鈕的實現(xiàn)和如何控制這些按鈕的狀態(tài)變化.故在PVS中，用到了recordtype（記錄類）這一概念，用來包含Buttons（按鈕）和Control（如何控制）之間的關(guān)系.具體地說，Buttons（按鈕）是所有的按鈕，包括電梯中所有樓層的按鈕，以及在樓道中，每一層的上、下請求的按鈕；而Control（控制）包含的是所有樓層的信息，電梯的移動以及電梯執(zhí)行的方向.使用記錄類型：Lift=［＃btns：Buttons，ctr：Control＃］.

在B方法中，不變量INVARIANT（ground｜→dn）εin并且（top｜→up）εin是為了限制這樣的需求：在底層沒有往下執(zhí)行的按鈕，同樣在頂層沒有往上執(zhí)行的按鈕.在PVS中，增加了2個新的類型：Up_floor和Down_floor，用來描述每一樓層確切的方向執(zhí)行請求.類型Up_floor定義了除了頂層外的每一層都有1個要求電梯往上執(zhí)行的請求，而類型Down_floor定義了除了底層外的每一層都有1個要求電梯往下執(zhí)行的請求.在B方法中變量moving轉(zhuǎn)換成了PVS中的枚舉類型Movement，表示電梯所處狀態(tài)，running（運行）或者h(yuǎn)alted（懸停）.

在B方法中，不變量out∈LIFT FLOOR表明的是在電梯內(nèi)部每一樓層的需求.而在PVS中，用［floor→boolean］描述在電梯中相應(yīng)樓層是否應(yīng)該?？康恼埱?B方法中抽象機OPERATIONS（操作）可以轉(zhuǎn)換成PVS的FUNCTIONS（函數(shù)），故Request_floor也相應(yīng)地轉(zhuǎn)換為PVS中的函數(shù).如有人在電梯中按下了任一樓層的按鈕，那么這一樓層的按鈕燈必須亮起，并且該電梯將立即或者不久將運行至該層?？?，以響應(yīng)該請求命令.

3.3 驗證性質(zhì)

由于篇幅所限，僅列出以下性質(zhì)的驗證：電梯一定會運行至相應(yīng)請求過的樓層.在PVS中，可以給出如下猜測：首先，對于任一樓層按鈕，發(fā)出請求后，都會有燈亮起；其次，電梯一定會在相應(yīng)樓層?？? response_push_floor：conjecture

使用命令（induct“f“）進行證明，會生成6個子目標(biāo).每個子目標(biāo)使用grind或ground都很容易證明，不做贅述.

4 結(jié) 語

本文根據(jù)2種形式化方法，B方法和PVS的特點，提出將B方法子集的一部分引入PVS中，給出了B方法語義到PVS語言的轉(zhuǎn)換規(guī)則.最后，對一個簡單的電梯控制系統(tǒng)，分別進行B方法和PVS語言描述，并根據(jù)上述轉(zhuǎn)換規(guī)則完成了驗證工作.由此表明，文中提出的轉(zhuǎn)換規(guī)則和方法的可操作性.B方法和PVS在形式化方法研究、系統(tǒng)檢測、檢驗證明等方面具有更加深入的研究價值，如何將B方法中更多部分引入到PVS中，將是后續(xù)工作的重點.

［1］ Owr S，Shankar N.Abstract datatypes in PVS［J］. Computer Science Laboratory，SRI International，1999，1（3）：308-309.

［2］ Pratten C H.An introduction to proving AMN specifications with PVS and the AMN-PROOF tool［J］. IRIN-IUT de Nantes，2002，5（2）：149-165.

［3］ Pilotto C，White J.Towards a verification framework for faulty message passing systems in PVS［J］.Innovations in Systems and Software Engineering，2011，7（2）：109-118.

［4］ 許慶國，繆淮扣.實時系統(tǒng)形式規(guī)格說明在PVS中的建立［J］.計算機科學(xué)，2006，33（12）：239-240.

［5］ Moscato M M，Pombo C G L，F(xiàn)rias M F.Dynamite：a tool for the verification of alloy models based on PVS［J］.ACM Transactions on Software Engineering and Methodology，2014，23（2）：100.

［6］ 李昊，張敏，王榕.基于PVS的數(shù)據(jù)庫安全策略形式化分析方法［J］.中國科學(xué)技術(shù)大學(xué)學(xué)報，2013，43（7）：591-598.

［7］ 唐宇.一種基于形式化B方法的軟件構(gòu)件模型［J］.天水師范學(xué)院學(xué)報，2009，29（2）：87-89.

［8］ 孫國棟，牛晉剛.超長整數(shù)運算的PVS規(guī)范與驗證［J］.計算機工程與應(yīng)用，2015，51（3）：93-94.

（編輯 呂丹）

Application of lntegrating B Method into PVS

LIU Mei
（School of Computer Science and Information Engineering，Shanghai Institute of Technology，Shanghai 201418，China）

A method to integrate the B method into prototype verification system（PVS）according to their characteristics was presented，which could convert a system described by B method into formal specification language of PVS.In this method，a machine in B method was expressed to be a theory in PVS，while an invariant to be a type in PVS.Some properties described by B method were transformed into conjectures of PVS language，then，these conjectures could be proved effectively by PVS prover.In the end，an example，a lift system controller，was given to illustrate the application of this method.

B method；prototype verification system（PVS）；formal method；lift system controller

TP 301.2

A

1671-7333（2015）04-0380-04

10.3969／j.issn.1671-7333.2015.04.014

2014-11-03

劉 梅（1968-），女，副教授，主要研究方向為數(shù)據(jù)庫理論及應(yīng)用，計算機課程教學(xué)方法.E-mail：liumei＠sit.edu.cn