多级完整性策略下的Web应用建模：形式化方法与模型检测

理论计算机科学电子笔记157（2006）167-185www.elsevier.com/locate/entcs基于多级完整性策略的Web应用建模G. 阿马托1理工科大学毕业。d'AM. Coppola，S. Gnesi2Istituto di Scienza e Technologie dellF.斯科扎里湖Semini3Dipartimento diInformaticaUniversita`diPisa，Italy摘要我们提出了一种形式化的方法来验证Web应用程序的可靠性，通过建模其组成对象之间的相互作用。建模利用了最近的“多级完整性”机制，该机制允许具有动态变化的可靠性的对象在应用程序中进行协作。 该方法的新颖之处在于能够描述对象可以修改的系统 它们自己的完整性级别，并对其他对象的此类更改做出反应。 该模型是形式化的，一个进程代数，属性使用ACTL时态逻辑表示，并且可以通过模型检查器进行验证。 上述模型的任何实例都继承了已建立的属性和证明技术。 为了证实我们的建议，我们考虑了几个Web应用程序的案例研究，展示了如何表达特定的有用属性及其验证模式。示例范围从在线旅行社、检测恶意网络机器人的反向图灵测试，到对等系统中的内容交叉验证关键词：形式化方法，模型检测，进程代数，时态逻辑。1电子邮件：amato@sci.unich.it2电子邮件：{coppola，gnesi}@ isti.cnr.it3电子邮件：{scozzari，jazi}@ di.unipi.it1571-0661 © 2006 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2005.12.053168G. Amato等人/理论计算机科学电子笔记157（2006）1671引言形式化方法越来越多地被用于验证分布式系统的设计，并且已经证明在指定商业和安全关键软件以及验证协议标准和硬件设计方面是成功的[6，11]。越来越多的人认为，在系统的生命周期开发中采用形式化方法将保证更高水平的可靠性，并通过从软件开发的最早阶段揭示可能导致后续故障的不一致性、模糊性和不完整性，大大增加对系统的理解。特别是模型检查技术[8，9]已经成为成功的形式验证技术。它们被定义为在表示系统行为的有限状态模型上自动检查系统属性（表示为时序逻辑公式）的真实性。非专家用户也可以轻松使用模型检查器。由于这个原因，模型检查在工业中比其他验证工具更受欢迎，目前有许多有效的验证环境，基于模型检查算法[7，14，19]。在过去的几年中，基于WEB的分布式应用程序已经得到了广泛的普及。一些系统已经导致了越来越多的需求的进化范式设计和控制的开发应用程序在WEB上。利用WEB作为底层平台的主要优势可以概括如下.WEB提供了统一的机制来处理计算问题，这些问题涉及大量物理分布和（内部）自主操作的异构组件。从概念上讲，WEB服务是驻留在网络节点上的独立组件。每个WEB服务都有一个接口，该接口可以通过标准网络协议进行网络访问，并描述了服务的交互能力。WEB上的应用程序是通过组合和集成WEB服务来开发的。Web应用程序表现出与经典分布式系统相同的验证问题。因此，我们也可以在Web应用程序中扩展用于验证它们的技术和工具。我们在本文中提出的形式化框架是基于[17]中提出的一些结果，其中对通信对象之间的交互策略进行了形式化验证。该政策是多层次完整性政策，在容错系统设计的背景下定义，以提高系统的可靠性。策略的最初定义只是由一组声明性规则组成：它可以通过定义通信协议来实现。执行完整性策略的协议在形式上被指定为一组交互进程，G. Amato等人/理论计算机科学电子笔记157（2006）167169进程代数我们考虑特定的交互模式，它隐含了最复杂的交互模式，并检查它们表示不违反完整性规则的时态逻辑公式。2.多层次的诚信政策完整性策略是在容错系统领域定义的。容错系统的设计通常包括故障和失效的建模或容错模式的定义。在软件体系结构层次上，容错模式通常描述一组组件及其交互。如果容错系统中的某个部件的故障会严重影响整个系统的可靠性，则该部件被称为关键部件。容错模式，特别是完整性策略，被定义为防止从非关键组件到关键组件的故障传播。完整性策略为每个系统组件分配一个完整性级别，范围包括一组有限的自然值，并说明通信模式。可能是关键的组件被指定为高完整性级别。在面向对象的框架内定义了多层次完整性策略该政策建立在Biba的[ 4 ]和Clark和Wilson的[ 10 ]政策基础上BibaClark-Wilson模型定义了一组基于商业数据处理实践的细粒度规则，以维护数据完整性。如果有可能证明数据没有失去其完整性，则数据可以流到低水平并返回。多级完整性策略允许某些对象通过降低其完整性级别来接收低级数据。基于一组通用的交互规则，它推广了Clark-Wilson策略，该策略利用了每个应用程序域的特定过程。该政策基于以下概念：完整性水平（IL）的范围从最低的0到最高的3。数据被赋予产生它们的对象的完整性级别单级对象（SLO）是其完整性级别在计算期间不改变的对象。因此，级别n的SLO仅允许从级别≥n的对象接收数据。多级对象（MLO）是该策略的核心：它们的完整性级别可以动态修改，因为它们可以接收低级别数据。为此，MLO被赋予三个值：maxil表示MLO可以具有的最大完整性级别。它也被称为MLO的本征电平，因为它是在170G. Amato等人/理论计算机科学电子笔记157（2006）1673il=32一il=2一个1RRminil=1RRminil=10MLOMLOFig. 1. MLO的行为：虚线箭头表示MLO的演变，粗箭头表示绑定请求对应的答案。应用程序的设计它是一个静态值。minil，表示MLO的完整性级别在与其他对象交互时可以达到的最小值它是在调用时根据调用级别设置的。在调用的应答返回后，不会保留它的内存：minil对于调用是本地的IL是当前完整性级别。它在调用时被设置为一个介于maxil和minil之间的值，如果在计算期间接收到较低级别的数据以服务于调用，则该值会减小。另外，il对于每个调用都是本地的。该策略要求在每次调用MLO时创建一个新的MLO实例。因此，MLO不能用于实现必须存储某些数据的组件。这意味着从功能的角度来看，MLO是一个无状态的对象：只有SLO可以存储数据。在图1中，我们提供了响应于调用的MLO的演变的示例：当maxil= 3的MLO接收到级别1的读取请求时，它设置其minil：不能返回完整性级别小于1的应答。il的值等于maxil：读请求不会破坏MLO的完整性级别。假设MLO需要委托部分应答构造，向第三个对象发送另一个读取请求。 分配给请求的级别等于minil：如果大于或等于minil，则接受对此请求的回答。由于答案的完整性级别是2，所以MLO可以接受它，但il被降低到级别2。 最后，提供对第一请求的应答，其电平等于当前il，并且MLO恢复其初始状态。将maxil值分配给一个对象应该根据其可信度级别来完成例如，该值可以由认证机构分配。在一个更加解耦的世界中，我们可以预见这样一种模型，在这种模型中，每个应用程序都以这样一种方式设计，即组件声明自己的maxil，这必须被交互方接受G. Amato等人/理论计算机科学电子笔记157（2006）167171条件A BSLOASLO、 BMLOAMLO， BSLOA BMLOA读 Bil（ A）≤ il（ B）il（ A）≤ maxil（ B）minil（ A）≤ il（ B） minil（ A）≤ maxil（ B）A写 Bil（ B）≤ il（ A）总是il（ B）≤ il（ A）总是Ar-w Bil（ A）= il（ B）il（ A）≤ maxil（ B）minil（ A）≤ il（ B）≤ il（ A）minil（ A）≤ maxil（ B）E. E.ASLO、 BMLOA BMLOA读 Bminil（ B）：= il（ A）;il（ B）：= maxil（ B）minil（ B）：= minil（ A）;il（ B）：= maxil（ B）A写 Bil（ B）：= min（ il（ A），maxil（ B））il（ B）：= min（ il（ A），maxil（ B））Ar-w Bminil（ B），il（ B）：= il（ A）minil（ B）：= minil（ A）;il（ B）：= min（ il（ A），maxil（ B））表1方法调用被接受所需满足的条件，以及接受后对象级别上的结果。验证对象（VO）用于从低级对象中提取可靠的数据，并提供固定完整性级别的信息。在实际系统中，有时需要从不可靠的来源（如传感器）获取数据，并将其用于关键任务。但是，这种使用可能会降低整个系统的级别或违反完整性策略。验证对象是升级这些数据完整性级别的安全方法。验证对象的一个例子是使用冗余数量的数据源，并使用适当的算法对其进行过滤。例如，可以使用投票策略。这些政策是众所周知的文献，特别是在分布式容错社区。其中，我们回顾了拜占庭将军问题的解决方案[20]，其中在存在故障的情况下寻求多个节点之间的协议。为了验证投票算法，我们可以应用[3]中给出的结果。给出了一组规则，描述了对象对之间所有可能的通信我们在表1中列出了它们：我们分别将A和B称为调用对象和被调用对象。表的第一部分考虑调用条件。如果不满足指定的条件，则拒绝调用。如果它被接受，则被调用的对象（如果是MLO）可能必须更改其完整性级别，如表的第二部分所示，其中考虑了调用事件。在读或读写调用的情况如果调用对象是MLO，则返回的数据可以如下降低其完整性级别：il（A）：=min（il（A），il（B））。通信模型基于方法调用的概念。172G. Amato等人/理论计算机科学电子笔记157（2006）167ǁ\a： P动作前缀执行操作a，然后执行进程P。切。行动a在行动中P+ Q不确定性选择进程行为之间的选择P与过程 Q的关系并行组合进程P和Q的交错执行。的两个过程在互补输入（？）输出（！）行动P a 操作限制操作a只能在同步内执行P=P′过程定义它包括递归表2CCS语法片段方法调用也被分配了一个完整性级别。特别是，读、写和写入请求的电平对应于被写入的数据的电平，读取请求的电平对应于要读取的数据的最小可接受电平。读写请求被分配两个完整性级别，一个用于读，一个用于写。3正式确认方法已根据以下步骤验证了多级完整性策略。我们遵循相同的方法来验证案例研究。– 使用CCS进程代数对机制进行形式化规范[21]。进程代数基于简单的语法，并提供了严格的语义，定义在标签转换系统（LTS）方面。进程代数非常适合描述交互策略，因为策略定义从对象的功能中抽象出来，要指定的相关事件是可能改变对象完整性级别（状态）的对象调用（动作）。在表2中，我们给出了下面使用的CCS运算符的子集– 使用ACTL时序逻辑[13]来描述所需的属性。ACTL是一个分支时间时序逻辑，其解释域是LTS。它是CTL[16]的基于动作的版本，非常适合于根据它执行的动作来表达系统的属性。我们使用ACTL的一个片段，由以下语法给出，其中φ表示状态G. Amato等人/理论计算机科学电子笔记157（2006）167173........属性：φ：：=true false φφJ[μ]φ AG φ A[μU μJ]（1）在上述规则中，μ是一个作用公式，定义为：μ：：=true aμ fora∈Act我们在这里提供一个非正式的描述ACTL运算符的语义形式语义在[13]中给出。任何状态都满足真，没有状态满足假。 一个状态满足φφJ当且仅当它满足φ和φJ。一个状态满足[a]φ，如果对于所有用a可达的下一个状态，φ为真。AG φ的含义是φ现在为真，将来永远为真状态P满足A[μU μJ]4，当且仅当在从P出来的每条路径中，μJ最终将被 执行 。还 要求 在μJ之 前只 能执 行 μ 或 τ一 个有 用的 公 式采 用A[trueUa]的形式这意味着动作A最终将被执行，并且任何动作都可以在A之前执行：这是表达活动性的最简单方式。安全性可以用AG[a]false来表示，这意味着动作a永远不会被执行。– （1）有限状态（Finite State）模型。为此，我们使用 JACK（JustAnother Concurrency Kit）验证环境[5]的工具，它基于进程代数、LTS和时态逻辑形式主义的使用，并支持系统开发过程的许多阶段。– 使用JACK，FMC中提供的ACTL模型检查器，根据模型检查ACTL公式。3.1多层次诚信政策的验证多层次完整性政策必须保证不同组件之间的交互不会影响应用程序的总体置信度非关键组件不会破坏关键组件。特别是，低完整性级别的数据不能流到更高的完整性级别（除非通过验证对象）。这个条件应该适用于孤立的对象和对象间交互的任何模式。在[17]中，验证了以下属性：(i) 具有内在层次i的对象不能提供层次j> i的答案。(ii) 内部级别为i的对象不接受级别为j > i。[4]这是公式A[tru e{μ}U{μ′}true]的A C TL的速记法。174G. Amato等人/理论计算机科学电子笔记157（2006）167≤≤ǁ(iii) 如果具有本征电平i的MLO接收电平j i的读取请求，并且为了服务于该请求，它用读请求调用小于j的本征级别Maxil的第三对象，则它不能应答初始请求。实际上，由于接收到新的数据，其水平降低到第三对象的最大(iv) 如果具有本征电平i的MLO接收电平j i的读取请求，然后是级别k j的写请求，那么它仍然可以应答读请求。换句话说，它的级别不会因为并发调用而降低。4开放系统的验证[17]中提出的模型假设系统的所有组件及其关系都是已知的。在网站规范的情况下，这个假设不能得到满足，因为我们只分析了系统的一部分，我们只知道其余组件（环境）的接口为了检查子系统的属性而这可以被认为是环境与特定子系统的接口。其结果是一个新的系统，其中更多的计算是允许的。形式验证可以通过观察涉及我们感兴趣的系统部分的动作来完成。由于我们允许更多的计算，即在计算树中有更多的轨迹，因此我们可以确保任何可以在新系统上验证的LTL公式在原始系统中确实成立。因此，我们将自己限制在可以用LTL和CTL表示的属性上，如4.2节所讨论的。4.1过程接口我们首先需要定义一个正式的接口概念，用于在CCS进程代数中表示的系统组件。这是通过使用限制操作符和一个模拟世界其他部分的虚拟进程来实现的。设P是作用集ActP上的一个过程。我们可以想象有一个过程W来描述世界的其余部分，因此我们想验证整个系统P W。当然，这是不可能的，因为我们无法指定所有可能的组件。实际上，我们对进程P和世界其他地方之间的通信不感兴趣。我们的想法是考虑过程W到P的界面，而不是过程W。为此，我们需要引入一个虚拟过程，我们使用它来挑选出我们感兴趣的W的适当接口。让DW，P成为虚拟人G. Amato等人/理论计算机科学电子笔记157（2006）167175||\||ǁ- {}过程DW，P=<$a1：DW，P+<$a2：DW，P+. . . +n：DW，P（2）其中{a1，...，a n}= Act W\Act P，Act W（resp. 行为P）是W（相应地）的动作的集合。 P），a′i是a i的补数a′i。 我们定义了W w.r.t. P作为过程WP=（W D W，P）（Act WzAct P）。通过这种方式， 我们获得了一种隐藏机制：我们只观察到参与的动作。P和W之间的通信。实际上，对于我们的目的，任何弱迹等价于WP的过程都将是可满足的，即任何表现出与W P相同行为的过程。当我们只观察系统的痕迹时。在下文中，我们将接口称为任何此类进程。因此，给定Ww.r.t.我们简单地考虑系统P||I.例如，给定P=？请求：！问Google：？google：！回复我们不想观察谷歌网站与其他网站的互动那么我们可以选择吗？问Google和！阅读谷歌作为唯一的行动，我们感兴趣的，并应在谷歌的界面描述4.2ACTL的线性片段我们的目标是验证CCS代理商定义的工艺上的ACTL公式。由于我们采用了上面的界面概念，我们对那些公式特别感兴趣，一旦证明了PI，其中I是Ww.r.t.的任何接口。P，他们也支持P W。换句话说，我们希望将自己限制在ACTL的一个片段上，这个片段保持弱迹等价。命题4.1在（1）中定义的ACTL的片段保持弱迹等价。5通过将（1）中的每个公式转换为等价的ALTL公式来进行命题的证明。一个ALTL公式是一个ACTL公式Aφ，其中φ不包含任何路径量化器（参见[18]，了解ALTL的一个稍微不同的定义）。实际上，ALTL保留了跟踪等价性，因为X操作符能够区分静默和非静默操作。然而，如果我们考虑ALTLX，Xa（但保持导出模态φ[μ]U[μJ]φJ和φ[μ]UφJ），得到了一个保持弱迹等价的逻辑5.证据可以在附录中找到。176G. Amato等人/理论计算机科学电子笔记157（2006）1675案例研究：旅行社我们的第一个案例研究涉及的建模和分析的架构的子集的Web，这是感兴趣的用户愿意组织旅行预订机票和酒店。用户与在线旅行社交互。旅行社依次访问航空公司、旅游经营者、单体酒店以及其他专门从事酒店预订的旅行社等的网站，在这里，我们考虑一个简化的场景，有两个可靠的网站，即旅行社和航空公司Alitalia6的网站，以及一个相当可靠的酒店预订网站。我们将意大利航空公司和旅行社建模为maxil为3的MLO，分别称为ALITALIA3和TA3，将酒店预订网站建模为HOTELSEEK，一个maxil为2的MLO。所有这些网站都应该相互作用，并从许多不同的其他组件接收数据。我们希望它们能够执行自己的工作，即使接收到的数据具有较低的完整性级别。与此同时，我们还记得MLO不能存储数据：我们可以想象这些组件与一些私有SLO交互，在那里存储任何最终保留的信息。为了实现这一点，我们指定了旅行社的SLO，并将其称为磁盘。由于旅行社是级别3的MLO，因此当通过写请求访问其磁盘时，它可以处于任何级别。因此，我们引入4个磁盘，每个完整性级别一个它们是特定的由过程DISKx参数化。我们还需要一个磁盘管理器，指定为级别3的MLO，以便根据完整性级别选择正确的DISKx图2描述了最终系统的架构。下面通过实例化[17]中定义的过程给出完整的规范。当旅行社需要访问以前的预订时，磁盘可以接收读取请求读请求X是级别X的读请求动作。一般来说，这意味着调用是由SLO发出的，其中x为il，x为最小值的MLO。当旅行社需要存储新的预订时，磁盘也可以接收写请求。只有x级的请求才能得到处理。不同级别的写请求将由另一个磁盘提供服务DISK_EXPERIMENTAL（3）=？read_data（y）.！read_disk（y）.！answer_data（y）.DISK_DESIGNER（3）+？write_data（y）.！write_disk（y）.DISK_DISKER（3）磁盘_0=？read_disk（0）. DISK_0 +？write_disk（0）.DISK_0DISK_1 =？read_disk（1）. DISK_1 +？write_disk（1）. DISK_16免责声明：我们使用的公司名称和完整性级别是出于示例的目的而自由介绍的，与实际网站的可靠性没有对应关系。G. Amato等人/理论计算机科学电子笔记157（2006）167177TA3HotelSeek2意大利航空3盘2盘1盘3磁盘0管理员3图二. 旅行社的架构。磁盘_2=？read_disk（2）. DISK_2 +？write_disk（2）.DISK_2DISK_3 =？read_disk（3）. DISK_3 +？write_disk（3）. DISK_3代理HOTELSEEK接受可读写的酒店预订请求和只写的确认请求。 rw hreservey，z表示由MLO发出的请求，其中y为minil，z为il，或者由SLO发出的请求，其中il = y = z。变量y表示请求的读级别，变量z表示写级别。 w确认y表示由y为il的对象发出的级别y的写请求。 酒店预订请求按照HOTEL RES流程的规定进行处理。HOTELSEEK（2）你说呢？r_w_hreserve（y，z）.！酒店（（[y<= z][z<= 2]HOTEL_RES（y，z，2））+（[y<= 2][2<= z]HOTEL_RES（y，2，2））+（[y>2]！answer_hres（-1）. HOTELSEEK（2）+？w_confirm（y）. HOTELSEEK（2）HOTEL_RES（min，il，max）=（ [min< =0] [0< = il] ！ （ 0 ） . HOTELSEEK （ 2 ） ） +（ [min< =1] [1< = il] ！ （ 1 ） . HOTELSEEK （ 2 ） ） +（ [min< =2] [2< = il] ！ （ 2 ） . HOTELSEEK （ 2 ） ） +（[min< =3] [3< = il]！（3）. 酒店（2）+！answer_hres（-1）. HOTELSEEK（2）意大利航空的规格非常简单。诸如意大利航空公司的网站可以使用群件协议来实现。这些协议解决了多用户系统（即群件系统[1，15]）中出现的并发控制问题，这些用户的行为可能是并发的。一个典型的例子是为两个或多个同时预订机票的用户预订相同的座位。意大利航空公司的高度诚信178G. Amato等人/理论计算机科学电子笔记157（2006）167可以通过正式指定协议并通过证明感兴趣的非干扰特性来保证站点。验证可以通过模型检查来完成，例如，使用[22]中给出的结果，其中公共订阅群件协议的一些属性已被证明。意大利（3）=？r_w_freserve（y，z）. ！飞行[y = z]！return_fres（z）. 意大利（3）+？w_confirm（y）. 意大利（3）最后是旅行社。TA（3）=？r_w_booktravel（y，z）. [y = z] TA_BOOK（y，z，3）+？r_infotravel（y）. TA_INFO（y，3，3）TA_BOOK（min，il，3）= F_BOOK（min，il，3）+H_BOOK（min，il，3）+ F_BOOK（min，il，3）.H_BOOK（min，il，3）F_BOOK（min，il，3）=！r_w_freserve（min，il）. 什么？return（x）.（[x< min]！answer_booktravel（-1）. TA（3）+ [min< = x] [x< = il] TA_FINALIZE（min，x，3）+[il <= x] TA_FINALIZE（min，il，3））H_BOOK（min，il，3）=！r_w_hreserve（min，il）. 什么？return（x）.（[x< min]！answer_booktravel（-1）. TA（3）+ [min< = x] [x< = il] TA_FINALIZE（min，x，3）+[il <= x] TA_FINALIZE（min，il，3））TA_FINALIZE（min，il，3）=！write_data（il）. ！w_confirm（il）.！answer_booktravel（il）. 技术助理（3）TA_INFO（min，3，3）=！read_data（min）. 什么？return（x）.（[x< min]！answer_info（-1）. TA（3）+ [x >= min]！return（x）.TA（3））我们还需要指定系统的通用用户，该用户可以询问信息或预订旅行。User（x）=！info.（（！r_infotravel（x）. 什么？sort（y）.（（[y <0]！失败User（x））+（[y>= 0]！成功User（x）+！书（啊！r_w_booktravel（0，x）.？answer_booktravel（y）. （（[y <0]！失败User（x））+（[y>= 0]！成功User（x）在我们的测试中，我们使用一个通用流程，其中包括旅行社、航空公司、酒店预订站点、级别2的通用用户和磁盘。（HOTELSEEK（2）||意大利（3）||技术助理（3）||用户（2）||圆盘机（3）||磁盘_0||磁盘_1||磁盘_2 ||DISK_3）\read_data\answer_data\write_data \answer_hres \r_w_hreserve \w_confirm\r_w_freserve\answer_fres \r_w_booktravel \r_infotravel\answer_booktravel\answer_info \read_disk\write_disk唯一不受限制的行为是信息，预订，酒店和航班。因此，我们将在指定ACTL公式时使用它们作为第一个例子，我们想证明，如果一个客户需要预订服务（行动！预订），旅行社将要么预订酒店（行动！旅馆）或一个小旅馆（行动！飞行）之前，任何积极的回答（行动！成功）。 形式上，我们要求验证以下ACTL公式：G. Amato等人/理论计算机科学电子笔记157（2006）167179Peer1对等体2−VO3RL2RL1图三. 对等验证服务体系结构。AG[！一本[真实的{~！success} U {！酒店|！flight} true]模型检验器的结果是公式为真，并且观察到153个状态。以下公式：AG[！info] A [true {~！success} U {！酒店|！flight} true]声明，在任何信息的要求将遵循预订酒店或机票。当然，在这种情况下，模型检查器的结果是公式为假。6案例研究：点对点验证服务我们在这里描述了一个对等体系结构，用户可以查询下载视频。这是在对等系统中下载之前识别远程文件内容的具体问题的一个简单实例，其中一些或所有对等点都是不可信的，或者必须实施基于内容的访问控制。在本例中，我们假设存在两个对等点，分别位于级别1和级别2。此外，该系统包括两个反驳列表，收集帮助信息，以了解文件的预期内容是否与文件名相对应。下载内容由一个Validation对象进行过滤，该对象首先查找具有读取视频请求的视频，然后验证答案通过查询反驳列表该系统如图3所示。对等体1如果对等体没有视频，不同的价值。如果没有从两个对等体P找到视频，则验证器VO向用户发送否定回答，否则它借助于代理VAL和VAL 2的子句来验证视频内容。这涉及查询一个或多个反驳列表进程RL。180G. Amato等人/理论计算机科学电子笔记157（2006）167在这个例子中，我们从VAL和VAL 2中的实际验证算法中抽象出来，并展示了一个完全不确定的行为，可以在任何具体的解决方案中进行细化。我们的验证方法是组合的：为了证明最终系统的正确性，我们只需要验证细化步骤。事实上，这里指定的VO的抽象行为对应于任何实际验证对象的接口，VAL代理需要特定的验证算法。为了完成示例描述，我们假设对等体在视频可用时执行可见动作视频，并且用户在搜索开始时开始执行可见动作，然后成功或失败。 最后两个操作区分找到有效视频的情况与未找到视频或视频内容不正确的情况P（x）=？read_video（y）. （（[y = x]（！视频. ！answer_video（x，x）.P（x）+！answer_video（x，-1）. P（x）+（[y> x]！answer_video（-1，-1）. P（x）RL（x）=？query_video（y）. （（[y = x]！query_answer（x）. RL（x））+（[y> x]！query_answer（-1）. RL（x）VO（x）=？user_req（y）. （（[y = x]！read_video（0）.什么？answer_video（z，w）.（（[z =-1]！user_answer（-1）. VO（x））+（[z>=0]VAL（x，w）+（[y> x]！user_answer（-1）.VO（x）VAL（x，w）=[w =-1]！user_answer（-1）. VO（x）+[w>= 0]（！（0）. 什么？query_answer（y）.（啊！user_answer（x）. VO（x）+！user_answer（-1）. VO（x）+VAL 2（x）VAL2（x）=！（0）. ？query_answer（y）. （啊！user_answer（x）. VO（x）+！user_answer（-1）. VO（x））User（x）=！start. ！user_req（x）. ？user_answer（y）. （（[y <0]！失败User（x））+（[y>= 0]！成功User（x）（3）函数的表达式：||P（1）||P（2）||（1）||中文（简体）||用户（1））\read_video \query_video \user_req \answer_video\query_answer\user_answer验证过程导致生成具有524个状态的模型，针对这些状态检查了以下属性，并返回预期结果。AG [！start ] A [true{ ~！start} U {！失败|！视频}true]--公式 为真--G. Amato等人/理论计算机科学电子笔记157（2006）167181AG[！start] A [true {true} U {！视频} true]182G. Amato等人/理论计算机科学电子笔记157（2006）167图四、编辑测试：只有人类才能阅读字符序列--公式 是--7反向图灵测试瓦特[23]提出的反向图灵测试是传统图灵测试的替代，用于人工智能，要求：• 让系统扮演观察者的角色• 观察者区分人类和机器。想要模仿人类的机器应该表现出天真的心理学，这种能力使我们倾向于拟人化，并使我们能够将智能归因于他人。一个示例测试是问很多问题的测试，比如观察员将答案与一张表格进行比较，该表格是通过向相当大的人群提出同样的问题而反向图灵测试的一个变体是编辑测试[12]，通常用于在分配新的电子邮件地址时区分人类和机器。它基于所谓的解释不对称，即人类在言语、书面文本、笔迹等方面“修复”缺陷的熟练方式的不以及计算机无法达到同样的解释能力。例如，在屏幕上打印出一个如图4所示的字符的光学序列，并要求观察实体用键盘键入字符实现反向图灵测试的组件可以在我们的框架中建模为验证对象。感兴趣的WEB子集的体系结构可以按照图5所示进行建模：验证对象拦截请求电子邮件地址的实体（人或机器）之间的交互。G. Amato等人/理论计算机科学电子笔记157（2006）167183ITT3提供商3图五. WEB的子集的体系结构，包括一个反向图灵测试。8结论我们提出了一种形式化的方法来描述Web应用程序的进程代数，可以自动验证的模型检查器。通过考虑不包含否定和存在路径量化的ACTL逻辑的一个片段，我们可以引入接口的形式概念，它允许我们以模的方式证明由时间公式表示的我们利用容错系统验证中提出的验证对象的概念，并展示验证对象发挥重要作用的Web应用程序的示例。我们详细描述了两个案例研究验证一些公式的帮助下，FMC模型检查。此外，我们简单地描绘了另一个例子，其中一个常用的Web应用程序可以很容易地建模为验证对象。作为未来的工作，我们打算调查的可能性，分别验证系统的不同部分，并组成的结果。引用[1] 贝克河，编辑，[2] D.E. 贝尔和L.J.拉帕杜拉安全计算机系统：数学基础和模型。技术报告M74-244，MITRE Corp.，马萨诸塞州贝德福德，一九七四年[3] Bernardeschi，C.，A. Fantechi和S. Gnesi，防护装置内部容错机制的正式验证261[4] K.比巴安全计算机系统的完整性考虑。技术报告Tech.代表ESD-TR 76-372，MITRECo.，Apr. 一九九七年。[5] Bouali，A.，S. Gnesi和S. Larosa，JACK：Just another concurrency kit，Bulletin ofthe European Association for Theoretical Computer Science54（1994），pp.207-224[6] Bowen，J.和M. Hinchey，形式化方法的七个神话，IEEE Software12（1995），pp.34比41[7] Burch ， J. ， E.M.Clarke ， K. McMillan ， D. Dill 和 J. Hwang ， Symbolic ModelChecking1020States and Beyond ， in ： Proceedings of Symposium on Logics in ComputerScience，1990.184G. Amato等人/理论计算机科学电子笔记157（2006）167[8] Clarke，E.，E. Emerson和A. Sistla，使用时序逻辑规范自动验证244-263。[9] Clarke，E.，O. Grumberg和D.Peled，[10] D.D Clark和D.R Wilson。商业和军事计算机安全政策的比较。在IEEE Symp.《安全和隐私》，第184-194页，加利福尼亚州奥克兰，1987年。IEEE计算机学会出版社.[11] Clarke，E.和J.Wing，Formal methods：state of the Art and Future Directions，ACMComputing Surveys28（1996），pp. 627-643[12] 柯林斯，H.，The editing test for the deep problem of AI，Psycoloquy8（1997）.[13] 德尼科拉河和F. Vaandrager，Action versus State based Logics for Transition Systems，Proceedings Ecole de Printemps on Semantics of Concurrency ， Lecture Notes inComputer Science469（1990），pp. 407-419[14] Dill， D. ， A. Drexler ，A.Hu 和C.H. Yang ， Protocol Verification as a HardwareDesign Aid，IEEEInternational Conference on Computer Design：VLSI in Computersand Processors（1992），pp.522-525[15] 埃利斯角和S. Gibbs，群件系统中的并发控制，在：在Proc. SIGMOD399-407[16] Emerson，E. Halpern，Sometimes and Not Never Revisited：on Branching Time versusLinear Time Temporal Logic，Journal of ACM33（1986），pp. 151-178.[17] Fantechi，A.，S. Gnesi和L.Semini，支持多层次关键性的完整性策略的形式化描述和验证，在：C。Weinstock和J.Rushby，编辑，Proc. DCCA129比146[18] Giannakopoulou，D. J. Magee，Fluent Model Checking for Event-based Systems，Proc. ESEC/SIGSOFT FSE 2003（2003），pp. 257[19] Holzmann，G.，IEEE软件工程5（1997），pp.279-295.[20] 兰 波 特 湖 ， R. Shostack 和