馬 倩，段振華

（西安電子科技大學(xué)計算理論與技術(shù)研究所，陜西西安 710071）

MSVL程序的自動定理證明方法

馬 倩，段振華

（西安電子科技大學(xué)計算理論與技術(shù)研究所，陜西西安 710071）

時序邏輯程序設(shè)計語言能被用于驗證C、Verilog/VHDL程序的正確性.但目前時序邏輯程序設(shè)計語言程序只能純手工進(jìn)行定理證明.針對該問題提出了一種基于定理證明器原型驗證系統(tǒng)的時序邏輯程序設(shè)計語言程序的自動定理證明方法.該方法首先使用原型驗證系統(tǒng)規(guī)范語言描述時序邏輯程序設(shè)計語言的語法和語義，使得原型驗證系統(tǒng)能夠正確識別時序邏輯程序設(shè)計語言程序；然后使用原型驗證系統(tǒng)規(guī)范語言描述時序邏輯程序設(shè)計語言的公理系統(tǒng)和待證定理；最后輸入原型驗證系統(tǒng)命令調(diào)用原型驗證系統(tǒng)證明器來進(jìn)行時序邏輯程序設(shè)計語言程序的推演證明.在證明過程中，細(xì)節(jié)被原型驗證系統(tǒng)自動地證明，使得人工僅在復(fù)雜的步驟上指導(dǎo)控制，從而實現(xiàn)半自動地驗證時序邏輯程序設(shè)計語言程序，簡化了該定理的證明過程.

時序邏輯；公理系統(tǒng)；定理證明；驗證

自動定理證明是一種利用計算機(jī)完全或部分代替人工進(jìn)行定理證明的方式.它克服了純?nèi)斯ぷC明方法易出錯、證明復(fù)雜等缺點，已成功應(yīng)用于數(shù)學(xué)定理的證明以及處理器、安全協(xié)議和程序驗證中.主要包括兩種方法:完全自動定理證明［1］和交互式定理證明［2］.完全自動定理證明雖然能夠使用計算機(jī)完全代替人工進(jìn)行自動推理，但是表達(dá)能力較弱、適用范圍有限.典型的定理證明器有ACL2和Otter等.交互式定理證明，也稱為半自動定理證明，表達(dá)能力強(qiáng)、靈活性高，能夠自動地證明瑣碎的細(xì)節(jié)，但對于一些復(fù)雜的證明需要人工參與指導(dǎo).典型的定理證明器有PVS、Coq和Isabelle等.特別地，原型驗證系統(tǒng)（Prototype Verification System，PVS）［3-4］是由斯坦福研究機(jī)構(gòu)開發(fā)的，主要由PVS規(guī)范語言和PVS證明器組成，提供了豐富的類型系統(tǒng)和強(qiáng)大的推理策略.

框架時序列邏輯語言（Modeling，Simulation and Verification Language，MSVL）［5］是一種基于投影時序邏輯（Projection Temporal Logic，PTL）［5］的可執(zhí)行語言，既能夠描述各種復(fù)雜的時序結(jié)構(gòu)，如順序、并發(fā)、非確定等，也能夠驗證各類性質(zhì)，如安全性、活性、周期性、區(qū)間相關(guān)性等.與其他時序邏輯程序語言［6］如操作時序邏輯（Temporal Logic of Actions，TLA）［7］、Tempura［8］相比，MSVL具有數(shù)據(jù)類型，同步和異步通訊語句，更加實用.目前時序邏輯程序設(shè)計語言的定理證明僅限于純手工驗證，沒有自動定理證明方法和機(jī)械化工具支持.當(dāng)待驗證系統(tǒng)較為復(fù)雜時，證明過程繁瑣且容易出錯.

針對該問題，筆者以MSVL為研究對象，探討了時序邏輯程序設(shè)計語言的自動定理證明方法，提出了一種基于定理證明器PVS的MSVL程序的交互式定理證明方法.該方法首先使用PVS規(guī)范語言描述MSVL語言的語法和語義，使得PVS能夠正確識別任何MSVL程序；然后使用PVS規(guī)范語言描述MSVL公理系統(tǒng)［9］和待證定理；最后輸入PVS命令調(diào)用PVS證明器來進(jìn)行MSVL程序的定理證明.在證明過程中，瑣碎的細(xì)節(jié)被系統(tǒng)自動地證明，使得人工僅在復(fù)雜步驟上指導(dǎo)控制，從而半自動地推演證明MSVL程序.

1 MSVL語言及其公理系統(tǒng)

1.1投影時序邏輯

MSVL的邏輯基礎(chǔ)是投影時序邏輯（PTL［5］）.令Prop表示原子命題的可數(shù)集合，V為靜態(tài)變量和動態(tài)變量的可數(shù)集合，D為任何數(shù)據(jù)類型的論域，N0為非負(fù)整數(shù)集合.投影時序邏輯的項e和公式P歸納定義如下:

其中，c∈D，為常量；v∈V，為動態(tài)或靜態(tài)變量；p∈Prop，為原子命題；P1，…，Pm及P，Q為PTL的合式公式；f（e1，…，em）與F（e1，…，en）分別表示函數(shù)與謂詞；?，∧，和=類似于經(jīng)典一階邏輯中的符號；○（下一狀態(tài)），Θ（前一狀態(tài)），+（加閉包）及prj（投影）是時序操作符.如果一個公式（項）不包含時序操作符，則稱該公式為狀態(tài)公式（項）；否則，稱它為時序公式（項）.

狀態(tài)s是一個賦值的序偶對（Ip，Iv）.對于任意v∈V，有s［v］=Iv［v］∈D∪｛nil｝，表示變量的值，其中nil表示未定義；對于任意p∈Prop，有s［p］=Ip［p］∈｛true，false｝.PTL的區(qū)間（即模型）σ=，是一個非空的狀態(tài)序列，其長度記為σ.若σ為有窮區(qū)間，則σ為狀態(tài)個數(shù)減1；否則，為ω.公式（項）的解釋是一個四元組I=（σ，i，k，j）（i，k∈N0，j∈N0∪｛ω｝，且0≤i≤k≤j≤σ），表示公式（項）在子區(qū)間σ（ij）上且當(dāng)前狀態(tài)是sk時的解釋.表達(dá)式e和公式P的語義解釋I［e］和I［P］可參照文獻(xiàn)［5］.如果（σ，0，0，σ）?P（簡記為σ?P）成立，則稱公式P是可滿足的；如果對于所有的區(qū)間σ，σ?P成立（簡記為?P），則稱P是有效的.

1.2MSVL語句及其公理系統(tǒng)

MSVL是可執(zhí)行的區(qū)間時序邏輯程序設(shè)計語言，集建模、仿真和驗證3種功能為一體.MSVL中表達(dá)式被看作PTL的項，語句被看作PTL的公式.MSVL語言的算術(shù)表達(dá)式e和布爾表達(dá)式b定義如下:

其中，m是整數(shù)，v是動態(tài)或靜態(tài)變量.MSVL語言由如下語句組成:空語句ε，next語句○P，合一語句x=e，正瞬時賦值語句x?e，賦值語句x∶=e，順序語句P；Q，合取語句P∧Q，并行語句P‖Q，always語句P，條件語句if b then P else Q，循環(huán)語句while b do P，選擇語句P∨Q，狀態(tài)框架語句lb f（x），區(qū)間框架語句frame（x），等待語句await（b），存在語句?x:P和投影語句（P1，…，Pm）prj Q.一些派生的MSVL語句定義如下:為了對MSVL程序進(jìn)行統(tǒng)一驗證，MSVL的公理系統(tǒng)［9］已被提出.它采用命題投影時序邏輯

圖1　基于PVS的MSVL程序的半自動定理證明方法

2 基于PVS的MSVL定理證明方法

2.1基本原理

2.2MSVL程序的PVS描述

MSVL程序的PVS描述包括MSVL語法和語義的PVS描述.語法的描述是用PVS規(guī)范語言定義所有MSVL表達(dá)式和語句，而語義的描述是用PVS規(guī)范語言表達(dá)MSVL的語義，包括狀態(tài)、區(qū)間和有效性等.

2.2.1MSVL語法的描述

使用PVS規(guī)范語言中的抽象數(shù)據(jù)類型（abstract datatype）來描述MSVL的表達(dá)式，將其定義為expression類型.其中，為方便表示，限定常量為整數(shù)，表示為const（n:int）:cst？；將動態(tài)和靜態(tài)變量分開，分別表示為variable（v:nat）:vr？和svariable（sv:nat）:svr？；下一狀態(tài)○表示為O（e:expression）:nx？；前一狀態(tài)Θ表示為preO（e1:expression）:prev？；算術(shù)運算表示為op（ex1，ex2:expression，optype: arithmetic）:op？.這樣就能表示MSVL中的所有表達(dá)式.謂詞vr？，nx？等表示expression類型的子類型.例如x:（vr？）聲明x是一個動態(tài)變量.

表1　MSVL語句對應(yīng)的PVS表示

2.2.2MSVL語義的描述

為了描述區(qū)間，首先使用theory和record類型定義序列sequ.將sequ表達(dá)為任意類型S的theory，使得它不僅可以描述狀態(tài)的序列，也可以描述其他類型的序列，如整數(shù)序列等.進(jìn)一步，使用record類型［#…#］，將sequ細(xì)化為三元組:第1元是布爾類型bool，指示序列是有窮或者無窮，如果為真，則序列是無窮的，否則序列是有窮的；第2元是大于等于-1的整數(shù)，表示序列的長度；第3元是數(shù)組類型，映射整數(shù)下標(biāo)到其所指示的具體元素S.

接著，使用tuple類型定義狀態(tài)為state類型，即state:TYPE=［［prop→bool］，［vars→Value］，［svars →Value］］.它包含3個函數(shù)分量:第1分量是從原子命題prop到布爾類型bool的映射；第2分量是從動態(tài)變量vars到整數(shù)Value的映射；第3分量是從靜態(tài)變量svars到整數(shù)Value的映射.由于區(qū)間是狀態(tài)的序列，因此區(qū)間可以定義為Interval類型，即Interval:TYPE=sequ［state］.

在表達(dá)式e和公式P的語法結(jié)構(gòu)上定義遞歸函數(shù)來描述PTL的語義解釋I［e］和I［P］.表達(dá)式e的語義函數(shù)為E（e）（sigma，i，j，k），將表達(dá)式e映射為Value類型；而公式P的語義函數(shù)為M（P）（sigma，i，j，k），將公式P映射為bool型.這里，e為expression類型；P為form類型；sigma是Interval類型；i是len i （sigma）類型，表示小于等于sigma長度的非負(fù)整數(shù)；j是len j（sigma，i）類型，表示大于等于i且小于等于sigma長度的非負(fù)整數(shù)；k是len k（sigma，i，j）類型，表示大于等于i且小于等于j的非負(fù)整數(shù).實際上，（sigma，i，j，k）描述了語義中的解釋I=（σ，i，k，j）.限于篇幅，將它們的詳細(xì)PVS描述略去.

MSVL公式的有效性?可描述為從form類型的公式f到bool類型的映射:

2.3MSVL程序的PVS證明

在MSVL程序的PVS描述基礎(chǔ)上，使用PVS規(guī)范語言描述MSVL的公理系統(tǒng)和待證定理，經(jīng)過編譯和類型檢查后，輸入PVS證明命令對待證定理進(jìn)行推演證明.

2.3.1公理系統(tǒng)的描述

MSVL公理系統(tǒng)中使用PPTL作為性質(zhì)規(guī)范語言，因此需要在PVS中描述PPTL公式.由于PPTL也是PTL的子集，因此類似于MSVL語句的定義，可以使用子類型來定義PPTL公式.公理系統(tǒng)中的推演關(guān)系|—和正確性斷言｛σk，A｝ P ｛σh，B｝在PVS中分別表示為|—（f）和H（sigma）（k，A）（P）（h，B）.其中|—將form類型公式f映射為bool類型，而H將三元組映射為bool類型.

利用PVS中定義的MSVL語句和PVS的AXIOM類型，對MSVL公理系統(tǒng)中所有的狀態(tài)公理和推理規(guī)則以及所有的區(qū)間公理和推理規(guī)則一一進(jìn)行描述.例如，根據(jù)表1中MSVL語句的PVS表示，狀態(tài)公理（A3）可以表示為

再如，區(qū)間公理（APC）可以表示為如下形式:

其中，Pc和Ac是狀態(tài)公式.其他公理和規(guī)則的PVS描述都可類似得到.這樣，就得到了完整的MSVL公理系統(tǒng)的PVS描述.

2.3.2證明命令

將待證定理表達(dá)為theorem或者lemma類型，然后調(diào)用PVS證明器進(jìn)行證明.在證明過程中，根據(jù)定理的形式，選擇與待證定理語法結(jié)構(gòu)相對應(yīng)的MSVL公理和規(guī)則，并通過輸入相應(yīng)的PVS命令將該公理或規(guī)則應(yīng)用于待證定理，使得定理得到進(jìn)一步推導(dǎo).例如，輸入命令“（lemma“APC”）”可以引入公理（APC）作為前提；輸入命令“（use“A4”）”可以引入公理（A4），且將其實例化后作用于當(dāng)前定理.在使用PVS命令對MSVL程序進(jìn)行驗證的過程中，常用的命令有bddsimp，assert，inst？，expand，use，lemma，skolem！，forward-chain等等.對于復(fù)雜的證明步驟，如歸納，由于不同類型的變量需要不同的歸納策略和歸納謂詞，因此不能完全自動化，需要人工考慮證明策略.而對于一些瑣碎的證明細(xì)節(jié)，如命題、等詞和算術(shù)的推理等，由于PVS證明器中內(nèi)置了相關(guān)的判定算法和自動重寫技術(shù)，因此可以自動地化簡.通過這種方式就實現(xiàn)了基于PVS的MSVL程序的自動定理證明，同時也得到了一個支持全部MSVL語言的定理證明工具.

3 應(yīng)用實例——面包房算法

面包房算法［12］是一個經(jīng)典的用于協(xié)調(diào)多進(jìn)程并發(fā)獲取臨界資源的進(jìn)程互斥算法，由Lamport于1974年提出.該算法假設(shè)每個進(jìn)程都有惟一的進(jìn)程號.當(dāng)進(jìn)程想要獨占地訪問臨界資源時，必須先獲得一個序列號，然后按照序列號的大小，由小到大依次訪問臨界資源.也就是說，擁有最小序列號的進(jìn)程擁有優(yōu)先權(quán)，可以先訪問臨界資源.當(dāng)兩個進(jìn)程擁有相同的序列號時，進(jìn)程號小的進(jìn)程擁有優(yōu)先權(quán).該算法滿足進(jìn)程互斥、無死鎖和先來先服務(wù)等性質(zhì).隨著算法的執(zhí)行，進(jìn)程序列號不斷增大，使得狀態(tài)空間無窮，不能采用一般的模型檢測方法［13］進(jìn)行驗證.下面以兩個進(jìn)程的面包房算法為例，對進(jìn)程互斥性質(zhì)進(jìn)行驗證以展示上節(jié)提出的方法的可行性.對于其他多個進(jìn)程的實例和其他性質(zhì)，驗證方法是類似的.

兩進(jìn)程實例的MSVL程序P如下所示，其中yi（i=1，2）是自然數(shù)，表示進(jìn)程i的序列號；At?cri指示進(jìn)程i是否正在訪問臨界資源，如果為1，表示進(jìn)程i正在訪問臨界區(qū)；如果為0，則表示沒有訪問.

該算法的安全性，即任何時刻最多只有一個進(jìn)程能夠訪問臨界資源的進(jìn)程互斥性，可以描述為PPTL公式:□（p1∧p2），其中p1表示At?cr1=1，p2表示At?cr2=1.因此，需要證明三元組｛σ0，（p1∧p2）｝ P ｛σw，true｝成立.它在PVS中可以表達(dá)為如下Bakery定理，其中sigma1是無窮區(qū)間，omega表示

無窮:

啟動PVS證明器，輸入合適的PVS命令進(jìn)行半自動證明.圖2（a）展示了面包房算法證明過程中產(chǎn)生的部分圖形化的證明樹，其中每個“|—”表示待證目標(biāo)，下方的命令為施加到該待證目標(biāo)上的PVS命令.圖2 （b）展示了證明結(jié)束時PVS系統(tǒng)的狀態(tài).在證明結(jié)束時，PVS在下方的*pvs*區(qū)域里顯示結(jié)束信息.由“Bakery.4”字樣可知，在驗證過程中自動產(chǎn)生4個子目標(biāo)，只有當(dāng)這4個子目標(biāo)都成功得到證明時，整個Bakery定理證明才算完成.“Q.E.D”字樣表明定理證明完畢，Bakery算法滿足進(jìn)程互斥性質(zhì).同時，總的驗證時間為55.26 s，且PVS證明器自動證明時間為15.61 s.

圖2　面包房算法的定理證明圖示

4 結(jié)束語

筆者提出了一種基于定理證明器PVS的MSVL程序的自動定理證明方法.該方法使用PVS規(guī)范語言描述MSVL語言的語法、語義和公理系統(tǒng)，然后輸入PVS命令對MSVL程序進(jìn)行驗證.面包房算法的實例展示了該方法的可行性.該方法對于其他時序邏輯程序設(shè)計語言的自動定理證明具有一定的借鑒意義.在未來研究中，要進(jìn)一步提高該方法的自動化程度，并應(yīng)用于更大更多的實例.同時，探討基于其他定理證明器，如Coq，的MSVL程序的自動定理證明方法.

［1］de BOER F，BONSANGUE M，ROT J.Automated Verification of Recursive Programs with Pointers［C］//Lecture Notes in Computer Science:7364 LNAI.Heidelberg:Springer Verlag，2012:149-163.

［2］BERTOT Y，CASTéRAN P.Interactive Theorem Proving and Program Development［M］.Berlin:Springer Verlag，2004.

［3］OWRE S，SHANKAR N，RUSHBY J M，et al.PVS Language Reference［EB/OL］.［2014-09-10］.http://www. docin.com/p.454926227.html.

［4］NERON P.Square Root and Division Elimination in PVS［C］//Lecture Notes in Computer Science:7998 LNCS. Heidelberg:Springer Verlag，2013:457-462.

［5］DUAN Z.Temporal Logic and Temporal Logic Programming［M］.Beijing:Science Press of China，2006.

［6］TANG C S.A Temporal Logic Language Oriented toward Software Engineering-Introduction to XYZ System（I）［J］. Chinese Journal of Advanced Software Research，1994，1（1）:1-27.

［7］LAMPORT L.The Temporal Logic of Actions［J］.ACM Transactions on Programming Language and Systems，1994，16（3）:872-923.

［8］MOSZKOWSKI B.Executing Temporal Logic Programs［D］.Cambridge:Cambridge University，1986.

［9］YANG X，DUAN Z，MA Q.Axiomatic Semantics of Projection Temporal Logic Programs［J］.Mathematical Structures in Computer Science，2010，20（5）:865-914.

［10］張南，段振華.進(jìn)位保留加法器的命題投影時序邏輯組合驗證［J］.西安電子科技大學(xué)學(xué)報，2012，39（5）:192-196. ZHANG Nan，DUAN Zhenhua.Compositional Verification of a Carry-save Adder with the Propositional Projection Temporal Logic［J］.Journal of Xidian University，2012，39（5）:192-196.

［11］逄濤，段振華，劉曉芳.Verilog程序的命題投影時序邏輯符號模型檢測［J］.西安電子科技大學(xué)學(xué)報，2014，41（2）:79-84. PANG Tao，DUAN Zhenhua，LIU Xiaofang.Symbolic Model Checking of Verilog Programs with The Propositional Projection Temporal Logic［J］.Journal of Xidian University，2014，41（2）:79-84.

［12］LAMPORT L.A New Solution of Dijkstra’s Concurrent Programming Problem［J］.Communications of the ACM，1974，17（8）:453-455.

［13］DUAN Z H，TIAN C，YANG M F，et al.Bounded Model Checking for Propositional Projection Temporal Logic［C］// Lecture Notes in Computer Science:7936 LNCS.Heidelberg:Springer Verlag，2013:591-602.

（編輯:王 瑞）

Automatic theorem proving technique for MSVL

MA Qian，DUAN Zhenhua
（Research Inst.of Computing Theory&Technology，Xidian Univ.，Xi’an 710071，China）

The MSVL is a temporal logic programming language.It can be used to verify C，Verilog/ VHDL programs.To do so，a program written in C or Verilog/VHDL is translated to an MSVL program，and then the task is changed to verify MSVL programs.However，at present，the correctness of MSVL programs can only be proved by hand with deductive approaches.This is tedious and error-prone.To handle this problem，an automatic theorem proving technique for the MSVL based on the interactive theorem prover PVSis proposed.To this end，first the syntax and semantics of the MSVL are described in the specification language of PVS，which enables MSVL programs to be correctly recognized by PVS.Further，an axiomatic system of the MSVL and some theorems are specified.Then the proof commands of PVS are input for invoking the PVS prover to deduce MSVL programs.During verification，simple details can be proved by PVS automatically while complex steps are controlled by human.In this way，MSVL programs can be verified semi-automatically，which facilitates the deduction of MSVL programs.An instance of the bakery algorithm is given to show that our method is feasible.

temporal logic；axiomatic system；theorem proving；verification

TP301

A

1001-2400（2016）01-0075-07

10.3969/j.issn.1001-2400.2016.01.014

2014-09-29 網(wǎng)絡(luò)出版時間：2015-04-14

國家自然科學(xué)基金資助項目（61133001，61272117，61202038）

馬 倩（1987-），女，西安電子科技大學(xué)博士研究生，E-mail:qma@mail.xidian.edu.cn.

段振華（1948-），男，教授，E-mail:zhhduan@mail.xidian.edu.cn.

網(wǎng)絡(luò)出版地址：http://www.cnki.net/kcms/detail/61.1076.TN.20150414.2046.011.html