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