理论计算机科学电子笔记147（2006）57-72www.elsevier.com/locate/entcs用于在OTS/CafeOBJ方法中生成和验证证明分数的工具包*清野孝弘1日本科学技术高等研究院绪方和宏2NEC软件北陆株式会社/JAIST二次幸吉3日本科学技术高等研究院摘要OTS/CafeOBJ方法可用于分布式系统的建模、描述和验证。规范以方程式形式书写，这些方程式被视为重写规则并用于验证规范。该方法的实用性证明了应用该方法的非平凡的问题，如电子商务协议和铁路信号系统。在本文中，我们描述了一个名为Bu的工具包，它有助于验证方法。给定用于分割案例和引理的谓词，Bu Bet会自动生成证明（称为证明分数），并使用CafeOBJ系统检查证明分数。Bu Bet亦有设施在网页浏览器上显示所产生的证明分数及验证结果。关键词：代数规范，CafeOBJ，观测转换系统，证明分数，验证。*本 研 究 是 文 部 科 学 省 科 学 技 术 振 兴 特 别 协 调 基 金 中 “ 促 进 电 子 研 究领 域 的 技 术 转 让 ” 项 目 的 一 部 分 。1Email：t-seino@jaist.a c. JP2电子邮件地址：ogatak@acm.org3Email：kokichi@jaist.a c. JP1571-0661 © 2006 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2005.06.03758T. Seino等人/理论计算机科学电子笔记147（2006）571介绍抽象机器和抽象数据类型都可以在CafeOBJ[4]中指定，这是一种代数指定语言。抽象机器的代数规范被称为行为规范。行为规范以方程形式书写，这些方程被视为重写规则并用于验证行为规范。重写是实现等式推理的一种有效方法，等式推理是最基本的推理方式，可以缓和证明的困难，否则证明可能会变得难以理解。我们使用观测转换系统（OTS;这是可以直接写在方程中的转换系统）作为抽象机器，并一直在开发一种验证行为规范的方法。这种方法被称为OTS/CafeOBJ方法[15]。在OTS/CafeOBJ方法中，系统被建模为OTS，OTS用CafeOBJ编写，并通过在CafeOBJ中编写证明（称为证明分数）并通过重写检查证明分数来验证OTS具有属性。我们已经通过案例研究证明了它的有用性，其中包括[13，14，17]。然而，在案例研究中，基本上证明分数完全是使用常用的文本编辑器（如Emacs）手工编写的，这会受到人为错误的影响，因此可能会忽略一些需要考虑的情况然后，我们设计并实现了一个名为Bu et的工具包，它可以帮助OTS/CafeOBJ方法进行验证。给定用于分割案例和引理的谓词，Bu Bet会自动生成证明分数，并使用CafeOBJ系统检查证明分数。虽然证明的成功取决于给定的用于案例分析和引理的谓词，但可以保证生成的证明分数覆盖所有案例，不包括人为错误。Bu Bet亦有设施在网页浏览器上显示所产生的证明分数及验证结果。由于Bu Probet在默认情况下只显示证明分数的层次部分，对于这些部分，应该进行进一步的案例分析和/或应该使用引理，因此这些工具可以帮助用户找到如何分割案例以及使用什么引理。这些设施还可以帮助用户阅读和理解校对分数。在本文中，我们描述了Bu的et和报告的一个案例研究，Bu的et已被应用到一个简单的互斥协议。2预赛我们假设存在一个由k表示的通用状态空间，并且已经定义了所使用的 数 据 类 型 ， 包 括 由 = 表 示 的 每 个 数 据 类 型 的 等 价 关 系 。 一 个OTS[15]S由O，I，T组成，使得1）O：T. Seino等人/理论计算机科学电子笔记147（2006）5759一组观察者;每个o∈ O是一个函数o：→D，其中D是一个数据类型，可以从观察者到观察者;给定两个状态1，2∈，mwrtS中的等式（1=S2）定义为daso∈O.o（1）=o（2），2)I：初始状态的集合，使得I满足，以及3）T：条件跃迁;ea chτ∈ T 是一个函数τ： τ → τsu cht，τ（τ1）=Sτ（τ2），其中ea ch[τ]∈τ/=S，ea chτ1，τ2∈[τ];τ（τ）是τ ∈τ wrt τ的成功或成功的证明;τ 的条件cτ称为有效条件。一个S的执行是一个无限序列，它是0，1，... 对于满足初始化（I0∈I）和约束条件（I0∈{0，1， . . . }。 τ∈T。（πi+1=Sτ（πi）。如果存在S的一个执行，则状态S被称为可达的，其中S出现。本文讨论的性质只是不变量。一个谓词p被称为不变量wrtS i，它对每个可达状态wrtS都成立。观测器和传输可以被计量化，其中， 记 录 器 都 表 示 数 据，. ，im：τ j→Di和τj1，.. . ，jn：n→n，设m，n≥0，存在一个数据类型Dk，使得k∈Dk，其中k=i1，.，im，j1，.，jn.CafeOBJ[4]（参见www.ldl.jaist.ac.jp/cafeobj/）是一种代数规范语言/系统，主要基于有序代数[6]和隐藏排序代数[5，9]。抽象机和抽象数据类型都可以在CafeOBJ中指定，它有两种排序：表示抽象数据类型和抽象机状态空间的可见和隐藏排序，以及两种隐藏排序的操作符：表示抽象机状态转换的动作和观察操作符，让我们知道抽象机的状态。 操作操作符和观察操作符都获取抽象机器的状态和零个或多个数据，操作操作符返回后继状态，观察操作符返回表征抽象机器状态运算符声明的语法是[b]opOpName：排序*->排序bop用于操作和观察操作符，而op用于其他操作符。运算符是用方程定义的公式声明的语法是[c]eqTerm= Term[ifTerm]。ceq用于条件方程，而eq用于非条件方程。CafeOBJ系统使用等式作为重写规则并重写术语。CafeOBJ也基于重写逻辑。重写规则的语法是transTerm=>Term。在Bu算法中，重写规则用于指导Bu算法生成证明分数。CafeOBJ规范的基本单位是模块。CafeOBJ系统提供了内置的模块，其中基本数据类型（如真值）specified.真值的模是BOOL。由于条件方程的真值是不可分的，因此BOOL几乎60T. Seino等人/理论计算机科学电子笔记147（2006）57每个模块，除非另有说明。BOOL的导入允许我们使用可见的排序Bool表示真值，常量true和false表示true和false，运算符表示一些基本的逻辑运算符。运算符中有not_，_and_，_or_，_xor_，_implies_和_iff_，分别表示 否 定 、 合 取 、 析 取 、 异 或 、 蕴 涵 和 逻 辑 等 价 条 件 选 择 运 算 符if_then_else_fi也可用。下划线_指示放置参数的位置。BOOL在CafeOBJ系统的验证中起着至关重要的作用。如果考虑模块中可用的方程，作为重写规则，它们是完备的WRT命题逻辑。因此，任何表示命题公式总是真（或假）的项肯定会还原为真（或假）。一般来说，布尔的一个术语简化为一个排他的合取词。S是用CafeOBJ写的。 用一个 隐藏的 序列表示，s ayH，odi1， . . ，由CafeOBJ观测器更新操作器，sayo，anddτdj1，. . ，djn由C af eOBJ操作符声明，比如a; o和a被声明为bop o：HVi1. Vim-> Vibop a：HVj1. Vjn->HVk是对应于Dk的可见排序，其中k = i1，. ，im，i，j1，. ，jn. 任何一个州，即。任何初始状态，都由一个常量表示，比如init声明为操作初始化：->H我们假设每一个字母的初始值为1，... . ，im是f（i1， . . ，im）。初始值为1，. ，这是用这个方程来实现的等式0（init，X11，.，Xim）= f（Xi1，. .，Xim）。Xk是一个C af eOBJ变量，其中k=i1， . . ，im和f（Xi1， . . ，Xim）是CafeOBJtenntgf（i1， . . ，im）。 Ea chτj1，.. . ，可能会改变一个字符串的值，. ，im，如果它被应用于状态i，i，...，jn成立，可以写成ceqo（a（S，X，1，...， Xjn），Xi1，...， Xim）= e-a（S，Xj1，. 、.、 Xjn，Xi1，.. 、.、Xim）如果c-a（S，Xj1，. ..，Xjn）。S是H的CafeOBJ变量，每个Xk是V k的CafeOBJ变量。a（S，Xj1， . . ，X，j，n）表示S的成功或失败。. ，jn. e-a（S，Xj1， . . ，Xjn，Xi1， . . ，Xim）detetoi1，.. . ，我在这个系统中。 c-a（S，Xj1， . . ，Xjn）denotescτj1，...，jn.τj1，.. . ..jnd oesnothold，whi chceecan be writtenasceq a（S，Xj1，...，如果不是c-a（S，Xj1，...，Xjn）。如果oi1的值，... . ，我不认为应用τj1，. . ，jn在一个新的状态（cτj1，...，jn），则下面的等式可以被推导为：等式0（a（S，X，1，...， Xjn），Xi1，...， Xim）= o（S，Xi1，...， Xim）。T. Seino等人/理论计算机科学电子笔记147（2006）57613证明分数我们描述的证明分数表明，一个谓词P1是不变的WRTS，这是写在CafeOBJ。我们经常需要其他的谓词，比如说p2，...，pn，用于验证，尽管这样的谓词应该在验证期间找到。 L etxi1， . . . ，xi mi，其中，所述类型是Di1， . . ..，n. pi可以被写为pi（n，xi1， . . . ，xi mi）。虽然某些不变性质可以通过重写和案例分析来证明，但我们经常需要归纳，特别是关于应用的转换数的同时归纳[15我们首先声明表示p 1的运算符，...，pn和定义算子的方程。运算符和方程在一个模块中声明，比如INV（它导入写有S的模块），如下所示：操作invi：H Vi 1.. . Vimi-> Bool等式invi（S，Xi 1，...， Ximi）= pi（S，Xi 1，. ，Ximi）。对于i = 1，. ，n. Vk是表示D k的可见排序，并且Xk是V k的CafeOBJ变 量 ， 其 中 k=i1 ， ..， imi.pi （ S ， Xi1 ， . ..， Xi mi ） 是CafeOBJterdntingpi。在模块INV中，我们还声明了一个常数xk，表示Vk的任意值，k = 1，...，n.然后，我们声明表示基本公式的运算符，以在归纳情况下和定义运算符的方程中显示。运算符和方程在一个模块中声明，比如ISSTEP（它导入INV），如下所示：操作步骤i：Vi 1. Vimi-> BoolJ等式i步骤i（Xi 1，...，Ximi）= invi（s，Xi 1，...，Ximi）蕴含invi（s，Xi 1，. ......、Ximi）。对于i=1， . . ，n. s和SJ，其中在模块ISTEP中定义了H的一个表达式;s表示任意状态和状态的一个中断状态。对于基本情况，我们写打开INV红色invi（init，xi 1，. ......、 ximi）。密切对于i = 1，.，n. CafeOBJ命令open创建一个临时模块，该模块导入一个作为参数给出的模块，CafeOBJ命令close销毁该临时模块。用开和关括起来的部分是校对分数的基本单位，在OTS/CafeOBJ法对于显示a chτj1的归纳 情况，. ，j，m，j（由运算符a决定的）保留每个p，i，我们假定对于归纳情况，状态空间被分成l个子空间，尽管这种情况分析应该在验证期间进行。l个子情况中的每一个都可以通过预测来计算，其中k=1， . . ，l;这些谓词62T. Seino等人/理论计算机科学电子笔记147（2006）57spec.modinv输入.mod脚本.mod自助餐服务器J1输出证明.xml输入Gateau（客户端）输出证明.htmlPSPHTTPIPCFig. 1. Bu et工具包概述。shouldsatisfy（ca sei1h）. . . 这是真的。对于归纳的情况，我们接着写开放ISSTEP--任意对象opy1m1：->V1m1opyjm...............--假设：->Vjmj.表示情况ik的方程的声明。--继承国等式SJ= a（s，y... 、.、 y）。JM--检查红色SIHi意味着步骤i（xi，. ，ximi）。密切对于i=1，.，n且k=1，. 湖注释以--开头，以-结尾。SIHi用于加强pthesinvi（s，xi1， . . ，xi mi）和diimii（s，tiii， . . . ）and. . . 和invik（s，tik1， . . . ），其中1≤m， . . ，k≤n，ea chtk是Vk的子集。4Bu Bet：OTS/CafeOBJ方法Bu Probet是一个用于生成和显示证明分数的工具包。图1中示出了BuChaet的概述。Bu Problem由Bu Problem服务器、Gateau（一个Bu Problem客户端）、PSP（Proof Score Presenter）和CafeOBJ系统组成。Gateau有三种类型的文件：spec.mod，其中OTSS在CafeOBJ中指定;inv.mod，其中声明模块INV和ISTEP;以及script.mod，其中编写指示Gateau生成证明分数的脚本。Gateau使用HTTP协议和进程间通信（IPC）方法。给定spec.mod、inv.mod和script.mod，然后Gateau将它们传递到CafeOBJ系统，基于从三个文件中提取的一些信息生成证明分数，并将证明分数传递到CafeOBJ系统。然后，Gateau从CafeOBJ系统接收重写证明分数的结果，根据证明分数和结果生成XML格式的文件proof.xml，并将CafeOBJJJT. Seino等人/理论计算机科学电子笔记147（2006）5763文件到PSP。PSP然后从proof.xml生成一个HTML格式的proof.html文件，在Web浏览器上显示证明分数和结果。在本节的其余部分中，我们将介绍Bu Webet服务器、Gateau和PSP。4.1Buffet服务器Buffet服务器提供五种服务：1）创建新会话，2）让CafeOBJ系统加载文件，3）从CafeOBJ系统获取模块信息，将模块重构为XML文档并将其传递给客户端，4）让CafeOBJ系统减少模块下的项并将重构的结果作为XML文档传递给客户端，以及5）完成当前会话。我们依次介绍这五种服务。当客户端请求时，Buffet服务器为客户端创建一个新的会话，启动CafeOBJ系统作为其子进程，并在服务器进程和子进程之间建立IPC连接。之后，客户端可以通过Buffet服务器与 CafeOBJ 系 统 进 行 通 信 。 中 的 CafeOBJ 命 令 用 于 将 文 件 加 载 到CafeOBJ系统中。 Buffet服务器具有CafeOBJ系统通过将命令和文件名发送到CafeOBJ系统来加载文件CafeOBJ命令show用于解析模块并使用解析模块的结果，前提是开关树打印设置为on。Bu服务器通过向CafeOBJ系统发送show命令和模块名称来使CafeOBJ系统解析模块，将模块重构为XML根据解析模块的结果生成文档并将其传递给客户端。Bu服务器通过发送命令red、术语和模块名称，使CafeOBJ系统减少模块下的术语，将结果术语重构为XML文档并将其传递给客户端。在会议结束Buffet服务器通过停止CafeOBJ系统来结束会话目前的Buberet服务器实现是用Perl编写的，大约有1,200行。4.2GateauGateau有五个命令new，input，parse，verify和quit。命令new和quit对应于Buffet服务器提供的第一个和第五个服务命令输入将文件名作为其参数，并将文件上传到Buffet服务器，后者执行第二项服务。命令解析采用一个模块的名称，其中OTSS应该被指定，将其传递给执行第三项服务的Bu节点服务器; Gateau从Bu节点返回的模块（一个XML文档）中提取表示S转换及其（有效）条件的操作操作符64T. Seino等人/理论计算机科学电子笔记147（2006）57J我J我server. 动作操作符及其条件用于生成证明分数，表明谓词对于S是不变的。 命令verify采用一个模块的名称，其中应该编写一个证明脚本来证明谓词是不变的wrt S，并将其传递给Bu服务器，Bu服务器执行第三项服务; Gateau基于Bu服务器返回的模块（这是一个XML文档）和命令parse获得的信息生成一个证明分数。 对于证明分数的每一个证明段落，Gateau制作与该证明段落对应的模块（不包括包含CafeOBJ命令的语句为红色），并将该模块上传到Bu服务器，以便CafeOBJ系统加载该模块，并请求Bu服务器让CafeOBJ系统减少该模块下的项（出现在证明段落中，表示待证明的公式），通过Buffet服务器从CafeOBJ系统接收结果（XML文档）基于结果和证明分数，Gateau将它们制作成XML文档，将其保存为文件并将文件名传递给PSP。当前的Gateau实现是用Perl编写的，大约有1,400行。 在本小节的其余部分，我们将描述证明脚本，如何根据证明脚本生成证明分数。4.2.1证明对于每个要验证的谓词pi（由运算符invi证明脚本，从该证明脚本生成证明得分P1。在p i的一个证明中，对于表示跃迁τj1，. . ，jm，wegive veepr edi cat esuchasci1， . . . ，cin 用于分割案件和用于多人-lassu chasinvi1（s，ti11， . . . ）， . . . invik（s，tik1， . . . 这就需要加强vi（s，xi1， . ） 中 的 归 纳 推 理 。 . ，ximi），对于τj1，.，JM帕雷塞斯岛 这样的谓词和公式以以下形式给出：重写规则。重写规则是为了预测ci1， . . . ，cin为我而活invi1（s，ti11， . . . ）， . . . invik（s，tik1， . . . ）罗ok立基反式谓词（a（S，Yj1，. .，Yjmj））=> ci1。···反式谓词（a（S，Yj1，. 、.、Yjmj））=> cini.translemes（a（S，Yj1，. 、.、Yjmj））=> invi1（s，ti1 1，.. . ）的。···translemes（a（S，Yj1，. 、.、Yjmj））=> invik（s，tik 1，. . ）的。运算符、谓词和引理被用作关键字来编写这样的谓词和公式。之所以以重写规则的形式给出这样的谓词和公式，是因为我们可以使用CafeOBJ系统进行解析重写规则，并且不必为这样的谓词和公式实现另一个解析器。基于这样的谓词和公式来生成证明分数，这将在下面描述。T. Seino等人/理论计算机科学电子笔记147（2006）5765我JJJ1JJK4.2.2如何制作烟雾弹Givenpredicatepi（由操作员在虚拟机中指定）以进行验证、预测，. . . ，cin 使用d来拆分情况s和d，用于mulasinvi1（s，ti11， . . . ）， . . .invik（s，tik1， . . . ）使用d来表示在vi（s，xi1， . . . ，ximi），则如下生成并检查pi的得分(i) 基本情况：Gateau具有CafeOBJ系统reduce项invi（init，xi1，. . . ，xi mi）在r模INV和给定的条件下，由证明过程和结果组成。(ii) 归纳情况：对于表示转变τj1的一个迭代算子a，. . .，jm，对于每个要检查的证明段落，生成临时模块PROOF TMP，并且表示要证明的公式的项在PROOF TMP下被简化为如下：. ，jm）：k：= 1;stack：=empty;push（stack，{ci0}）;push（stack，{<$ci0}）;Whilestack/=emptydoCs：= pop（stack）;（* 设Cs为{c}，. ..，cJ}。*）的文件1N使模块mod PROOFTMP {pr（ISSTEP）opy1m1：->V1m1。..... . 你好 。 .奥皮扬：->Vjmj .jJ J表示c1，. ，cn '。等式SJ= a（s，y、...、 y）。jmj}的情况;设T为步骤i（xi 1，.，ximi）;让CafeOBJ系统在PROOF TMP下降低T;如果结果为真，则（* 证明在情况Cs中成功。* ）的文件生成证明段落和结果的XML文档;如果结果为false，则设T为SIHi，则i隐含步骤i（xi 1，.，ximi）;让CafeOBJ系统在PROOF TMP下降低T;生成证明段落和结果的XML文档;（* 如果结果为真，则证明在情况Cs下成功。* ）的文件（* 如果不是，可能需要其他引理* ）的文件否则如果k≤ini则push（stack，Cs<${ck}）;push（stack，Cs<${<$ck}）;k：=k+1;其他设T为SIHi，则i隐含步骤i（xi 1，.，ximi）;让CafeOBJ系统在PROOF TMP下降低T;生成证明段落和结果的XML文档;（* 如果结果为真，则证明在情况Cs下成功。* ）的文件（* 如果不是，可能需要进一步的案例分析和/或其他引理* ）的文件定;定k是一个整数变量，stack是一个谓词集的堆栈。push和pop是栈的常用操作符。mod是声明模块的关键字，pr是导入模块的关键字Each预测ateckJ 是第一个. . . . lnJJ 或<$（11.. . lnJJ），K K每个lκ都是文字，即形式ακ或<$ακ，ακ是原子对于穆拉。 在ca se中，ckJ是f（l1. . lnJJ），weecl是方程J JkckJ=false. 在这一点上，这是一个很好的例子。 . lnJJ，wed eclarean66T. Seino等人/理论计算机科学电子笔记147（2006）57每个Lκ的方程。在lκ是形式<$ακ的情况下，我们声明等式lκ=false。在lκ是形式ακ的情况下，如果ακ是形式left = right，则我们声明等式left = right，否则我们声明等式lκ= true。4.3PSP给定一个XML文档的证明分数和减少证明分数中的证明段落的结果，PSP生成一个HTML文档。当PSP生成的HTML文档首次显示在Web浏览器上时，结果不为真的证明段落，其结果被显示，而其他证明段落（其证明成功）被隐藏。证明段落根据用于拆分的谓词分层显示案例和每个证明通道是可点击的，允许证明通道出现和消失。PSP的当前实现是用XSLT（XSL Transformations，见www.w3.org/TR/xslt）编写的，大约有600行。5一个案例研究：一个互斥协议我们描述了一个案例研究，Bu Bunet已被应用于验证， 简单的互斥协议具有互斥属性。由多个进程重复执行的协议可以写为l1：剩余部分l2：重复直到<$fetch store（lock，true）临界区cs：lock：= falselock是一个布尔变量，最初设置为false。fetch store（x，v）原子地将变量x的值与值v交换，并返回x的原始值。每个进程最初位于位置l1。5.1互斥协议设B、P和L是布尔值、进程ID和位置（l1、l2和cs）的类型。互斥协议被建模为OTS SMX，使得1）OMX由lock：B →B和loc i：B →L组成，i∈P，2）IMX是{B ∈ L |<$lock（）i∈P. （loc i（k）= l 1）}，3）TMX由tryi：n → n，enter i：n → n和leave i：n → n组成，对i∈P，其有效条件 为 rectryi（ k ） n （ l oci （ k ） =l1） ， cente ri （ k ） n（ l oci=l2kl ock（k）），cleavei（c）s（loci=cs），定义如下：(i) L etJbetryi（）. 如果ctryi（j）成立，则nl ock（J）=l ock（j）andndl ocj（J）=（如果i=j则l2 else l o cj（j））。否则，什么都不会改变。T. Seino等人/理论计算机科学电子笔记147（2006）5767我我(ii) 令J为te ri（）。 如果ce nter（n）成立，则nl ock（nJ）=true，并且l ocj（nJ）=（如果i=j，则cs else locj（n j））。否则，什么都不会改变。(iii) 设J为el eav ei（）。 如果cleave（n）成立，则nl ock（nJ）=falseanddl ocj（nJ）=（if i=jthen l1 else locj（n j））。否则，什么都不会改变。SMX是用CafeOBJ编写的CafeOBJ规范的签名SMX是--anyinitial stateopinit：-> Sys--观测算子bop lock：Sys-> Boolbop loc ：系统Pid ->位置--动作运算符返回：系统Pid->系统返回：系统Pid ->系统返回：系统Pid ->系统返回Sys是隐藏排序，表示P，Pid是可见排序，表示P，Loc是可见排序，表示L。常量init表示任何初始状态。观察操作符lock和loc表示观察者lock和loci，操作操作符try、enter和leave表示转换tryi、enteri和leavei。这三个操作符在等式中定义为：--试试eqlock（try（S，I））= lock（S）。ceq loc（try（S，I），J）=（if I=J then l2 else loc（S，J）fi）ifc-try（S，I）.ceqtry（S，I）= Sif not（c-try（S，I））.--输入ceq lock（enter（S，I））=true 如果c-输入（S，I）。ceq loc（enter（S，I），J）=（if I=J then cs else loc（S，J）fi）如果c-输入（S，I）。ceqenter（S，I）= Sif not（c-enter（S，I））.--离开ceq lock（leave（S，I））= false if c-leave（S，I）.ceq loc（leave（S，I），J）=（if I=J then l1 else loc（S，J）fi）如果c-离开（S，I）。ceqleave（S，I）= Sif not（c-leave（S，I））.运算符c-try、c-entr和c-leavee表示ctryi、centeri和cleavei，其中定义为等式c-try（S，I）=（loc（S，I）= l1）。等式c-enter（S，I）=（loc（S，I）= l2而不是lock（S））。等式c-leave（S，I）=（loc（S，I）= cs）。5.2互斥协议（Mutual Exclusion Protocol）我们描述了SMX具有互斥性质的验证对于验证，我们所要做的就是证明谓词（loci（i）= cs）<$locj（i）= cs）<$（i=j）不变量wrtSMX。谓词由定义为以下的运算符inv1表示：等式inv1（S，I，J）=（loc（S，I）= cs和loc（S，J）= cs意味着I= J）。运算符在模块INV中声明和定义。在模块中，常量还声明了表示排序Pid的任意值的i和j操作者68T. Seino等人/理论计算机科学电子笔记147（2006）57图二、从证明分数和结果显示的Bu Bauet摘录（1）.表示在每个归纳情况下要示出的基本公式由定义为等式istep1（I，J）= inv1（s，I，J）意味着inv1（s '，I，J）。运算符在模块ISSTEP中声明和定义。在模块中，还声明了常数s和s首先，我们不使用任何谓词来分割案例，也不使用任何公式来加强归纳假设，而是让Bu Bet生成并检查inv1（s，i，j）的证明分数，并显示证明分数和结果。Bu Bunet报告说，已经检查了七个案件，七个案件中有三个证明成功。我们在图2中显示了部分证明分数和Bu Bauet显示的结果。小三角形是可点击的按钮。一个倒置的三角形意味着它的内容被显示，而一个顺时针旋转90度的三角形意味着它的内容被隐藏。图2中从顶部开始的第一个按钮对应于由enter表示的enteri的感应情况。 归纳法案例中有两个证明段落。一示出了对应于第二按钮的一个按钮，并且示出了对应于第二按钮的另一个按钮。最后一个按钮是隐藏的。证明在第二个证明段落中成功，但对于第一个证明段落，我们需要案例分析。接下来，我们使用谓词来分割情况，谓词如下所示：--尝试transpredicates（try（S，P））=>（i = pid 1）. transpredicates（try（S，P））=>（j = pid 1）.--输入transpredicates（enter（S，P））=>（i=pid 1）. transpredicates（enter（S，P））=>（j= pid 1）. transpredicates（enter（S，P））=>（loc（s，i）= cs）.transpredicates（enter（S，P））=>（loc（s，j）= cs）.--请假T. Seino等人/理论计算机科学电子笔记147（2006）5769图三. 从证明分数和结果显示的Bu Bauet摘录（2）.transpredicates（leave（S，P））=>（i = pid 1）. transpredicates（leave（S，P））=>（j = pid 1）.但是我们并没有使用任何公式来加强归纳假设。 在这种情况下，BuBauet报告说，已经检查了18个案例，18个案例中有15个证明成功。我们在图3中显示了部分证明分数和Bu Bauhet显示的结果。看图中的证明段落3，我们注意到进程j在位置cs，而lock（s）在状态s是假的，这似乎是矛盾的。因此，我们猜想谓词（loci（i）= cs）<$lock（i）也是不变的。谓词由定义为（在模块INV中）的操作符inv2表示为等式inv2（S，I）=（loc（S，I）= cs隐含lock（S））。我们还声明并定义了运算符istep2，它表示在每个归纳情况下要显示的基本公式，作为模块ISTEP中的istep1。除了分裂情况的谓词之外，我们还使用公式来加强归纳假设inv1（s，i，j），并且公式被给出为translemmas（enter（S，P））=>inv2（s，i）. translemmas（enter（S，P））=> inv2（s，j）.在这种情况下，Bu Bauhet报告说，证明在所有18个案例中都取得了70T. Seino等人/理论计算机科学电子笔记147（2006）57对于inv2（s，i）的验证，我们使用谓词来分割情况，并使用公式来加强归纳假设：--尝试transpredicates（try（S，P））=>（pid 1=i）. transpredicates（try（S，P））=>（loc（s，i）= cs）. transpredicates（try（S，P））=> lock（s）.transpredicates（try（S，P））=>（loc（s，i）= l1）.--请假transpredicates（leave（S，P））=>（pid 1=i）. transpredicates（leave（S，P））=>（loc（s，i）= cs）. transpredicates（leave（S，P））=> lock（s）.translemmas（leave（S，P））=> inv1（s，i，pid 1）.Bu Bunet报告说，已经检查了15个案例，所有案例的证明都成功了。注意，需要由inv2表示的谓词来加强由inv1表示的谓词的不变证明的归纳假设，反之亦然，这意味着如果每个证明分数被单独写入，因此，需要同时进行诱导[15]。6相关工作BOBJ[8]是一种基于序排序和隐排序代数的代数规范语言，它是CafeOBJ的 兄 弟 语 言 。 BOBJ 实 现 了 带 有 案 例 分 析 的 条 件 循 环 共 归 纳 重 写（c4rw）。给定方程（用于拆分情况）和引理，c4rw自动生成证明分数并检查证明分数。BOBJ允许我们指定如何比Bu bet更详细地拆分案例，但给出用于拆分案例的方程的用户负责方程是否涵盖了整个案例。如[8]所示，有些问题可以用c4rw很好地验证BOBJ是榻榻米系统的一部分[7]。Tatami系统提供了显示证明的设施，以使它们更好地吸引基于代数符号学（将代数规范与社会符号学相结合）的软件工程师。这些设施背后的基本思想可以用来改进我们显示证明分数的方式。已经提出了几个证明助理。他们中的许多人，都是一个人，一个人。它们在一定程度上提供了一些自动证明机制，但基本上是帮助用户构造他们的证明。用户将称为策略的命令输入到证明助手中，以在他们的证明上取得进展。策略通常将证明目标简化为零个或多个证明子目标，这些子目标希望更简单。但用户应该选择适当的策略，以成功的证明。这意味着用户基本上需要知道-T. Seino等人/理论计算机科学电子笔记147（2006）5771尽管证明助手可以防止用户犯错误，但他们的优势和经验使他们能够在没有任何证明助手的情况下自己完成证明在现有的支持使用代数规范语言验证（分布式）系统的工具中，有落叶松证明器（LP）[10]和Maude归纳定理证明器（Maude ITP）[3]。LP的设计方针是使证明助手易于使用，特别是对于工程师，但LP的用户基本上需要具有与使用其他证明助手所需的技能相似的技能。Maude ITP帮助验证用Maude[2]编写的抽象数据类型，Maude [2 ]是一种基于隶属方程逻辑和重写逻辑的代数规范和编程语言，但不帮助验证抽象机器。7结论我们已经描述了在OTS/CafeOBJ方法中用于生成和显示证明分数的Bu节点，并报告了关于验证简单互斥协议的案例研究。除了互斥协议之外，Bu et已经成功地应用于验证NSLPK认证协议[11]和Otway-Rees认证协议[16]具有保密性。引用[1] Bert ott，Y. 和P. Cast'eran，“I n t e ract i v e The ore m Pr ov i n g and d Program D ev e lo p m en t - Coq'Art：The Calculus of Inductive Constructions，”Springer，2004.[2] Clavel，M. 、F. 杜兰，S。 Eker，P. Lincoln，N. 我的天-我的天，J。 Meguerand d J. Quesad a，M au de：重写逻辑中的规范化和编程语言，TCS 285（2002），pp. 187-243[3] Clavel ， M. 、 F.杜兰 ， S 。 EkerandJ. Meseguer ， Buildingquationalprovingtoolsbyyre-e-e-ctionin rewriting logic ， in ： CAFE ： An Industrial-Strength Algebraic Formal Method ，Elsevier，2000 pp.1-31[4] 迪亚科内斯库河和K. Futatsugi，[5] 迪亚科内斯库河和K. Futatsugi，面向对象代数规范中的行为一致性，J.UCS6（2000），pp. 74比96[6] Goguen，J.一、[7] Goguen，J. A
我的内容管理
展开
