资源描述：
《并发系统性质验证的一种形式化方法》由会员上传分享，免费在线阅读，更多相关内容在教育资源-天天文库。
1、第16卷第3期重庆师范学院学报(自然科学版)1999年9月Vol.16No.3JournalofChongqingTeachersCollege(NaturalScienceEdition)Sep.1999并发系统性质验证的一种形式化方法张广泉(重庆师范学院数学与计算机科学系,重庆,400047)摘要:采用Manna和Pnueli提出的命题线性时态逻辑PLTL作为并发系统的形式化规约语言,用PLTL公式描述系统的性质,给出并发系统性质验证的一种模型检验算法。关键词:并发系统;程序验证;命题线性时态逻辑;模型检验
2、算法中图分类号:TP311文献标识码:A文章编号:1001-8905(1999)03-0001-05程序的正确性是衡量一个程序质量优劣的首要标准,这是因为只有正确的程序才可能满足问题需求和达到预期效果和目标。目前保证程序的正确性主要有两种手段:测试(test)和验证(verification)。众所周知,测试只能表明程序中存在错误,而不能表明程序中没有错误(E.W.Dijkstra)。程序验证是研究如何使用数学方法,严格证明一个程序的正确性,这也是形式化方法所要解决的核心问题。目前程序验证方法已有很多,主要可分
3、为两类:演绎证明和模型检验。演绎证明方法主[1]要基于逻辑和代数等数学工具,其典型代表分别是Hoare逻辑公理化方法和代数归纳法;笔者在文[2]中给出一种推广的代数归纳法用于顺序递归程序的验证,但是传统的演绎证明(如Hoare逻辑等)方法有较大的局限性,仅适于顺序和确定性程序的验证,而不适于并发和非确定性程序的验证。由于并发程序要比顺序程序复杂得多,其正确性验证尤为重要,目前[3,4]一个重要的并发程序验证方法就是模型检验(model-checking),这是一种形式化确认(validation)方法。具体步骤
4、是:先给出系统(功能)一种形式化描述,然后构造一种算法来检验系统的(实现)模型是否满足系统的形式化描述。模型检验方法最初由E.M.Clarke和E.[3]A.Emerson于1981年提出的,他们用有穷状态转换图(即有穷状态机FSM)作为并发系统的计算模型,用分支时态逻辑CTL描述并发系统的性质,然后构造一种模型检验算法,通过穷尽状态空间以判定CTL公式在有穷状态转换系统是否有效。本文采用Manna和Pnueli提出的一种线性时态逻辑PLTL作为并发系统的形式化规约[5][6～8]语言,用PLTL公式描述系统的
5、性质(安全性、活性等),给出并发系统性质验证的一种模型检验算法。1PLTL模型检验算法为了检验一个时态公式φ在一有穷状态系统P上是否P—有效?即给定一个程序P和收稿日期:1998-07-23作者简介:张广泉(1965-),男,江苏连云港人,重庆师范学院数学与计算机科学系副教授,博士。主要从事软件形式化技术,非经典逻辑及应用等方面研究。2重庆师范学院学报(自然科学版)第16卷一个时态公式φ,φ是否在P的所有计算上均成立?要解决此问题,首先要解决与之相关的一个问题,即P-可满足问题。即给定一个程序P和一个时态公式φ
6、,是否存在P的一个计算满足φ?显然,公式φ是P-有效的,当且仅当φ不是P-可满足的。因而,如果能给出检验P-可满足的一个有效算法,则P-有效性问题也随之得到解决。为了检验公式φ的P-可满足性,我们采用Tableau表格方法。即对一个公式ψ,可构造相应的表Tψ,这里Tψ是一个有向图,其结点是ψ的原子,原子A和B之间有一条有向边当且仅当A和B满足条件R★、R★、R★。算法1步骤1、2给出程序P的状态转换图GP的构造方法;算法1步骤3、4给出Tψ的构造方法;当构造了表Tψ后,应该删去一些从初始φ-原子不可达的无用原子
7、,算法1步骤6给出Tψ表的修剪方法;接着,再构造(P,φ)的行为图B(P、φ),用于遍历程序P的状态转换图GP和表Tφ,算法1步骤6、7、8给出B(P、φ)及其极大强连通子图S1,…,St的构造过程;步骤9、10步判断是否存在合适子图Si,若存在,则程序P有一个计算满足时态公式φ。1.1模型检验算法算法1步骤1将所有满足初始条件Θ的状态作为GP的结点;步骤2重复步骤(1),直到没有新结点或新边加入GP;(1)设S∈GP,S1,S2,…,Sk是S的后继,则从S到Si画一条(有向)边加入GP,i=1,…,k步骤3ψ
8、的原子作为Tψ的结点;步骤4原子A和B之间有一条有向边当且仅当A和B满足下列三个条件R★、R★、R★:R★:对每一★p∈Υψ,★p∈A当且仅当p∈BR★:对每一★p∈Υψ,p∈A当且仅当★p∈BR★:对每一★p∈Υψ,p∈A当且仅当★p∈B步骤5重复步骤(1),(2),直到没有极大强连通子图(MSCS)被删除;(1)删去一个从初始ψ-原子不可达的MSCS;(2)删去一个不满足要求的终止
