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

馬 倩，段振華

（西安電子科技大學計算理論與技術研究所，陜西西安 710071）

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

馬 倩，段振華

（西安電子科技大學計算理論與技術研究所，陜西西安 710071）

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

時序邏輯；公理系統；定理證明；驗證

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

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

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

1 MSVL語言及其公理系統

1.1投影時序邏輯

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

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

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

1.2MSVL語句及其公理系統

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

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

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

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

2.1基本原理

2.2MSVL程序的PVS描述

MSVL程序的PVS描述包括MSVL語法和語義的PVS描述.語法的描述是用PVS規范語言定義所有MSVL表達式和語句，而語義的描述是用PVS規范語言表達MSVL的語義，包括狀態、區間和有效性等.

2.2.1MSVL語法的描述

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

表1　MSVL語句對應的PVS表示

2.2.2MSVL語義的描述

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

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

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

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

2.3MSVL程序的PVS證明

在MSVL程序的PVS描述基礎上，使用PVS規范語言描述MSVL的公理系統和待證定理，經過編譯和類型檢查后，輸入PVS證明命令對待證定理進行推演證明.

2.3.1公理系統的描述

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

利用PVS中定義的MSVL語句和PVS的AXIOM類型，對MSVL公理系統中所有的狀態公理和推理規則以及所有的區間公理和推理規則一一進行描述.例如，根據表1中MSVL語句的PVS表示，狀態公理（A3）可以表示為

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

其中，Pc和Ac是狀態公式.其他公理和規則的PVS描述都可類似得到.這樣，就得到了完整的MSVL公理系統的PVS描述.

2.3.2證明命令

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

3 應用實例——面包房算法

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

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

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

無窮:

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

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

4 結束語

筆者提出了一種基于定理證明器PVS的MSVL程序的自動定理證明方法.該方法使用PVS規范語言描述MSVL語言的語法、語義和公理系統，然后輸入PVS命令對MSVL程序進行驗證.面包房算法的實例展示了該方法的可行性.該方法對于其他時序邏輯程序設計語言的自動定理證明具有一定的借鑒意義.在未來研究中，要進一步提高該方法的自動化程度，并應用于更大更多的實例.同時，探討基于其他定理證明器，如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］.西安電子科技大學學報，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］.西安電子科技大學學報，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 網絡出版時間：2015-04-14

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

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

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

網絡出版地址：http://www.cnki.net/kcms/detail/61.1076.TN.20150414.2046.011.html