（计算机软件与理论专业论文）框架时序逻辑程序设计解释器及模型检测工具.pdf

摘要 本文主要讨论一个框架时序逻辑程序设计语言f t l l ( f r a m e dt e m p o r a ll o g i c p r o g r a m m i n gl a n g u a g e ) 的解释器及一个基于命题投影时序逻辑p p t l ( p r o p o s i t i o np r o j e c t i o nt e m p o r a ll o g i c ) 进行性质描述的模型检测工具的实现。 文中首先介绍了实现解释器的基于范式的基本方法，然后给出了解释器的基本框 架并详细说明了各个模块的功用。此外还对f t l l 中几个重要的结构的实现做了详 细说明，包括框架、等待、投影、指针等操作。作为该解释器应用，它可以作为 由o w l - s 描述的抽象模型的模拟器，文中给出了一个详细的例子。 随后，本文介绍了用f t l l 为系统建模，p p t l 进行性质描述，然后分别将系 统和性质的非转换为各自的范式，接着对范式求交，并找它们的模型，看能否找 到反例，从而进行模型检测的方法。并介绍了一个以此实现的模型检测工具，并 给出了算法和一个例子。文章最后回顾了现有的模型检测工具。 关键词：时序逻辑投影解释器模型检测 a b s t r a c t t h i st h e s i sm a i n l yd i s c u s s e st h ei m p l e m e n t a t i o no fa ni n t e r p r e t e rf o rf r a m e d t e m p o r a ll o g i cp r o g r a m m i n gl a n g u a g e ( f 1 l l ) a n d am o d e lc h e c k e rw i t hp r o p o s i t i o n p r o j e c t i o nt e m p o r a ll o g i c ( p p t l ) s p e c i f y i n gt h ep r o p e r t i e so ft h es y s t e m t h eb a s i c a p p r o a c hu s i n gn o r m a lf o r mt h e o r y i sp r e s e n t e df i r s t l y t h e n ，t h es t r u c t u r eo ft h e i n t e r p r e t e ri s d i s c u s s e da n de a c h o fi t sm o d u l e si se x p l a i n e d i np a r t i c u l a r , t h e i m p l e m e n t a t i o na p p r o a c h e so fs e v e r a li m p o r t a n tc o n s t r u c t s i n c l u d i n gf r a m e , a w a i t , p r o j e c t i o na n dp o i n t e r a r eg i v e n a sa na p p l i c a t i o n ，t h ei n t e r p r e t e ri su s e da st h e s i m u l a t o ro fs e r v i c em o d e l so fo w l - sw e bs e r v i c ec o m p o s i t i o n s u b s e q u e n t l y , t h i st h e s i ss h o w sam o d e lc h e c k i n gm e t h o d i tm o d e l st h es y s t e m w i t hf r l la n ds p e c i f i e st h ep r o p e r t i e sw i t hp p t la f t e rt r a n s f o r m i n gt h es y s t e ma n d t h en e g a t i o no ft h ep r o p e r t i e st ot h e i rn o r m a lf o r m s ，i tu n i t e st h e mt os e ew h e t h e rt h e r e a r ec o u n t e r - e x a m p l e s t h ea l g o r i t h ma n da ne x a m p l ea r eg i v e ni ns u c c e s s i o n f i n a l l y , t h i st h e s i sr e v i e w st h ee x i s t i n gm o d e lc h e c k e r s k e y w o r d s ：t e m p o r a ll o g i c p m j e c t i o ni n t e r p r e t e r m o d e lc h e c k i n g 创新性声明 本人声明所呈交的论文是我个人在导师指导下进行的研究工作及取得的研究 成果。尽我所知，除了文中特别加以标注和致谢中所罗列的内容以外，论文中不 包含其它人已经发表或撰写过的研究成果；也不包含为获得西安电子科技大学或 其它教育机构的学位或证书而使用过的材料。与我一同工作的同志对本研究所做 的任何贡献均已在论文中做了明确的说明并表示了谢意。 申请学位论文与资料若有不实之处，本人承担一切相关责任。 本人签名：圣幺治 日期上& 鱼 关于论文使用授权的说明 本人完全了解西安电子科技大学有关保留和使用学位论文的规定，即：研究 生在校攻读学位期间论文工作的知识产权单位属西安电子科技大学。本人保证毕 业离校后，发表论文或使用论文工作成果时署名单位仍然为西安电子科技大学。 学校有权保留送交论文的复印件，允许查阅和借阅论文；学校可以公布论文的全 部或部分内容，可以允许采用影印、缩印或其它复制手段保存论文。( 保密的论 文在解密后遵守此规定) 本学位论文属于保密，在一年解密后适用本授权书。 本人签名： 。一? ：8 ” 导师签名： !1 醚： h + 由_ | ? ： j r 第一章绪论 第一章绪论 1 1 研究背景 随着各种计算机系统设计复杂度的提高，系统设计的正确性已成为问题的关 键。目前在系统的开发过程中，系统的验证在整个系统的开发时间和经费上所占 比重越来越大，而在设计阶段的后期才发现系统的错误会造成时问和经费的巨大 浪费。例如奔腾5 8 6 芯片中的除法运算错误是在大量进入市场后被一位用户发现 的，虽然这种错误发生的概率为几亿分之一。这个设计错误为i n t e l 公司造成四亿八 千万美元的经济损失。 保证系统正确性的途径是多方面的。首先对系统的需求分析要全面而准确， 不能有任何实质性的漏洞，以产生正确的系统规范，建立系统准确的模型。确认 系统实现的正确与否的主要途径是通过反复的模拟。但是模拟只能用典型的情况 对系统进行考察。对系统进行穷尽的模拟是不可能的。在大型系统中，要模拟系 统完全的行为可能要连续运行多年时间，这显然是不实际的。 测试是保证设计正确性的另一个手段。对硬件系统的测试是在加工后进行的； 对软件系统的测试是在编码后进行的。但是测试只能证明错误存在而不能证明错 误的不存在。对于复杂的系统，进行穷尽的测试也是不可能的。现在人们普遍认 为随机测试也不能完全解决问题。其他提高可靠性的方法有设计冗余表决系统， 即用多个同样的系统同时工作并进行表决；多个设计队伍同时设计同一系统如软 件的多版本方法等也可以提高可靠性。但是所有现有的办法都只能在一定程度上 有效。 形式化方法提供了保证设计正确性的另一条重要途径。它用数学方法表达系 统的规范或系统的性质，并且根据数学理论来证明所设计的系统满足系统的规范 或具有所期望的性质。在不能证明所期望的性质时，则可能发现设计错误。在系 统设计中，从系统的设计规范到系统的最后实现，在设计的每个阶段，都用形式 化的方法对该设计阶段的设计进行验证，尽可能地在每个设计阶段发现错误，及 时地更正，避免将设计错误引入下一个设计阶段。实践证明，形式化方法确实通 过形式规范和证明增强了对系统的理解从而发现了设计错误，或者通过形式化的 自动验证发现了用其他方法不能发现的设计错误。近年来，形式化方法越来越显 示出其优越性。 1 2 形式化验证 形式化验证是形式化方法的一个重要方面之一，是目前计算机领域的前沿课 2 框架时序逻辑程序设计解释器及模型检测工具 题之一。它是用数学的方法对设计的系统进行分析，以便完备地证明系统具有需 要的性质。一般来说，形式化验证可分为模型检验【2 5 】和定理证明方法。 1 2 1 模型检验 基于一种分支时序逻辑即计算树逻辑c t l ( c o m p u t a t i o nt r e el o g i c ) 1 2 0 , 2 1 j 和有限状态机f s m ( f i n it es t a t em a c h i n e ) 的模型检验的基本思想是用f s m 表示 系统的状态转移的有限结构，把用户所希望的系统的特性用c - - 7 f l 公式表示出来，通 过遍历f s m 来检验c t l 公式的正确性。随着程序或电路规模的增大，状态数目将呈 指数增加而引起组合爆炸。8 0 年代术，又发展了二叉决策图b d d ( b i n a r yd e c i s i o n d i a g r a m ) 1 2 9 1 矛d 符号模型检验技术。符号模型检验的含义是用一个御尔公式表示使 它满足的所有状态，状态的转移关系也用布尔公式表示，而布尔公式则以压缩方 式存储在b d d 中。通过适当排列变量的顺序可以大大简化b d d 的结构，这使得模型 检验可以处理大规模的数据结构和控制结构，从而缓和了组合爆炸的问题。模型 检验已被用于验证大量的实际设计。近年来模型检验的应用急剧扩大。除了硬件 设计之外，还包括i e e e 的标准的验证、各种协议验证、大型通讯软件验证。 1 2 2 定理证明器 我们可以将系统及其性质用基于某种逻辑的形式化系统中的一些公式表示以 该形式化系统的公理和推理规则为基础，可以逐步推导出表达系统性质的公式， 从而证明设计的系统具有该性质。当然推导过程中往往需要反映模型的假设条件 的定义和引理。如果我们利用一个计算机程序来辅助手工推导过程，这个计算机 程序可以称为定理证明器。它与自动机定理证明器之间构成了自动化程度不同的 定理证明器，如交互定理证明器和证明检验器。 早期的定理证明技术主要用于软件验证，但目前在硬件验证方面均取得显著 成就。例如著名的基于高阶逻辑的系统p v s 是由美国s r i 开发的一个原型验证系统， 原型可以是软件、硬件或通讯协议，证明的自动化程度较高。同时还有用于验证 r o c k w e l li n t e r n a t i o n a l 的在航空工业中使用的流水线处理器a a m p 5 。a a m p 5 是 r o c k w e l l 公司内部使用的微处理器。p v s 用来验证其微程序是否正确地实现了有代 表性的指令集，从中发现了四个设计错误。其中两个是真正的错误。在另外两个 故意设置的错误中，其中一个是前期设计经制造后被发现而故意保留的，另一个 是专门设置的错误，这个错误用模拟和测试都是难以发现的。 1 2 3 形式化综合 形式化综合是保证设计正确性的另一条途径。通常意义下的形式化验证是指 第一章绪论 3 综合后的验证。综合前验证则是指对自动综合工具的验证，这实际上是软件系统 的验证问题。一个自然的想法是在综合过程中同时进行形式化验证，这个过程就 是形式化综合。形式化综合一般利用一种逻辑系统从设计规范开始推演或通过一 系列变换得出设计结果。在形式化综合中，只允许使用j 下确性保留变换规则。 全自动的形式化综合工具是人们追求的目标，但要达到这个目标的路还很长。 交互式形式化综合工具是目前发展的主流。如何使用变换规则并指导综合过程是 形式化综合工具能否实用化的关键。只有把那些高深的逻辑定理和演算隐藏在简 单易学的用户界面之后，才能使形式化综合工具为广大用户所接受。 目前，形式化验证在一些著名的大学和大公司都有相应的研究机构，如美国 的s t a n df o r d ，h a r v a r d 等著名大学在这方面有许多成果。在闩本，英国和欧洲也有 不少研究人员从事形式化方面的研究，近些年来，也开发出了一些成熟的验证工 具。依靠不同的数学理论，形式化验证也有不同的分支，主要有四个方向：基于 逻辑的验证，包括时序逻辑，一阶逻辑，高阶逻辑；基于自动机理论的验证；基 于p e t r i 网理论的验证和基于过程代数的验证。 1 3 时序逻辑 时序逻辑又称时态逻辑、时间逻辑等，最初产生于哲学和语言学，它是由模 态逻辑演变而来的。在模型检测方法中，时序逻辑作为一种规范语言已广泛地应 用于数字电路系统【1 2 , 1 4 , 2 7 , 2 8 】，软件工程【6 】等领域的形式化验证中。将时间因素引入 模态逻辑，将口解释为“将来永远 ，解释为“将来会 ，便得到时序逻辑的极 小系统，它是由a n p r i o 于1 9 5 5 年在“d i o d o r a mm o d a l i t i e s ”一文中首先提出的。 继p r i o r 之后，许多逻辑学家对时序逻辑进行过研究，并提出各种不同的时序逻辑 系统，它们均是极小系统的扩充，按照时间模型大致可分为三类：线性时序逻辑、 分支时序逻辑和区间时序逻辑。在各种各样的时序逻辑中，以a p n u e l i 和z m a n n e 的线性命题时序逻辑l p t l ( l i n e a rp r o p o s i t i o nt e m p o r a ll o g i c ) 和e c l a r k e 和 e e m e r s o n 的分支时序逻辑，也称计算树逻辑c t l ( 最具有代表性。在线性时序逻 辑中，时间被看成是线性的，每个时刻有且只有一个后继。在分支时序逻辑中， 时间被看成是分支的，即每个当前时刻有多个未来时刻。这两种逻辑在形式化方 法研究中占有重要的地位，在这两种时序逻辑的基础上，又派生出其它的时序逻 辑。 线性命题时序逻辑在1 9 7 7 年首先由a p n u e l i 和z m a n n e r 引入到计算机科学 中，用于描述并发性和反应式系统的特性。作为一种描述系统特性的语言，u ，t l 可以方便地表示这类系统的安全性( 即坏的事件永不出现) 和活性( 即好的事件 终会发生) 。 4 框架时序逻辑程序设计解释器及模型检测工具 研究时序逻辑的方法同其它逻辑一样，包含了语法和语义两个方面。语法方 面主要是研究l p t l 的推理系统，有代表性的基于l p t l 的推理系统是s t a n d f o r d 的s t e p 系统和中科院的x y z 系统。即将要证明的系统及其性质用基于l p t l 的 形式表示出来，以该形式化系统的公理和推理规则为基础，逐步推导出表达系统 性质的公式，从而证明设计的系统具有该性质，在证明的过程中允许人和机毛交 互。这两个系统既可以证明软件的正确性，也可以证明一定规模的硬件设计。但 是由于定理证明器中的定理有限加之需要人工干涉才能完成。这样用户必须对全 部设计都要非常了解并且具有很好的数学功底。这些缺点限制了这些系统的实际 应用。 l p t l 的语义是检验在一个特定的模型中公式的真值情况，把这种方法称为是 模型检验。在这里的模型是指系统的一种实现方式，它本质匕是一个状态转移图， 状念转移图实际上与有限状态自动机的结构非常相似，我们只需要经过一定的变 换就可以将它转换成自动机。状态转移图可能构成所要横坐标公式的模型，图的 状态的标号是子公式集合。 从语义上研究l p t l 是一个非常活跃的领域，它的优点是所研制的工具完全 是自动化的。如果系统不满足给定的性质，模型检验系统可以给出反倒，从而帮 助设计人员找出设计错误。这一点可能它的最有吸引力之处，因此模型检验比定 理证明在形式化验证更加受到实际设计人员的欢迎。研究表明jl p t l 公式的模型 检验是p s p a c e 问题。基于语义的l p t l 系统有s p i n ，s p i n 是一个采用偏序方法 实现的模型检测工具，可以验证用p r o m e l a 语言描述的程序的正确性。 随着自动机理论的扩充，表示实时系统的特性的时序逻辑语言相应地做了扩 展，使它们能定量地描述表示系统的时间特性。早在八十年代，b m o s z k o w s k i 就 提出了用1 t i x i n t e r v a lt e m p o r a ll o n c ) 定量的表示数字电路的时间特性，但丌l 是 在离散的时问中解释时序逻辑公式的。类似的时序逻辑还包括m t l ( m e t r i c t e m p o r a ll o g i c ) ，t p t l ( t i m e dp r o p o s i t i o nt e m p o r a ll o g i c ) ，r 1 广r l ( r e a l t i m e t e m p o r a ll o g i c ) 和x c t l ( e x p l i c i t - c l o c kt e m p o r a ll o g i c ) 。 1 4 时序逻辑程序语言 时序逻辑程序设计是一个顺序和并发程序规范和验证的范例。在时序逻辑被 引入用来验证程序的性质以后，新的问题出现了，因为人们必须处理三种不同的 描述符号，一为程序设计语言，一为逻辑框架，另一个是对程序性质的描述。因 此，时序逻辑的一个子集被提出用作程序设计语言的基础。这就意为着程序的编 写，程序性质的说明和对程序性质的验证都可以用一种符号来描述。目前，已经 有许多时序逻辑程序设计语言，像t e m p u r a i 引，x y z e 1 5 , 6 j ，t l 圳，t o k i o i s l $ t i 第一章绪论 5 m e t a t e m 4 】等。 关于t e m p u r a ，在过去的二十年中，已经出现了好几个版本的解释器【l ，7 ，勉2 7 1 。 b e nm o s z k o w s k i 用l i s p l 3 】编写了第一个解释器，这个解释器是关于最原始的 t e m p u r a 的。在1 9 8 4 年后半年，他又改写了这个解释器，使其能够处理双层存储 以及多次扫描的问题。r o g e rh a l e 于1 9 8 5 年在剑桥大学开始了一个c 版本1 2 j 的解 释器，现在由a n t o n i oc a u 和b e nm o s z k o w s k i 维护。1 9 9 2 年，d u a n 扩展了t e m p u r a 并用p r o l o g 开发了另一个版本的解释器【lj 。基于c - t e m p u r a 的a n a t e m p u r a l l 2 j 是一 个运用区间时序逻辑( i t l ) 及其可执行子集t e m p u r a 对系统进行运行时验证的一个 工具。运行时验证技术是使用断言点来检验一个系统是否满足时间性，安全性以 及用1 t l 描述的安全性性质。断言点被插入到系统的源代码中并会在系统的运行 中产生一个信息序列，像变量的值和变量变化的轨迹。既然一个i t l 性质对应一 个状态( 区间) 序列的集合，运行时检验就是验证系统所产生的集合是不是我们 所要验证的性质的序列集合的子集。它就是用来做这个集合包含关系的测试的。 以上各个版本的解释器为时序逻辑程序设计语言的发展做出了重要贡献。在 这些解释器中，大部分传统的语言结构都已经实现了，像顺序，分支和循环等， 另外许多的数据类型，例如整型，数组等也被实现了。不过还有一些重要的语法 结构没有实现，像f r a m i n g 和指针。此外这些解释器所处理的语言与传统的语言差 别甚大，比如变量的值不能传递。 框架t e m p u r a l 7 】是一个用f r a m i n g 和一个新的投影结构扩展了的t e m p u r a ，它 非常像传统的程序设计语言。而且，其中一个新的指针结构1 1 0 j 也定义了出来，根 据每个框架时序逻辑的公式都可以转换为它们各自范式f l j 的理论，我们就重新开发 了一个新的解释器，并实现了f r a m e dt e m p u r a 中的所有结构。在这个解释器中， 如果一个程序被正确地执行完毕并且它的结果为真，则表明这个公式可以被满足， 并且它的模型就会被输出出来，否则就说明这个公式是不可满足的，在运行的过 程中出现了错误，从而找不到符合它的模型。最后在网络服务及电路模拟方法给 出了两个应用的例子。 1 5 模型检测 在过去的二十年中，模型检测技术已经成为一个强大的具有前途的对系统进 行自动验证的方法。笼统地说，一个模型检测器就是一个能确定一个给定的结构m 是否一个逻辑公式驴的模型，或者说m 满足妒，简写为mi = 驴。直观上，m 是所 讨论系统的一个抽象模型，特别是一个有限的像自动机的结构，而庐，来自于时序 的或模型逻辑，则用来说明一个给定的性质。模型检测器则提供一个按钮操作的 方法来证明由m 表示的系统满足这个性质。这种完全的自动性带来的事实是有效 6 框架时序逻辑程序设计解释器及模型检测工具 的模型检测器可以用来构建强大的逻辑，形式和模型检测的吸引力。 模型验证是一个状态空间的穷尽搜索过程，搜索的可穷尽性有赖于为系统建 立的有穷状态模型。一般来说，模型检测工具所使用的状态空问搜索方法可分为 两种：局部方法和全局方法。 全局方法首先产生系统的整个状态空问，并计算出满足原子命题公式的状态， 然后根据公式的结构自底向上进行计算。全局方法的缺点是对存储空间的要求比 较高，需要存储系统的所有状态，不过使用符号化模型检测技术，可以有效地降 低算法的存储需求。全局方法的优点是在算法结束时不但能知道系统是否满足性 质，而且还能知道系统的哪些状态满足性质。 局部方法并非在一开始就产生出系统的全部状态空间，而是边搜索边产生， 只产生搜索过程中所需要的那部分状态空间，也叫o n t h e n v 【2 2 j 方法。这样做避免 了预先生成全部的状态空间，如果系统不满足性质，那么有可能只产生和搜索了 部分状态空间。如l t l l l 9 】模型检测算法，对于待验证的系统s 和u 乙公式痧，算 法首先把公式，妒转化为另一个系统s ，然后对s 和s ，。的同步组合系统进行深 度优先搜索，在搜索时只产生搜索过程所需要的局部状态空间，并进行性质检测。 相对全局方法，局部方法对存储空间的要求相对较低，但是由于搜索过程需要不 断地回溯，局部方法的时间代价比较高。 模型检测经过这些年的发展，出现了不少著名的工具，比较著名的是基于u l 的模型检测工具s p i n 和基于c t l 的模型检测工具s m v 。目前大部分的模型检测 工具都是基于l t l 和c t l 的。由于l t l 和c t l 都是定义在无穷的状态序列上的， 所以它们验证的仅限于永不终止的反应系统，而p p t l 是定义在有穷区间和无穷区 间上的。此外，p p t l 的表达能力要强于c t l ，它的表达能力与正则式是等价的， 本文第四章了介绍了一个基于p p t l 的检测工具，它分别将系统s 和系统的性质的 非，咖转化为它们各自的范式的形式，然后同步求交，判断系统是否满足所给的性 质。 1 6 本文所做的工作及内容安排 本文主要介绍一个用于程序模拟执行及性质验证工具的实现。它分为两个部 分，程序模拟部分是一个解释器，它只模拟执行确定性的程序，不包含非确定性 操作及无限循环程序。程序性质验证部分可以处理各种类型的程序，包括非确定 及无限循环程序。它首先找出程序的各个模型，在这个过程中，在每个状态都把 程序化为范式的形式，并把用命题投影时序逻辑描述的性质也化为范式的形式， 然后进行性质验证。文中首先讨论了解释框架时序逻辑程序的基本方法，根据范 式理论，一个程序可以被重写为两部分，一部分是在当前状态下可以执行，另一 第一章绪论 7 部分需要在下一个状态执行。在每个状态，程序都会被重写为两个部分，可执行 的这一部分会被立即执行，另一部分则在经过处理后被放到下一个状态来执行， 这样程序的模型最终就可以被推导出来。然后本文会详细介绍该解释器的框架及 各个模块及结构的实现细节，此外，还会给出它在一些领域中应用的例子。最后 文章介绍了如何使用框架投影时序程序设计语言及命题投影时序逻辑来做程序性 质验证。 全文由五章组成： 第一章为绪论，简要介绍了软件安全中的形式化验证方法，并回顾了时序逻 辑的发展历程及现状。并介绍了近年来时序逻辑程序设计语言t e m p u r a 及其解释 器的研究工作以及全文的研究工作。 第二章首先介绍了时序逻辑的语法、语义及一些重要结构，然后详细介绍了 框架投影时序逻辑程序设计语言f r a m e dt e m p u r a 。 第三章介绍程序模拟执行部分，即解释器，实现的基本方法及解释器的框架。 此外重点介绍了一些重要结构的实现细节。最后给出了它在w e b 服务及电路方面 应用的例子。 第四章介绍了基于框架时序逻辑程序设计语言( f t l l ) 和p p t l 公式的验证工 具，首先介绍了相关方面的基本理论，然后给出了基本的算法，最后用一个完整 的实例来说明工具的运行过程。 第五章则简要介绍了目前主要的模型检测工具。 最后是对本文的总结和以后工作的展望。 第二章投影时序逻辑及框架时序逻辑程序设计语言 9 第二章投影时序逻辑及框架时序逻辑程序设计语言 投影时序逻辑p i t l ( p r o j e c t i o ni n t e r v a lt e m p o r a ll o g i c ) 是基于区间时序 逻辑的，它是区i 日j 时序逻辑的带有投影结构的扩展。本文中所讨论的包括命题投 影时序逻辑和一阶投影时序逻辑。 2 1 1 命题投影区i 、日j 时序逻辑 2 1 语法 扩展了的命题投影区间时序逻辑使用包含时序操作结构的命题逻辑来讨论时 间的区间问题。时序的操作包括向前和向后的操作。假定z 表示所有的整数，表 示所有的j 下整数，。表示所有的非负整数。 ( 1 ) 字母表 1 ) 命题常量：t r u e ，f a l s e 2 ) 一个可数的原子命题集合p r o p 3 ) 联结词：一( 非) ，a ( 与) ，v ( 或) ，- ( 蕴涵) ，( 等价) 4 ) 时序操作符：0 ( n e x t ) ，：( c h o p ) ，( s o m e t i m e s ) ，o ( w e a kn e x t ) ，p r j ( p r o j e c t i o n ) ，口( a l w a y s ) 5 ) 其它p p l l l 公式：e m p t y , m o r e , s k i p , l e n ( 2 ) 公式定义 定义2 1p p l l 公式归纳定义如下： p ：_ p1 只v 只l eio el ( 只，己) p r jq 式( 2 一1 ) 其中p e p r o p ，置，己和q 为p p t l 公式 2 1 2 一阶投影区间时序逻辑( p i t l ) ( 1 ) 项 设p r o p 为一可数的命题集合，v 为有类型的变量的集合。我们假定变量 分为静态的和动态的。8 一 t r u e , 六a l s e 代表布尔域。d 表示我们所要用到 的各种数据，包括整数，链表，集合等。z 表示所有的整数，表示所有的 j 下整数，。，则表示所有的非负整数。n 。= n 。u ) 。项可以归纳定义如下： 1 0 框架时序逻辑程序设计解释器及模型检测工具 1 ) 单个的具有类型的静态变量：a , b ，c ，u ， ，可能带有下标。 2 ) 单个的具有类型的动态( 状态) 变量：x ，y ，z ，x ，y ，z ，可能带有下 标。 3 ) 如果厂是一个具有m ( m 0 ) 参数的函数，并且p 1 一，e 。是y 中与厂的 参数的类型相符的项，那么f ( e l 一，e 。) 也是v 中的一个由厂的类型所 定义的项。特别地，当m = 0 时，厂是一个常项。 4 ) 如果e 是个项，那么o e ，b e g ( e ) ，e n d ( e ) 也是具有类型的项。 ( 2 ) 原子公式 1 ) 每个命题p e p r o p 部是一个原子公式。 2 ) 如果p 是一个原始的具有m ( m 0 ) 参数的谓词，并且p 1 ，一，e ，是y 中 具有与p 中参数类型相匹配的项，那么p ( e 1 , - - - , e 。) v 中的一个项。 3 ) 如果p 。，e ：是具有相同类型的项，那么e ，= e ：是一个原子公式。 ( 3 ) 基本公式 1 ) 每个原子公式都是一个基本的公式。 2 ) 如果p 和q 是基本的公式，那么下面的公式也是基本公式： 一p ，p q ，虫：p ，o e ，o p ，p ；q ，p + 设n 是一个可数的命题集合，y 是一个可数静态的和动态变量的集合。项e 和 公式p 由下面的语法给出： e ：_ 工iui 观io eib e g ( e ) ie n d ( e ) i ，( e l 一，e 。) 式( 2 - 2 ) p ：暑刀ie 1 ；e 2lp ( e l ，一，e 。) l 叩lp l p 2i 虫：pi 印i 印i ( p l ，一，p 。) p r j , p 式( 2 - 3 ) 这里x 是动态变量，u 是静态变量。在厂( p l ，p 。) 和p ( e l 一，e 。) 中，f 是函数，p 是谓词，假定项的类型和与厂和p 中的参数类型是一致的。如果一个公式( 项) 中不包含任何时序操作符，那么它就被称作状态公式( 项) ，否则它就是时序公式 ( 项) 。 2 2 语义 下面我们介绍一阶投影区问时序逻辑( p i t l ) 的语义，命题投影区f n j 时序逻辑 ( p p t l ) 的语义为p i t l 语义的特例。 ( 1 ) 状念 第二章投影时序逻辑及框架时序逻辑程序设计语言 1 1 我们定义一个状态s 为yu p r o p 上的赋值( ，p ) ，对任意的变量y 矿，定义 研，】= ，i v ，并且对任意的命题万p r o p ，定义s 防】。i p 陋】。i v m 是一个具有合 适类型的值或咒f f ( 未定义) ，l p 防】属于 t r u e , f a l s e 。 ( 2 ) 区间 假定静态变量在区间上保持不变，而动态变量则在不同的状态具有不同的值。 一个区间d 就是一个非空的状态系列，可以是有限的，也可以是无限的。当区间o r 为无限的时候，它的长度i i 为缈，否则即为它的状态数减1 。不论区问是有限的 还是无限的，为了使它们具有一个统一的表示，我们使用个扩展的整数符号作 为它标记，即 n 。= n ou 枷) 并且把比较符= ， ，扩展到。上，假定对所有的f 。，i 有- c o 。此 为我们把! 定义为s - 一叫 。为了简化定义，我们把仃表示为 ，当 盯是无限的时候，1 。i 是未定义的。( f d ( osf 型sh ) 表示子区间 ， o r ( k ) ( 0 k d a 表示 。 ( 3 ) 解释 一个解释即为一个元组i p ，i ，k ，) ，口表示区间，i , k 为整数，- 一个整数 或甜，并r osf 匀sh 。我们用标记p ，f ，k ，) l = p 来表示某个公式p 在仃的子区间 的当前状态& 是满足的。对每个项e ，它的值在i = p ，f ，k ，_ j ) 上表示为 i m ，并按下面的方式归纳定义： i v a u i a 】= s k 【口】= f ：【口】= 班口】如果a 是一个静态变量 i 一嗍 i x 】= & m = ，：m 如果石是一个动态变量 i f u n i f ( e 1 ，一，p ，) 】= i e n e x t i 【o ( e ) 】 i e p r e vi 【o ( p ) 】 i fi e 】= 刀f z 某个h 1 ，m ，) f ( i e 。】- oo l e 。】) 否则 = 。 f ，七+ ：z 气昙贝j f 后 j 2 仃七一；窖贝f f f 尼 i b e gi b e g ( e ) = ( 仃，i ，i ，k 】 1 2 框架时序逻辑程序设计解释器及模型检测t 具 i 一册d i e n d ( e ) 】= f 仃 正j 咒, f j z i p l 否i f 贝o ， 为了定义投影操作的语义，我们首先定义一个辅助的操作符。设 盯； 是一个区间，r 1 ，厶( h 苫1 ) 是整数使得 0s r osr 1s s 厂 5 h ， 则在厂l ，上的投影即为区间 口 ； 。此处1 一，f ，是通过删除，1 ，r h 中的冗余元素得 到的。也就是说i ，一，f ，是厂1 ，厶中最长的递增子序列。例如， j ； 。 为了方便证明，我们定义标记- l ，一，p 。h ，册) ，对于公式p 1 ，和整数 r l ，o - 1 ，r 卅。( 厂ls s 一l 虫) 来说，p l ，一，p 。在它的某个子区间上执行。 厂1 ，k 一。为分界点，而则为这个子区间的右端点。形式上，设i = p ，i ，k ，歹) 为一 个解释，那么有 ( 仃，i ，k ，) i = - l ，p 。h ，r ) 当且仅当 p ，i ，k ，1 ) | 互p 。并且对所有的1 s ，l ，有p ，厂 小r ) | 暑仇。 我们把盯j f “，乞) 推广一下，令i 为t o 。对于区问o r = 和 os ，ls r 2s sr sl o r l ( 。) ，我们定义 口10 一 盯l ( ，1 ，r ，) = o rj r “，厶) 并且对于整数，l ，仃j ，( ，1 ，厶) 和以前一样定义。 那么对于解释i p ，i ，k ，_ | ) ，我们可以用b l ，p ，l r , ，k ) 形式化地定义投影 操作为： p ，i ，k ，j ) i = p l ，一，p 。) p r j q 当且仅当存在厂1 ，1 乇。和，o = k 使得 p ，i ，k ，) i 一瞄l 一，p 。h ，_ ) 并且 厂卅= j ，对某个oshsm ，有仃j r ( 厂1 ，r ) l _ q ，或者 ，卅 j 并h _ o l ( ，1 ，) d ( j ) i - q 。 我们引入的投影操作( p 1 一，p 。) p r j q 可以看作是标准投影和并行操作的结合。 直观地，q 与p 1 p 。在一个区l 、日j 上并行地执行，这个区间通过去除原区间中的集 合点得到。该投影操作允许p l ，p 。，q 各自独点，他们都有权利来定义它们自己所 第二章投影时序逻辑及框架时序逻辑程序设计语言 1 3 执行的区间。特别也，进程序歹l j p l , p 。与进程g 可能结束于不同的状态点。虽然 里程间的通信仍然依赖于共享变量，但它们的通信与同步只发生在集合点上( 全 局状态) ，否则它们就各自独立地运行。新的投影操作允许用不同的时间区间来 刻画程序运行的说明。 关系i = 归纳定义为： i p r o p i l pi f 对某个命题p 有s 女【p 】2 t r u e 。 i n o ti j = ，p i fi j p 。 i a n di i = p qi fi i - - p 并且i h 。 i n e x ti i - 印i fk _ 并且( 口，f ，k + l _ 】= p 。 i s o mi l = pi f 存在厂使七s ，g ，并且p ，f ，k ，- i ) i = p 。 i c h o p i i p ；q i f 存在厂使k s ，纠，p ，f ，k ，j ) i zp 并且 p ，_ ) i tq 。 i p r e v il 一印i ff k 并且( 盯，f ，k - 1 , j ) l p 。 i s o m p il 一pi f 存在，使fszs k 并且p ，i ，z ，) i p 。 i p ，： if 一0 l 一，p 。) p r y q ，如果存在整数七= r os s s r ms 使 p ，f ，) | _ p l ，p ，1 ，- l ，r , ) l - p ，( 对1 ，s 历) 并且对下面 的某种情况有p ，0 ，0 ，j 口l q ) ： ( a ) _ 并且一o r l ( r o ，名) 口( ，l 州) ( b ) = j 并且对某个0s hsm 有仃= l ( r o ，r h ) ( 4 ) 优先级 为了避免过多地使用括号，本文使用以下的优先级规则： 1 - 20 ，+ ，车，口，0 ， 3j ，v 4 = 1 4 框架时序逻辑程序设计解释器及模型检测工具 5a ，v 6 一h 7 ： 8 其中从1 到8 优先级依次递减。 2 3 框架技术 f r a m i n g 技术在传统的命令式语言中已经使用了很多年。在传统的语言中，它 被认为是理所当然的。但是在时序逻辑程序设计中我们不得不重新考虑这种情况。 f r a m i n g 关注的是变量的值如何从一个状态传递到另一个状态，在这方面，时序逻 辑没有提供任何方法，前一个状态中变量的值并不会传递到下一个状态。因此， 如果我们想要变量继承前一个状态的值，我们不得不重复在每个状态给为题赋值。 这样不仅繁琐，而且效率低下。此外，在时序逻辑程序设计中，如果没有f r a m i n g 的话，同步通信也不能实现。 时序逻辑程序设计中另一个亟待解决的问题是并行进程的通信问题。一些模型 中用共享为题，一些使用同步消息传递，还有一些使用异步通道。对于使用共享 为题的并行程序中并行进程的同步通信，一个同步结构a w a i t ( c ) 和一些相似的结构 是需要的。它意为着a w a i t ( c ) 改变什么变量，而是等到它的条件成立时终止。 在时序逻辑中给a w a i t ( c ) 建模需要一种不确定的平衡，因为在当前状态你不知 道它需要等待多久。但是它同时也必须允许变量的会下发生改变，这样外部的进 程才能改变变量使其条件成立。要解决这个问题就需要某种形式的f r a m i n g 操作。 f r a m i n g 技术的关键是如何感知对变量的赋值，为了定义对一个变量，比如茗， 的赋值操作的存在，我们使用一个叫做赋值标记的标记，由谓词矿“) 来表示。每 当一个变量被赋值时它就为真，否则为假。 为了定义f r a m i n g 操作，我们先定义下列赋值： 定义2 2 ( 1 ) x i = pd e fx i = e p 。( 1s fs 甩) ( 2 ) t 一+ p d e f3 a ：( 口；e c ( e m p t y 一仁口) ) ( 3 ) x i d = 一一d e f3 a ：0 = e d g 。仁口) ) ( 4 ) 工f ：= + ed e fx i o = + eas k i p ( 5 ) 仁l ，x 。) o p ( e 1 ，一，) d e fb ，o pp ，) b 。o p 巳) 第二章投影时序逻辑及框架时序逻辑程序设计语言 1 5 此处口是一静态变量，e 为一表达式，p 。则为一与状态x i ( 1s is 刀) 相关的原子命 题。p ，不用作别处，在( 5 ) 中，叩：墨- + 10 一+ i ：- + i 寺。 使用这个赋值标志，我们可以定义状态f r a m i n g 和区间f r a m i n g 操作。直观地， 当一个变量在某个状态是框架的，如果没有遇到赋值语句对它赋值，则它的值是 不变的。如果一个变量在一个区白j 的所有状态上都是框架的，则它就是一个区间 框架的变量。我们由些可以定义下面的两组操作，定义2 2 是一个向f i 一个状念看 的操作，式子( 1 ) 说明x 。在当前状态是框架的，式子( 2 ) 则定义x 。是区间框架的。 定义2 3 则是定义一个向后一个状态看的操作，其中式子( 1 ) 说明工。在当前状态是 框架的，式子( 2 ) 则定义x 。是区间框架的。实际上，这两个定义是相等的。 那么，设b 为一静态变量，并且五，x 。为动态( 状态) 变量。有 定义2 2 ( 1 ) l b f ( x 一d e _ f f o - a f ( x 女) 呻3 b ：( 眦i - bax 女。6 ) ( 2 ) f r a m e ( x 一c l e f 如d ，e _ 蟛k ) ) ( 3 ) f r a m e ( x l ，吖。) 丝f r a m e ( x 1 ) f r a m e ( x 。) 定义2 3 ( 1 ) l f f ( x 。) 塑0 一a f ( x 。) 一r t b ：k b o x t - b ) ( 2 ) f r a m e o 。) 塑d ( m o r e 呻谚k ) ) ( 3 ) f r a m e 。0 1 ，) 堂f r a m e 仁。) f r a m e g 。) 动态变量s 在p 中被称为是框架的，