显式符号建模在形式验证中的应用

理论计算机科学电子笔记130（2005）301-321www.elsevier.com/locate/entcs形式验证的显式符号建模翁贝托科斯塔1，2 塞尔吉奥坎波斯3牛顿维埃拉5Departamento de Ciência da ComputaçãoUniversidade Federal de Minas GeraisBelo Horizonte，巴西David Déharbe大卫·德哈布北里奥格兰德联邦大学应用信息和数学系巴西纳塔尔摘要我们提出了一个模型，结合显式和符号表示的显式符号形式验证模型。显式模型和符号模型都已成功地用于有限状态并发系统的验证，如复杂的时序电路和通信协议。该模型的目的是同时使用显式和符号技术来验证同一模型，并使其有可能采用最有效的技术，以每个方面的模型。首先，我们形式化的显式符号模型，并显示它可以从一个标记的状态转换系统生成。 然后，我们将这些想法应用到Verimag中间格式描述的系统中，并提出了集成底层模型的主要算法。保留字： 模型检验，显式状态，二叉决策图1 由巴西CAPES的赠款支助。2电子邮件：umberto@dcc.ufmg.br3电子邮件：scampos@dcc.ufmg.br4 电子邮件地址：david@dimap.ufrn.br5电子邮件：nvieira@dcc.ufmg.br1571-0661 © 2005 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2005.03.016302联合Costa等理论计算机科学电子笔记130（2005）3011介绍由于计算应用程序的复杂性不断增加，自动化工具已用于帮助开发人员查找硬件和软件系统中的错误。实现这一目标的两种方法是模拟和形式验证。模拟方法包括对给定的输入执行测试并检查结果。这种技术可以很容易地评估控制和数据方面，但通常只检查状态集的一部分。换句话说，模拟可以说明特定的输入是成立的，但它不能证明整个状态集的正确性。形式化方法包括基于数学的语言，技术和工具，用于指定和验证硬件和软件系统[12]。复杂系统和关键应用程序受益于形式化方法，因为它们使系统更可靠。与模拟不同的是，形式验证技术在问题域上执行穷举搜索，证明符合规范，而不仅仅是指出某些输入数据的错误。模型检验是一种著名的、成功的验证有限状态并发系统的形式化技术它已成功用于验证复杂的时序电路设计和通信协议[11]。模型检验是指通过一个有限的模型来表示一个给定的系统，并对其进行详尽的分析，以确定它是否符合某些属性。模型可以表示为图，其中每个顶点是系统的状态，并且边是状态之间的有效转换。国家可以明确地或通过某种象征性的表示来表示。显式模型单独枚举状态，将它们存储在哈希表等结构中。显式方法倾向于呈现相对更可预测的效率和记忆行为。另一方面，符号模型探索状态空间中的规律性，旨在产生更紧凑的表示。与显式模型检查不同，符号模型检查使用布尔逻辑公式的高效编码来原子地表示和探索状态集。因此，与显式模型检查相比，符号模型检查通常允许我们验证具有更多状态的系统[14]。为了执行符号模型检查，状态和转换的集合由特征函数表示。特征函数的计算表示必须是有效的，并且应该提供基本的运算，如合取、析取、等式检验、存在性量化和替换。二元决策图[6]，被称为BDD，是一种非常有效的命题逻辑函数的符号表示。不幸的是，有时候的确如此联合Costa等理论计算机科学电子笔记130（2005）301303很难通过简单的布尔表达式来表达令人满意的数据信息，例如对整数或实数的约束[17]。一般来说，整数和算术运算不能通过简单的布尔表达式有效地表示，这是由于所产生的表示的大小[8]。此外，具有连续变量的系统范围在不可数域上，如实时系统，不适合符号模型检查[16]。通常，显式方法比符号方法更有效的状态空间呈现出一个不太规则的结构。在本文中，我们提出了一个模型结合显式和符号表示的显式符号形式验证模型。 我们打算使用显式和符号技术一起验证同一个模型，并使之有可能采用最有效的技术，模型的每个方面。在下一节中，我们将介绍相关的工作和我们的主要目标。在此基础上，我们建立了显式符号模型，并展示了如何从一个标记状态转换系统。然后，我们讨论了形式验证工具如何使用我们的模型来验证Verimag中间格式[4]中给出的系统。还示出了为集成基础模型而开发的算法。最后，我们提出了我们的下一个步骤和一些评论。2相关工作我们的显式符号模型集成了底层的显式和符号模型。因此，它与明确的和象征性的验证者及其技术有关。目前，SPIN [13]和JPF [5]是众所周知的，并且广泛使用的显式状态模型检查器。另一方面，SMV [15]，NuSMV [9]和Verus [7]是具有代表性和成功的符号状态模型检查工具。现有的算法优化，从这样的工具，如上的SPIN使用的嵌入式技术，应考虑为底层模型的实现，以提高模型检查。2.1满贯SLAM项目[3]中采用的方法与我们的项目更密切相关，因为它在同一环境中采用了显式和符号模型。SLAM从C代码中提取抽象模型，并静态检查软件的时态属性。此外，SLAM使用谓词抽象，符号推理和迭代细化。Bebop是SLAM的一部分，负责执行布尔程序的可达性分析。布尔程序是程序的抽象，其中具体状态已经被映射到在有限的预测集的评估下的抽象状态。生成的程序大致对应于一个C程序，304联合Costa等理论计算机科学电子笔记130（2005）301相同的控制流结构，但所有变量都是布尔类型。由于所有的变量都是布尔类型，所以程序的状态空间是有限的。因此，布尔程序的可达性和可终止性是可判定的。关于谓词抽象算法及其相应实现的更多信息可以在[1]中找到给定布尔程序，Bebop执行过程间数据流分析以确定可达性信息[2]。Bebop显式地表示控制流，并使用BDD隐式地表示状态集。由于使用了编译器优化技术，控制流特性的显式表示是合理的。另一方面，BDD用于象征性地表示过程的输入和输出行为。它们用于表示程序点处的可达状态集。一个状态包含程序计数器和所有变量在该点可见的值。与我们的显式符号模型相比，SLAM缺乏灵活性，因为控制流和数据流信息必须分别有显式和符号表示。所提出的模型更一般，因为它允许我们根据任何策略在显式空间和符号空间之间移动变量。因此，我们可以尝试各种组合，并选择最适合系统需求的组合。 有关建议模型的可扩展性的更多详细信息，请参见第73显式符号建模虽然显式符号模型可以直接从标记的状态转换模型中生成，但我们决定分两步完成这项任务最初，显式和符号模型都是通过对原始模型的变量进行划分而生成的投影。然后，将显式模型和符号模型相结合，构成显式-符号模型。这种方法提供了一个更直观和清晰的过程来理解模型的形式化。3.1原始模型设M=（S，R，L）是给定系统的模型，其中S表示状态集，R<$S×S表示状态之间的转移关系，L：S→2AP表示给每个状态分配一组原子命题的标号函数。 假设AP是M的原子命题的集合。假设集合AP被分解为分别由显式命 题 AP e 和 符 号 命 题 AP s 组 成 的 子 集 ， 其 中 AP=APe<$APs 和APe<$APs=<$。使用这种比例分割，生成两个问题关系，即，联合Costa等理论计算机科学电子笔记130（2005）301305eeSss，sJ∈S，s<$esJ←→L（s）|AP =L（sJ）|APs，sJ∈ S，s <$ssJ←→ L（s）|AP= L（sJ）|AP每个导出等价类[s]e是一个显式状态，每个等价类[s]s是一个符号状态。换句话说，每个状态s∈S对应于一个显式状态[s]e和一个符号状态[s]s。因此，状态集合S被投影成显式和符号化的状态集合Se和Ss，如下所定义：下图：Se={[s]e|s ∈ S}Ss={[s]s|s ∈ S}Ee和Es关系分别为显式和符号状态定义了两个标记函数Le和Ls显式状态e和符号状态s的标签如下所示Le（[s] e）= L（s）|APe Ls（[s] s）= L（s）|APs因此，L（s）= Le（[s]e）<$Ls（[s]s），因为L（s）= L（s）|亚太经合组织|美联社。原始系统的投影要求原始的转换关系R被分成一个转换关系的显式和另一个符号部分的模型，Re和Rs，分别。为了保持显式变迁和符号变迁之间的对应，必须对原始变迁进行标记。一个显式变迁和一个符号变迁只有在它们来自同一个原点时才被赋予相同的标号id∈Ntransition（s，id，SJ），其中s，SJ∈S。所以，标签将明确的和象征性的转换，指示在模型上一起发生的转换如果有一个原件转换关系R，得到以下两个转换关系Re={（[s]e，id，[sJ]e）|（s，id，SJ）∈ R}Rs={（[s]s，id，[sJ]s）|（s，id，SJ）∈ R}也就是说，如果（s，id，sJ）∈R，则（[s]e，id，[sJ]e）∈Re且（[s]s，id，[sJ]s）∈Rs。将显式模型和符号模型结合起来，可以恢复原始模型每两个变迁（[s]e，ide，[sJ]e）∈Re和（[s]s，ids，[sJ]s）∈Rs，其中ide=ids，定义一个原始变迁（s，id，sJ）∈R，使得id=ide=ids，L（s）=Le（[s]e）<$Ls（[s]s）和L（sJ）=Le（[sJ]e）<$Ls（[sJ]s）。3.2显式符号模型给定Me=（Se，Re，Le）和Ms=（Ss，Rs，Ls），通过这两个模型的合成，得到了显式符号模型Mh=（Sh，Rh，Lh）每个显式符号状态sh∈Sh由一对（se，ss）给出，其中se∈Se，ss∈Ss，并且存在显式符号转移306联合Costa等理论计算机科学电子笔记130（2005）301H（se，ide，sJ）∈Re且（ss，ids，sJ）∈Rs使得ide=ids.对于每个sh∈Sh，e s我们有Lh（sh）=Lh（sh）|APeLh（sh）|APs，其中Lh（sh）|APe =Le（se），Lh（sh）|AP=Ls（ss）。若（se，id，sJ）∈Re且（ss，id，sJ）∈Rs则（sh，id，sJ）∈SE S H其中sh，SJ∈Sh. 由于Rh的定义，模型Me和Ms必须以交错和同步的方式进行探索，标签请注意，在探索中的状态期间，Se和Ss。采用显式-符号模型，我们可以以直接的方式恢复原始的显式和符号模型。给定Mh=（Sh，Rh，Lh），我们生成eMe=（Se，Re，Le），使得Se={Se|（se，ss）∈Sh}，Re={（se，id，sJ）|（（se，ss），id，（sJ，sJ））∈Rh}和Le（se）=Lh（（se，ss））|AP.的e e se可以类似地获得模型Ms4中间格式中间格式[4]，在本文中也称为IF，是一种为了对异步通信实时系统建模而开发的语言。 它被用作一组称为IF验证环境的验证工具之间的交换格式。IF模型由多个流程实例组成，通过共享变量和消息传递并行运行并异步交互。消息传递是通过信号、信号路由实例和FIFO通信缓冲器来完成的。在本节中，我们将显式符号建模应用于IF模型。首先，我们描述了语言中的主要组成部分，并提出了一些例子，它的结构。接下来，我们将展示如何使用这些组件来生成显式和符号模型。最后，我们结合显式和符号模型，以模仿的显式符号模型的原始模型的行为。4.1建模语言系统规范由通用组件组成，包括动态组件（如进程、信号路由和信号）和静态组件（如变量、数据类型、常量值和外部过程）。形式上，系统被给出为元组（D，S，P），其中D是包括布尔、整数、时钟、pid和用户定义的，S是类型化信号的集合，P是进程类型的集合。在图1中，我们展示了构成交替位协议IF规范的一些元素。联合Costa等理论计算机科学电子笔记130（2005）301307系统bitalt;type data = range 0..return（boolean）;...过程变送器（1）;...endprocess;...末端系统;（一）process transmitter（1）; var b boolean;...state start #start;task b：= false;nextstate idle;endstate;...endprocess;（b）第（1）款Fig. 1. 中间格式系统（a）和过程（b）示例。进程被定义为扩展的有限状态机。每个进程实例都有一个唯一的标识符编号和一个存储所有传入消息的输入FIFO缓冲器。进程规范包括一组局部变量（对应于局部内存）和一组控制状态。数据类型、常量和过程定义也可以包括在内。从形式上讲，每个过程被看作一个元组（Q，X，T，q0）∈P，其中Q是控制状态集，X是类型变量集，T是转移集，q0∈Q是初始状态.请注意，X包含局部变量和全局控制状态通过动作、到其他状态的转换以及可能的子状态来定义过程的行为。 嵌套子状态的数量没有理论限制状态规范包括时间约束和延迟信号集。初始状态在状态定义期间由关键字#start定义。由于模型检查器需要跟踪当前被访问的状态，我们的显式符号模型使用存储这种信息的变量从现在开始，我们把这样的变量称为程序计数器。状态之间的转换由条件守卫控制。因此，过渡可以被看作是对刺激的反应过程。转换可以通过激活某些非定时保护、激活某些定时保护或在流程实例的输入缓冲器中存在某些信号来触发当满足条件保护时，在将控制传递到另一个状态之前可能需要执行某些操作动作包括变量赋值、时钟设置、时钟和变量重置、信号发送、过程调用、进程和信号路由的创建和销毁。转换还可以与停止操作一起使用，这意味着流程实例的销毁。 在一般来说，条件保护g被定义为系统变量，即g∈2X。 不定时的警卫是通过提供子句，由常量、变量和布尔运算符、算术运算符和关系运算符组成。定时保护是通过when子句实现的，when子句控制时钟变量的时间约束。最后，通过输入子句实现输入缓冲器中信号的存在。所有信号在每个流程实例中共享一个队列，因此，当308联合Costa等理论计算机科学电子笔记130（2005）301状态q8;...假设c = b;...nextstate空闲;...结束状态;（一）状态忙;输入ack（c）;下一个状态q8;当t = 1时;...nextstate busy;endstate;（b）第（1）款图二. 条件守卫。预期的消息在缓冲器中，但不是报头中的消息的队列。为了对队列建模，我们的显式符号模型向X添加了其他变量，包括用于控制读写位置的变量。最终，阅读和写作位置被用来确定输入子句的成功或失败。在图2中，显示了一些保护和转换。所提供的子句（图2（a））建立了用于执行从状态q8到状态idle的转换的条件。 同样，输入和条款，图2（b），建立了执行转换的条件从状态忙碌分别到状态Q8和忙碌请注意，在保护条件和转换本身之间可以有一些语句由于在某些控制状态下可以启用多个转换，并且在执行时必须考虑所有情况，因此流程可能具有非确定性行为。各个进程的执行是交错的。4.2显式和符号模型设M=（D，S，P）是一个以中间格式指定的系统。将M个变量划分为显式和符号两部分，分别生成两个独立的模型Me=（D，S，Pe）和Ms=（D，S，Ps）考虑每个过程（Q，X，T，q0）∈P，变量划分导致显式过程（Qe，Xe，Te，q0e）∈Pe和符号过程（Qs，Xs，Ts，q0s）∈Ps.给定每个过程（Q，X，T，q0）∈P，必须分析其控制状态和相应的保护。在Xe变量上执行的防护、动作和转换被投影在模型Me中，G a而X以上的 在模型M中预测变量。 设q qJ∈Tss−−→是（Q，X，T，q0）∈P的一个转移，其中q∈Q是源状态，g∈2X是布尔保护，a是动作，QJ∈Q是目标状态.这种转换影响Xe和Xs中的变量，其中这些变量表示程序计数器、条件保护和操作。因为两个模型都是抽象的，所以原始的转换会导致一个显式转换和一个符号转换：qgee eJGs asJe−→qe∈Te和qs−→qs∈Ts联合Costa等理论计算机科学电子笔记130（2005）301309ei1S使得ge=g|X，ae=a|X，qe和QJ∈Qe，gs=g|X，as=a|X，qse qJ∈e ees ss其中，Qe=Q|Xe，Qs=Q|Xs。Me和Ms的初始状态是由初始状态q0投影，即q0e=q0|Xe和q0s=q0|Xs。请记住，这种显式和象征性的转换必须与对方.4.2.1显式转换关系显式转换关系应该表示为一个链表数组，其中一个数组条目对应于一个状态，链表定义了当前状态可以转换到哪些状态Te（Qe，QJ）=（qe，L1），（qe，L2），.e1 2其中Li=qJJ埃伊2Jei3、、......例如，这个转换关系定义了trans-transition-状态之间的转换（qe1Je11），（qe1Je12）等等。4.2.2符号转换关系符号转换关系应表示为当前状态和下一状态的命题之间的公式Ts（Qs，QJ），以使其简单。使用BDDs。4.3显式-符号组合模型的生成系统变量的划分导致产生不同的显式和符号模型。每个生成的模型只覆盖变量的一个子集，只调查搜索空间的一部分。这样的模型必须以交错的方式执行，以便允许我们探索整个搜索空间并模拟原始系统的行为。由于效率问题，我们提出了一种新的关联变迁的方法。代替使用建模中定义的转换标签，通过将符号转换与显式转换相关联来交错显式和符号模型。给定Me=（D，S，Pe）和Ms=（D，S，Ps），Mh=（D，S，Ph）如下所示获得。 对每个（Qh，Xh，Th，q0h）∈Ph，我们通过为每个显式转换引入符号转换来组合显式和符号表示：Th（Qh，QJ）=（qe，L1），（qe，L2），.h1 2其中Li=（qJ，Ts），（qJ，Ts），（qJ，Ts），. 且Ts= Ts（Qs，QJ）。图表-ei1i12012年12月22日ei3i3ij ijs每个（qe，Li）∈Th（Qh，QJ）可以表示为图3所示。AC-Ih根据这种显式符号模型，首先，我们探索显式符号中的状态，模型，然后在符号模型中的状态。 IntuTsij 代表，q，q→q→q310联合Costa等理论计算机科学电子笔记130（2005）301伊杰伊杰ei1埃伊2ei3伊杰从qsi的J西伊季与从qei的显式转换相关联至QJ. 这样的转换定义了从（qe，qs）伊伊伊至（qJJ西伊季），均在Qh. 因此，Qh对应于对（qe，qs）的集合asso。其中qe∈Qe，qs∈Qs.因此，Xh= X e<$Xs和q0h=（q0e，q0s）。图三.显式符号转换显式和符号模型可以直接从显式符号模型中得到。因为每个qh∈Qh对应于一对（qe，qs），其中qe∈Qe和qs∈Qs，所以一个显式符号状态恰好与一个显式符号状态相关联。关于过渡关系Th（Qh，QJ）=（qe，L1），（qe，L2），...，（qe，Ln），每对（qe，Li）对应h1 2niJ从qei到 对于Li对中的每个显式状态q，其中Li=（qJ，Ts），（qJ，Ts），（qJ，Ts），. 同上。 同样，sym-我1我 2我 3J通过构造T_s_ij，可以得到一个双曲过渡关系，其中（q，T_s_ij）∈ L_i.5模型检测算法我们的算法假设系统的属性是在计算树逻辑，简称CTL。CTL是一种重要的具有离散时间概念的分支时态逻辑。CTL对于一组重要的系统属性的表达能力很强，允许指定安全性，活性，公平性和死锁自由。有关CTL语义的详细信息，请参见[10]。设Φ是模型M上的CTL规范。 根据定义，Φ要么由原子命题ap给出，要么由应用于CTL子公式的时间逻辑运算符组成：Φ：：= F alse |T rue |AP|（欧元Φ）|（Φ ∧ Φ）|（Φ ∧ Φ）|（Φ →Φ）|AX Φ |EX Φ |A [Φ U Φ] |E [Φ U Φ] |AG Φ |EG Φ |AF Φ |EF Φ至q，q联合Costa等理论计算机科学电子笔记130（2005）301311J格SJSJ其中新的连接词AX、EX、AU、EU、AG、EG、AF和EF被称为时间连接词。假设Φ是通过解析树以结构表示的方式给出的。 在这样的解析树中，叶子代表原子命题，在显式模型或符号模型中表示，而内部节点代表显式符号表达式，在显式符号模型中表示。首先，算法将显式和符号状态转换为相应的显式符号状态。后算法处理输入和输出显式符号状态的集合5.1原子命题在分析原子命题时，我们必须考虑两种不同的情况。首先，原子命题ap可以是显式的，以显式编码状态表示。第二，ap可以是符号化的，由BDD表示独立的情况下，输入必须产生一组显式符号状态S。5.1.1显式命题考虑命题ap∈Xe。 首先，该算法确定其中ap成立的显式状态集合E。接下来，对于每个qei∈E，它确定由qsi表示的符号状态，这些符号状态构成有效的显式符号状态（qei，qsi）。01S←02 E ← {qe ∈ Qe|Qe|=ap}03 为每一个人 ∈Edo04对于每个Tsij其中e（qei，Li）∈Thandd（qej，Tsij）∈Lido05add（qei，qsi）tooS其中Tsij=qsi<$qsj5.1.2象征性命题考虑命题ap∈Xs。首先，该算法确定BDDqsi，其表示ap保持的符号状态的集合。之后，它访问显式转换关系，寻找符号转换Tsij=J Jqsi，对于某些q∈Qs. 对于找到的每个Tsij，算法创建一个显式符号状态（qei，qsi），其中（qei，qej）是显式转换asso。我是TSJ。01S←02 qsi ←Qs|AP03 为每一个人 ∈Qedo04对于每个Tsij 其中e（qei，Li）∈Th且d（qej，Tsij）∈Li05if（Tsijqsi）06开始假则07add（qei，qsi）tooS312联合Costa等理论计算机科学电子笔记130（2005）301J08打破09端请注意，上述算法只包括一个显式符号状态（qei，qsi）的结果，如果qei和qsi同时保持显式和符号模型，分别。具体来说，内部循环确保状态qei和qsi彼此关联。较小的状态集需要较少的内存并提高搜索的性能。此外，在传递到显式变量的探索之前，必须探索尽可能多的符号变量，以降低组合显式模型和符号模型的成本。换句话说，我们应该在探索对应的模型之前尽可能多地探索每个基础模型5.2显式符号表达式下面的算法假设初始表达式已经被用来产生显式符号状态。每个算法取输入显式符号状态I1和I2的集合，并产生另一个显式符号状态S. 因为时间逻辑运算符<$、Xl、EX、EU和EG可以用于为了定义其余的CTL运算符，我们将讨论限制在这些基本运算符上。5.2.1否定给定由输入状态集合I1表示的表达式，该算法产生输出显式符号状态集合S，其中，对于每个显式状态qei∈Qe，如果（qei，qsi）对于某些qsi∈Qs在I1中，则算法产生符号状态的补数<$qsi，并检查它是否与显式状态qei组成有效对。如果是，则将对（qei，<$qsi）添加到S中。另一方面，如果（qei，qsi）不在I1中，对于某些qsi∈Qs，该算法将所有有效对（qei，qsi）加到S上.换句话说，该算法将当前有效的显式符号状态集替换为它的补集。01S←02 为每一个人 ∈Qedo03if（qei，qsi）isinI1forsomeeqsi ∈Qs然后04开始05if（Tsij<$$>qsi）/=falseandd（qei，<$qsi）∈/I1则06当e（qei，Li）∈Th，（qej，Tsij）∈Li时，add（qei，<$qsi）toS07端08其他09对于每个Tsij 其中e（qei，Li）∈Th且d（qej，Tsij）∈Li10add（qei，qsi）toS其中Tsij=qsi<$qsj联合Costa等理论计算机科学电子笔记130（2005）3013135.2.2析取给定γ和δ分别由输入显式符号状态表I1和I2表示，该算法产生输出显式符号状态S，其中δγ成立.首先，I1中的显式符号状态存储在S中。接下来，I2中的显式符号状态也被复制到S。具有共享显式状态的显式符号状态通过执行其符号状态的析取来合并。01S←02对于每对（qe，qs）I1，03将（qe，qs）加到S04 对于I2do的每个pair（qe，qsi）05if（qe，qsj）∈Sforsomeqsj ∈Qs，则06在S中用h（qe，qsj<$qsi）替换e（qe，q sj）07其他08add（qe，qsi）tooS5.2.3EX（X）给定由输入显式符号状态集合I1表示的EXO，该算法产生输出显式符号状态集合S，其中EX（EXO）成立。对于I1中的每个显式符号状态（qej，qsj），首先算法计算显式分量qej的前驱集合E。 之后，对于每个qei∈E，它计算符号状态qsj的前趋qsi，限制为Tsij，并将（qei，qsi）添加到S。01S←02foreachhpairr（qej，qsj）ofI1do03 begin04E←{qe|<$（qe，qej）∈Te}05为每一个人 ∈Edo06开始07qsi ←EXsymb（Tsij，qsj）08if（qsi /=false），则09开始10if（qei，qsk）isinSforsomeeqsk ∈Qs，则11在S中用h（qei，qsk<$qsi）替换e（qei，q sk）12其他13add（qei，qsi）tooS14端15端16端注意，EXsymb（Tsij，qsj）在符号转换Tsij上产生qsj的前导，其中Tsij是与从qei到qej的显式转换相关联的符号转换。这个限制保证了显式转换（qei，qej）和符号转换（qsi，qsj）分别在显式和符号模型中同时发生314联合Costa等理论计算机科学电子笔记130（2005）3015.2.4E（γ）给定λ和γ分别由输入显式符号状态集I1和I2表示，该算法产生输出显式符号状态集S，其中E（λ U γ）成立。该算法计算E（U γ），确定γ成立的状态，并向后查找成立的状态，直到收敛到E（U γ）成立的最大集合。01S←对于每对（qe，qs）的I2，将（qe，qs）加到S上04 做05继续←false06辅助←EX（S）07对于每对（qe，qs）的Aux，08如果（（qe，qs）不在S中且（qe，qs）在I1中），则09开始10将（qe，qs）加到S11continue←true12端13 while（继续）因为E（U γ）在γ成立的状态下成立，所以算法首先将I2的状态加到S上。之后，它计算S中状态的前身，名为Aux，使用之前在显式符号状态上定义的EX算法。包含在I1中但还没有包含在S中的Aux的状态被加到S中。当跨越行06-11的循环中的S5.2.5EG（乙）EG（n）的显式符号算法是在传统的显式EG算法的基础上改进而来的。显式EG（EG）是在修改后的状态图上计算的，在修改后的状态图中，删除了所有不保持EG的状态，过渡关系相应地受到限制。 在此基础上，该算法的显式版本是基于强连通分量（SCC）的计算。在显式符号版本中，原始状态图必须修改，以便相关状态是状态的显式和符号分量都成立的状态。 因为公式是以从基本子公式到更复杂的子公式以自底向上的方式计算的结构表示给出的，所以用于在显式符号模型上计算EG的相关状态的集合对应于集合I1的输入显式状态，因此，首先我们必须从显式符号状态图所有在I1中找不到的状态。在显式-符号状态图中，关于符号状态的信息通过与显式转换相关联的符号转换来记录，因此符号状态的确定需要额外的计算以从符号转换中存在地量化出下一个状态变量。联合Costa等理论计算机科学电子笔记130（2005）301315SJJJJ下面的算法用于计算输出显式符号集J其中，EG（n）成立。 注意，Xs代表下一个状态的集合符号变量01 对于每个qe∈Qe，J02对于所有qs∈<$X（Ts），if（qe，qs）∈/I1，其中e（qe，L）∈JTh，（qe，Ts）∈L03从状态图中消除qeJ04 SCC←{C|CisanontrivialSCCofTh}05 S←JC∈SCC {（qe，qs）|（qe，L）∈ Th，（qe，Ts）∈ L，qs=<$Xs（Ts）}06S←J07 while（S）08开始JS）do09S←SJ J10对于每个h（qe，qs），其中e（qe，L）∈Th，（qe，Ts）∈L，qs=Xs（Ts）do11if（qe，qs）∈/S则12将（qe，qs）加到S13端在上述算法中，跨越线01-03的循环用于生成J修改状态图，其中，Th。 对于每个显式状态qe，循环查找与某些显式转换相关联的符号转换Ts，其中qe是当前状态。第02行计算当前符号状态的集合J J其中Ts的跃迁来自于，Xs（Ts）。若存在qs∈ <$Xs（Ts）使得（qe，qs）属于I1，则在显式符号状态图上保持qe否则，从状态图中消除qe之后，第04行计算非平凡强连通分量，仅考虑JTh的显式转换。 这样的计算可以从算法中进行调整。例如，Tarjan的Rithm [18]。接下来，第05行将属于强连通分量的所有显式符号状态添加到解S中。最后，从06到13的行用于查找所有导致S中状态的状态。6微波炉型号在这一节中，我们给出了一个例子，以阐明显式符号模型的生成和相关技术和算法的应用。尽管我们在前面关于建模语言的讨论中提到了替代位协议，但出于教学原因，我们在描述微波炉行为的小示例上说明了模型检查，摘自[11]。316联合Costa等理论计算机科学电子笔记130（2005）3016.1微波炉模型的分解假设微波炉的行为由过程（Q，X，T，q0）建模，由图4所示的Kripke结构给出，其中状态集合Q由椭圆表示，变量集合X由椭圆内所示的命题表示，即X={开始，关闭，加热，错误}，过渡关系T由弧表示，q0=S1。为了清楚起见，每个状态都用在该状态中为真的两个原子命题来标记以及对国家中虚假命题的否定。弧上的标签表示导致转换但不是Kripke结构的一部分的操作。见图4。 微波炉模型。假设集合X被分解为分别由显式命题和符号命题组成的子集Xe={start，close}和Xs={heat，error}现在，考虑一个特殊的观点下的状态集，其中只有显式的命题很重要。由于具有相同的显式命题集的状态在这种显式观点下是不不同的，因此这些状态被认为是相同的，并被投射为一个显式状态。图5示出了考虑显式命题（a）的状态分组和生成的相应显式过程（Qe，Xe，Te，q0e）（b）。注意我们还有另一组状态，Qe，以及另一组仅由明确命题组成的命题，Xe。图5（b）中的弧对应于显式过渡关系Te，并已被标记，以揭示它们投影的原始过渡自然，qoe=ES1。符号过程（Qs，Xs，Ts，q0s）也是以类似的方式生成的，即从符号的角度考虑原始模型。图6联合Costa等理论计算机科学电子笔记130（2005）301317图五、显式状态（a）和相应的显式模型（b）的映射给出了符号状态的分组（a）和相应的符号过程（Qs，Xs，Ts， q0s）（b）。图六、符号状态（a）和相应的符号模型（b）的映射6.2显式符号微波炉模型鉴于图5（b）和图6（b）中所示的显式和符号模型，具有共同标签的递归、显式和符号转换应链接在一起，以便在模型检查期间建立它们的相互依赖性。本小节探讨了这种组合模式的运作，318联合Costa等理论计算机科学电子笔记130（2005）301检查CTL表达式。表达式EX（<$close_error）是感兴趣的表达式，因为它允许 我 们探 索 一 些更 重 要 的CTL 运 算 符。 根 据 前 面的 划 分 ， close∈Xe，error∈XS.请注意，所有的算法都产生显式符号状态作为输出。查找紧密保持的状态通过使用用于处理显式原子命题的算法，第02行，我们生成闭合保持的显式状态，E={ES3，ES4}。跨越线03-05的循环生成闭合成立的显式符号状态的集合S，使得S={（ES3，SS2），（ES3，SS3），（ES4，SS1），（ES4，SS2），（ES4，SS3）}。查找紧密保持的通过在显式符号状态集上使用否定算法，其中关闭保持，特别是第04-07行，我们生成S={（ES1，SS2），（ES2，SS1）}。查找错误成立的状态通过使用处理符号原子命题的算法，第02行，我们有qsi表示集合{SS1}。行03 - 09产生S={（ES2，SS1），（ES4，SS1）}。查找接近错误成立的通过使用析取算法，第02-03行，我们添加每个状态，-close保持到输出集合中。之后，第04-08行包括错误保持在输出集中的状态，产生S={（ES1，SS2），（ES2，SS1），（ES4，SS1）}。查找EX（<$close_error）成立的状态给定输入状态集I1={（ES1，SS2），（ES2，SS1），（ES4，SS1）}，考虑按所示顺序对其进行处理。EX算法的外循环的每次迭代都考虑一个特定的输入显式符号状态。对于第一个状态（ES1，SS2），该算法最初通过使用行04来计算其显式分量ES1的前代子集合E1。之后，跨越行05-15的循环通过仅考虑与相关显式转换相关联的符号转换来计算符号分量SS2的前导。相关的显式转换是从E1到联合Costa等理论计算机科学电子笔记130（2005）301319ES1.每一个符号前趋子及其对应的显式前趋子构成了S1的显式符号状态。下面，我们展示了EX算法外循环的第一次到第三次和最后一次迭代的结果第三次迭代的显式符号状态集S3是EX（<$close_error）成立的状态。这种显式符号状态对应于原始状态{S4，S3，S1，S5，S2}，正如预期的那样。E1={ES3}S1={（ES3，SS3），（ES3，SS2）}。E2={ES 1，ES 4}S2={（ES3，SS3），（ES3，SS2），（ES1，SS2），（ES4，SS1）}。E3={ES 2，ES 3，ES 4}S3={（ES3，SS3），（ES3，SS2），（ES1，SS2），（ES4，SS1），（ES2，SS1）}。7显式符号模型的灵活性我们的显式符号模型有重要的DIFFERENTIAL方面的SLAM项目。我们的方法是更一般的，而不是处理一个固定的方法，其中控制流和数据流信息必须分别有显式和符号表示。显式符号模型允许我们根据任何策略在显式空间和符号空间之间移动变量。因此，我们可以尝试各种组合，并选择最适合系统需求的组合例如，考虑具有数据相关控制的系统，即，控制流依赖于符号表示的变量的评估的系统。在这种情况下，我们有机会通过将这些符号变量移动到显式模型来提高整体性能，减少显式和符号表示之间的交互当然，还涉及其他问题，如这些符号变量与其余变量之间的依赖关系，但所提出的显式符号模型可以支持这种配置，只要它是有利的。作为另一个例子的通用性的可扩展性实现，我们的显式符号模型也支持分区的变量，完成SLAM。因为IF系统的控制保护中涉及的程序计数器和变量确定控制流信息，320联合Costa等理论计算机科学电子笔记130（2005）301为了实现这一目标，它必须将这些变量移到显式模型中，一个类似于SLAM的分区。因此，显式符号模型提供了使用更灵活的环境来评估不同表示并选择改进模型检查过程的环境的可能性。8最后发言在本文中，我们提出了一个模型，结合显式和符号表示。所设想的显式-符号模型认为，显式和符号技术应使用在一个集成和同步的方式，使我们能够有一个更好的探索的搜索空间的建模系统。因此，我们的主要贡献是为系统的形式验证提出了一个灵活的环境。目前，我们的工作是驱动显式符号模型及其算法的计算实现，考虑中间格式中指定的系统。这样的实现将帮助我们改进概念模型，并使我们能够衡量不同表示对控制和数据流密集型系统的验证的影响。根据文献，它似乎是一个很好的选择，表示控制流显式和数据流象征性，如在SLAM。 未来的实验将有可能获得更多的信息来回答这个问题。引用[1] 放大图片作者：Thomas Ball，Rupak Majumdar，Todd D. Millstein和Sriram K.拉贾马尼 C程序的 自 动 谓 词 抽 象 。 SIGPLAN Conference on Programming Language Design andImpl