使用Spin和Escort验证UMTS协议：基于Promela语言和ASN.1数据模型的模型检测方法

理论计算机科学电子笔记118（2005）71-85www.elsevier.com/locate/entcs使用Spin和Escort的UMTS协议马蒂·卢克凯宁1芬兰赫尔辛基大学计算机科学系，邮政信箱26，00014维韦克K Shanbhag2Sun Microsystems，Divyasree Chambers，班加罗尔560025K. Gopinath3CSA部门，印度科学研究所，班加罗尔560012摘要下一代移动通信协议已经变得非常复杂，标准化机构在标准化过程中确定协议的正确性变得越来越困难。 一个方便的符号来指定协议和一种方法来分析他们的行为在一定的抽象级别可能是非常有用的。模型检查已经被证明是一种有效且相对易于使用的技术，用于验证形式化描述的行为。然而，使用模型检查有两个主要的缺点：一个是状态爆炸（现实生活中的程序的行为模型往往是非常大的）;另一个限制模型检查器的工业应用的因素是他们的限制输入语言。例如，在电信领域，标准使用ASN.1符号定义协议的数据模型，如果可以直接使用电信行业的“本地”数据定义语言构建验证模型，则会更简单在本文中，我们认为模型检查的RLC协议在UMTS系统中，看到正在进行的发展作为第三代移动通信系统。我们简要描述了ESTO，一个模型检查器，其中的行为可以通过基于Promela的语言形式化地指定，用于控制结构，但数据模型来自ASN. 1。我们讨论了RLC的验证问题，然后讨论了在验证问题上使用Eynth的结果，并与Spin进行比较，Spin也是Eynth实现的基础。作为实现ESPIN的一个侧面，我们已经能够在Spin实现中找到一些复杂的性能错误。我们相信，这种类型的保留字：模型检测，Spin，Promela，ASN.1，电信协议，RLC，UMTS1571-0661 © 2005 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2004.11.00772M. Luukkainen等人理论计算机科学电子笔记118（2005）711介绍测试和调试并发和反应式程序（如通信协议）是一项繁琐的任务，部分原因是计算环境造成的不确定性。如果一个程序是用形式语言描述的，那么它的行为可以通过数学结构来分析，比如可达图，它描述了程序所有可能的计算序列。如果这种形式定义的程序的正确性要求也使用数学符号来指定，例如时态逻辑[12]，[1]或状态自动机[10]，则可以使用称为模型检查器[2模型检查器检查程序的每一个可能的计算序列，因此它被称为穷举验证技术。由于所有可能的执行序列都被覆盖，模型检查可以完全保证程序的正确性。模型检查已被证明是程序验证中一种有效且易于使用的技术。然而，使用穷举模型检查有一个主要缺点：现实生活中的程序，例如电信协议的行为图往往非常大。在文献中，这个问题通常被称为状态爆炸。为了缓解这个问题，在过去的十年中已经采取了许多渐进的步骤，并且已经可以使用有效的模型检查器实现。Spin就是这样一个验证系统[4]。移动设备的下一代协议已经变得非常复杂，标准化机构在标准化过程中确定协议的正确性变得越来越困难。因此，如果能够使用模型检查等技术来确保标准的正确性，将是非常有益的通常，输入语言，如Promela（与模型检查器Spin一起使用），具有有限的数据结构构造集。 这可能是这种工具的大规模工业使用的限制因素。ASN.1（Abstract Notation One）[5]是一种在电信协议规范中广泛使用的数据定义语言。如果模型检查器能够增强ASN.1数据建模能力，在建立标准之前检查协议临时版本的正确性，电信领域的验证工程师1电子邮件地址：mluukkai@cs.helsinki.fi2电子邮件：vivek. sun.com3电子邮件地址：gopi@csa.iisc.ernet.inM. Luukkainen等人理论计算机科学电子笔记118（2005）7173行业将受益于这种直接在其验证工作中使用ASN.1数据模型的能力。在这篇文章中，我们报告的应用程序的EQUIPMENT模型检查的无线电链路控制协议[9]的UMTS，一个标准的第三代移动通信系统[11]。本文的结构如下：第2节简要介绍了Spin和Escape工具，以及它们之间的关系。在第3节中，描述RLC协议。第4节解释了如何对协议及其用户环境进行建模，并讨论了验证结果。结论见第5节。2自旋、电子自旋及其相互关系Spin [4]是一个有效的异步系统模型检测工具，特别是针对通信协议而设计的。Spin的输入语言称为Promela（“Process Meta Language”）。协议被建模为一组Promela进程，它们通过通道或共享变量相互通信。Promela的控制结构的设计基于SDL中的控制结构，SDL是一种自70年代以来用于指定通信协议的语言。Promela的不确定性和保护命令使得通信协议实体的行为表达非常方便。模型检查器Spin具有许多功能，如死锁检测，验证断言，系统不变量，检测非进度周期和活锁，以及指定线性时态逻辑（简称LTL）属性用于模型检查。节省大量空间和时间的算法，如位状态散列，在线模型检查和偏序约简已被纳入Spin。因此，修改Spin系统以处理ASN.1一直是ESPRIT项目的设计目标[8]。Spin有一个模拟器，它只随机检查状态空间的一部分，还有一个（生成的）验证器，它可以尝试彻底检查系统的状态空间，或者可以使用位状态散列等技术以相当高的保证水平检查状态空间的相当大的部分。Escort系统也有这些组件，并且Spin中的大多数归约策略，例如偏序归约和位状态散列，已经被当前版本的Escort支持与Spin 中的Promela类似，Escort 语言是Escort 工具的输入语言。Emela语言被设计为一个方便的结合，它将ASN. 1表示法用于Promela的数据类型和控制结构。在功能冲突的情况下，这些决定是出于语言设计的实现优雅的轻松和方便。74M. Luukkainen等人理论计算机科学电子笔记118（2005）71ASN.1可用于定义应用程序中的数据类型和常量值。然而，Promela是一种完整的语言，具有一组基本数据类型和typedef结构来帮助用户组成数据类型，以及一组可用于定义协议实体行为的控制结构。Emela语言用ASN.1取代了Promela的所有数据类型功能。因此，除了chan构造之外，Promela的所有数据类型都不会在ESTO中保留。与Promela相比，ASN.1具有更丰富和更具表现力的此外，EQUIPMENT语言还根据需要增加了运算符集。简而言之，E = Promela -{mtype ， typedef ， bit ， byte ， bool ， short ， int} +ASN.1+ 适当地重载了现有操作符的语义+一些新的操作符。此外，由于ASN.1中的子类型机制的存在，它允许用户定义数据类型，例如只有有限的一组可能值的整数，模型检查可以更有效，因为存储系统状态所使用的内存量可以减少，这自然有助于对抗状态爆炸。Spin非常有效地表示状态，但由于对齐等原因，允许状态向量中的填充和其他无关物质。由于EASIL使用ASN.1数据模型，因此它要求所有变量都尽可能地约束在值空间中，以便通过使用子类型来获取这些值。例如，如果一个整数变量从8. 15，它可以用3位来表示。此外，如果有两个变量被限制在，比如，5.七比三... 7，只有15种可能性，并且两者都可以仅用4位来表示，而不是2+3（5位）或更糟的3+3（6位）。因此，EQUIPMENT有一个称为状态压缩基础设施的关键设施，它保证在存储每个系统状态时使用最少的位数。3RLC协议通用移动通信系统（UMTS）是使用WCDMA（宽带码分多址）无线电接入技术的第三新的无线电接入技术要求无线电接入网络中的重大改变，该无线电接入网络由参与使用无线电接口的数据传输的网络元件和协议组成。无线链路控制（RLC）协议是UMTS新一代协议之一.根据OSI参考模型，它是第2层协议，提供M. Luukkainen等人理论计算机科学电子笔记118（2005）7175Iub传输WCDMA L1Iub传输WCDMA L1PDCPPDCPMacMacUE节点B RNCL3RRC /IP+应用RRC /IP+应用L2L1WCDMA L1图1.一、UMTS协议层通过不可靠的无线电接口向上层提供可靠的数据传输服务。它使用较低层提供的不可靠数据传输服务，即MAC（媒体访问控制）协议（见图1）。RLC协议在2000年3月由3GPP标准化，3GPP是由对第三代系统的管理和开发感兴趣的制造商、运营商、当局等组成的国际标准化论坛。规范[9]定义了协议的几个服务、函数和过程RLC向上层提供与数据传输相关的若干服务。根据规范[9]，该协议执行RLC连接建立和释放，以透明、未确认或确认模式传输数据，允许在数据传输期间动态设置QoS（服务质量），并通知上层不可恢复的协议错误。在本文中，我们集中在确认模式下的可靠数据传输服务的验证。确认的数据传输服务发送上层PDU（协议数据单元）并保证递送到对等实体。确认数据传输模式具有以下特征[9]：• 无差错递送：接收RLC实体仅递送无差错SDU服务数据单元（Service Data Unit，上层PDU）。• 唯一传递：RLC通过检测重复，将每个SDU仅传递一次到接收上层。• 按顺序递送：RLC提供对SDU的按顺序递送的支持，即，RLC以与发送上层实体将SDU提交给RLC相同的顺序将SDU递送给接收上层实体• 无序输送：作为按顺序递送的替代，可以让接收RLC实体以与在发送侧递送到它的顺序不同的顺序将SDU递送到上层。• 加密：该服务尚未在规范中定义。RLCRLC76M. Luukkainen等人理论计算机科学电子笔记118（2005）71−• 不适合RLC层PDU的SDU应该分段，并在协议的另一端有几种可选的ARQ（自动重传请求）方案可供选择。我们研究了停下来等待，也许是最简单的一种，用于我们的验证模型。在从用户接受新的SDU之前，必须确认上面的RRC层的每个SDU（从这一点起，其将被替换地称为用户），并且在RLC不能根据要求递送SDU的情况下，其通知发送上层实体。为了简单起见，我们省略了分割和重组过程。假设用户数据的大小，即RLCSDU（服务数据单元）的大小与RLCPDU中的数据字段的大小完全相同。为了简单起见，除了分段，连接和填充功能也可以省略。由于加密在标准中没有精确定义，我们也将其从模型中排除该规范定义了上层用于建立和释放RLC连接的配置消息的一些参数。参数用于将RLC协议实体配置为适当的模式，并定义在加密和分段中使用的参数值因为我们的模型中只有一个功能模式，根本没有加密或分段，所以参数被从配置消息中删除RLC中的连接建立阶段包括仅从上层接收单个配置请求消息初始化后，协议准备好进入数据传输阶段。我们假设在协议的两端同时建立连接（即接收到相应的消息）。这就是协议的具体说明，因为首先，MAC和RRC协议（见图1）建立物理链路，然后RRC层建立RLC连接。因此，与OSI栈中的协议相比，该协议的结构非常不同，在OSI栈中，通常需要在可以建立层n处的连接之前建立层n当从上层接收到SDU时，启动数据传输过程。对于每个SDU，RLC协议实体创建相应的PDU。SDU被放置到PDU的数据字段中，在PDU报头中具有适当的序列号。在将PDU发送到负责接入无线电接口的MAC层之后，立即设置用于PDU传输的定时器。在前一个数据传输过程完成之前，不接受用户的进一步请求。数据传输过程在发送端接收到PDU的确认时终止，或者在异常情况下，在向用户发送协议错误通知后终止。在正常情况下，发射机接收到M. Luukkainen等人理论计算机科学电子笔记118（2005）7177在重传的最大计数之前对PDU进行确认。重传通常由PDU传输定时器超时触发。当接收到具有适当序列号的确认时，PDU传输定时器被重置。具有其他序列号的确认将被忽略。在接收到PDU之后，接收侧中的RLC协议实体重新移动报头并且将SDU递送到上层。在向MAC发送相应的确认之后，它更新序列号。发送侧在接收到确认之后更新序列号。在发送方的PDU传输定时器到期并且已经达到PDU的预定最大重传计数的异常情况下它的目的是使数据传输更快，并使协议恢复到一致的状态。发送方发送复位消息并设置定时器。接收方确认消息并将序列号更新为预定义的初始值。在发送端，序列号在接收到复位消息的确认后立即更新为相同的初始值。还为重置消息定义了最大重传计数。在重置的情况下，通知用户实体。如果重置过程成功，则报告可恢复的错误;否则，报告不可恢复的错误。然后由用户决定如何继续。断开连接阶段总是由用户实体发起，包括接收来自上层的断开消息。出于与连接建立相同的原因，断开也在发送侧和接收侧上几乎同时发生。每一个连接协议实体都在接收到断开连接请求时终止，并且将为下一个连接生成新的实体4形式化建模与验证非正式地描述了RLC协议，我们现在提出的原则建模的协议和它的环境。为了比较Escort系统的功能，我们对Escort和Spin进行了建模和验证。RLC协议之下的MAC层为RLC级PDU的递送提供不可靠的传送。因此，我们将MAC建模为两个不可靠的FIFO队列，每个方向一个。当将PDU交给MAC时，它会做出不确定的决定，是进一步传递消息（将其放入队列）还是丢弃消息。78M. Luukkainen等人理论计算机科学电子笔记118（2005）71不会复制或损坏数据包。实际上，数据包的损坏由于RLC层以下的纠错过程检测并拒绝被破坏的消息，因此对于RLC来说，这类似于分组的丢弃。对于新的RLC连接，在MAC层中为其分配新的逻辑信道在我们的模型中，当RRC层建立RLC连接时，它首先动态地创建MAC连接，然后在协议的两端创建两个RLC实体，其中一个是发送方实体，另一个是发送方实体。是接收器实体。因此，在我们的模型中，RRC层被建模为两个静态实体，然后动态创建下面的层如前一节所述，连接建立大约同时发生在RLC的两端。在我们的模型中，这通过使用命令两个RRC实体打开RLC连接的“oracle”来处理。实际上，是oracle创建底层MAC层，将其句柄传递给RRC实体。然后，RRC实体创建RLC实体，并向它们传递它们用于连接的MAC句柄。oracle还用于对RRC实体可以决定在任何时间点终止RLC连接的事实进行如果发送RRC正在终止RLC连接，则通过oracle将该信息传递到在真实的UMTS栈中，RRC实体之间的实际通信通过单独的MAC连接发生。为了简化模型，我们使用了使用oracle作为中介的直接同步。因此，oracle在我们的模型中具有双重作用：它是RRC层之间的控制通信的手段，并且包含来自上层应用协议的控制，以决定何时应该创建或终止RLC连接模型的结构如图2所示，其中静态实体用实线绘制，动态实体用虚线绘制。神谕及其信号用虚线表示每个单独的协议实体被建模为一个EASN进程。RLC发送器和RLC接收器过程的行为在图3和图4中以扩展状态自动机的形式进行了概述。在这两个过程中，从上面一层接收到断开消息会导致立即终止，这是从自动机描述中排除的。在图中，转换是以保护命令的方式指定的，例如，从RC？CR_ab：= 1表示当接收到来自用户的CR消息时，ab的值被设置为1。MAC层指定有两个独立的不可靠FIFO缓冲器，一个从发送RLC实体到接收实体，另一个用于另一个方向。完整的规格在两个EQUIPMENT和Promela格式可以找到在M. Luukkainen等人理论计算机科学电子笔记118（2005）7179从RRC？来自_rrc的CR？DT（sdu）空闲就绪ab=1 cnt=0cnt MAX−>CNT++num==ab−>ab++num！=AB−>CNT+Mac！数据（sdu，ab）从Mac？重定位- >to_rrc！状态RE;从Mac？ack（num）发送cnt==MAX−>cnt=0cnt ==MAX- >to_rrc！状态UE;cnt ==MAX−>cnt=0Mac！重置为cnt MAX−>CNT++复位连接/断开Oracle连接/断开创作RLC−接收器RLC−发送器RNC_RRCUE_RRCmac层图二. 规范结构图三. RLC发送方空闲从RRC？CR−> exp=1准备Mac！resetAck- > exp =1 from_mac？复位num==exp−> exp++num！=exp从Mac？data（sdu，num）- > to_mac！ack（num）见图4。 RLC接收机http://www.cs.helsinki.fi/u/mluukkai/easn/网站。建模中的一个特别有趣的点是使用动态进程创建和动态cre的传递通道标识符80M. Luukkainen等人理论计算机科学电子笔记118（2005）71这两个特性同时受到Spin和Escort的支持。 在这方面，该模型不同于[6]，[3]中报告的前两个模型，其使用标记的转换系统规范和静态结构，其中相同的RLC和MAC组件被重用于后续连接。 这里的RLC协议的模型严格遵循标准中定义的模型，因为实际上不同的MAC连接不共享逻辑信道。动态方面建模的实际方法如下：(i) 首先，创建三个进程：oracle、发送用户和接收用户。(ii) 在开始RLC连接之前，oracle创建一个MAC实体。(iii) MAC实体定义四个本地通信信道，两个用于两个对等RLC，并将信道标识符传递给oracle。(iv) 然后，oracle将信道标识符传递给RRC实体，RRC实体然后开始RLC连接建立。(v) 然后，两个RRC实体都创建RLC实体，将对应的MAC信道标识符传递给所创建的进程。(vi) 在断开连接时，RLC实体和MAC实体都终止。在终止过程中，MAC和RLC之间的信道也消失了，因为这些信道是在对MAC进行建模的过程中本地定义的。(vii) 对于下一个RLC连接，Oracle重新开始。上述建模是可能的，这是由于Promela或Estrom建模语言动态创建进程并在进程之间传递通道标识符的能力。从验证的角度来看，被终止的协议实例对系统的当前状态组件没有任何影响也很重要。 实际上，如果终止发生在我们的模型中，则会发生这种情况，其中确保旧实体在新实体生成之前已经终止。待证明的性质和验证技术如果对协议的行为有任何影响，则在发送n个SDU的列表后，应该存在死锁的可能性，每个SDU仅由一个数字组成0.因此，如果我们能够证明该协议不会因任何可能的包含零的已发送SDU列表而死锁，则该协议在发送任何内容的SDU的一般情况下没有死锁消息重复的检测让我们假设当发送列表s1，s2，. ，s n，M. Luukkainen等人理论计算机科学电子笔记118（2005）7181−sdu = 0torlc！DataReq（sdu）fromrlc？DataAcksdu = 1torlc！DataReq（sdu）fromrlc？数据确认来自rlc？数据确认图五. 用于验证顺序递送的飞虎队因此，接收用户将被给予SDU s1，.是的，是的，是的，... s n. SDU的内容对协议的行为没有任何影响。因此，在发送SDU 0i-1 10n-i的列表的情况下（首先重复i-1次0，然后1，最后n i次1），由值1组成的SDU将被发送给接收用户两次。因此，如果我们能够表明，对于以0i 10j的形式发送的SDU的任何可能列表，协议恰好传递一个具有内容1的SDU，则当发送任何内容的SDU消息的按顺序传递让我们假设，当发送列表s1、s2、.时，协议可能改变传递第i个和第i + 1个SDU的顺序。，SDU的% s % n。因此，接收用户我们将在SDUs1， . . . ，si+1，si， . . sn. 因为我们的公司对协议的行为没有任何影响，在发送SDU 0i 1n−i的列表的情况下，由1组成的第一个SDU将在由0组成的最后一个SDU之前发送。因此，如果我们能够表明，对于形式为0i 1j的所有可能的已发送SDU列表，协议在由1组成的任何SDUs之前递送由0组成的所有SDU，则SDUs以与发送任何内容的SDU的一般情况相同的顺序被接收。验证本身是通过对RRC发送方实体进行建模来进行的，其发送所需类型的SDU，然后在RRC接收方中，我们检查接收到的SDU流是否为正确类型。作为示例，图5中示出了用于顺序递送验证的RRC发送器的一部分。因此，它首先发送内容为0的SDU，然后在某个时间点不确定地开始发送内容为1的SDU。以这种方式，可达性图将包含执行，其中考虑类型0i 1j的每个SDU列表验证结果我们成功地验证了所有感兴趣的属性，并为最大重传次数提供了几个不同的值下表总结了在验证RLC协议的等效模型时，对Escort和Spin进行验证的一些性能测量列出的措施是DFS搜索的深度，状态向量的大小（字节），状态和转换的数量，内存的使用（兆字节）和时间。对各种验证选项的结果单独报告，82M. Luukkainen等人理论计算机科学电子笔记118（2005）71（参见[4]，以了解各种选项的更具体描述）：• nodreduce，意味着存储状态向量大小的默认优化被关闭，• Bitstate，Holzmann• Collapse，Wolper表1死锁检测选项深度状态矢量大小存储状态状态匹配过渡总Mem.（MB）时间（实际）（m：s）工具NoReduce3307521160421934073094498.5150：6.666伊森330715211604219340730944910.8700：2.065自旋1646525492838812937405.2150：2.115伊森16461525492838812937406.2390：0.663自旋NoReduce330701156011925083081091.1290：4.383伊森BitState33111521157471928003085471.1290：1.420自旋BitState163805480538703935081.8130：1.446伊森15381525470938555932641.8130：0.476自旋崩溃1646285492838812937404.703一分五十四点七八一伊森16841525519538876940715.3180：0.920自旋NoReduce3307281160421934073094497.695七分三十四点三八七伊森崩溃33451521163271935173098449.1290：2.917自旋从表中可以看出，Etrance使用的内存量最多与Spin相同，但随着验证模型的大小增加，Etrance在内存使用方面的表现越来越好。我们已经注意到，与Spin相比，Escort的内存性能提高了20%以上它必须付出的代价是运行时间的增加在从Spin中制作Escort的过程中，Spin源代码中与状态编码及其管理有关的某些部分已经完全为Escort重新编写，从而可以看到其性能的改进这种方法是有意识地选择的，而不是简单地将ASN.1类型转换为适当的Promela类型。事实上，这个新的代码组件并没有在ESTO中发展，或者说，只要它从Spin中替换到ESTO中的代码，就可以在它的运行时中（相当清楚地）显示出来。通过使用GNU Multi-Precision ArithmeticPackage，EQUIPMENT使用整数算术来计算对应于系统到达状态另一方面，M. Luukkainen等人理论计算机科学电子笔记118（2005）7183表2消息重复选项深度状态矢量大小存储状态状态匹配过渡总Mem.（MB）时间（实际）（m：s）工具NoReduce12315230131464931295062619.67716.673分伊森123115630131464931295062626.7420：5.849自旋673526116436835979995.5220：2.225伊森6731566116436835979996.9560：0.736自旋NoReduce123102990236440799431021.1290：10.693伊森BitState12311562980216422659402861.1290：3.777自旋BitState67306113636828979641.8130：1.517伊森6731566100236731977331.8130：0.492自旋崩溃673286116436835979994.908二：七千八百八十伊森6731566238037016993965.830 0：0.956自旋NoReduce12312830131464931295062617.424六十一比二点一一七伊森崩溃123115630253064949395202322.4410：8.552自旋表3按顺序传递消息选项深度状态Vec尺寸存储状态状态匹配过渡总Mem.（MB）时间（实）（m：s）工具NoReduce12325224259652911477171016.0920：13.773伊森123215624259652911477171021.9290：4.648自旋674524802228983770054.7030：1.741伊森6741564802228983770055.8300：0.536自旋NoReduce125802411635257977669601.1290：8.868伊森BitState12321562360525154557515071.1290：2.985自旋BitState67404800528975769801.8130：1.208伊森6741564796928955769241.8130：0.395自旋崩溃674284802228983770054.294一分十九点二三八伊森6741564891829117780354.9080.759自旋NoReduce12322824259652911477171014.352三十六：五十六点三五七伊森崩溃123215624349252924877274018.3450：6.868自旋手，采用多项式算术为同样的目的。虽然Polynomial算法可能比多精度整数算法更快，但后者允许Etnion递增地计算散列值。在所附的表中，84M. Luukkainen等人理论计算机科学电子笔记118（2005）71注意ESTO报告0字节的状态向量大小，因为位状态运行与Spin报告的非零值相反。对于这些运行，Spin首先在连续字节数组中表示系统的到达状态，然后基于此将两个整数索引计算到位数组中，M. Luukkainen等人理论计算机科学电子笔记118（2005）7185在每个到达状态的两个索引处设置位。通过其使用，增量计算的两个指标（从那些对应的状态，该系统是在演变到其当前状态之前），不需要表示所达到的状态显式。有关各种设计决策及其基本原理以及相关的ECOMM实现方面的完整讨论，请参阅[7尽管这个RLC案例研究并不是一个大的案例，但我们已经观察到，ESTO简化了大型电信协议或系统的正式规范，因为它涉及一个（手动翻译）步骤（与使用Spin时相比），必须通过使用Promela类型对ASN. 1数据进行建模。“N-version” Programming: SPIN and EASN由于ESTO的代码库源自Spin系统，状态向量表示和处理（模型检查器的重要和关键部分）发生了变化，状态数量存在任何差异等。在这两个系统中，可以探索，以确定根本原因。这样的一个实验揭示了在这里提出的RLC模型下，自旋系统中的下列异常。• 当使用会合通道时，在搜索期间向后移动时压缩掩码没有完全恢复搜索的正确性并没有受到影响，但是到达的状态的数量变得比必要的这在Spin 3.4.6（2001年3月29日）中得到了修正。• 在s-hash函数中，计算出的hash值也会错误地检查多达3个无关字节的状态向量参数。这有时导致了对一些国家的重新探索。5结论在这篇文章中，UMTS无线电链路控制协议[9]的验证已经被考虑。该协议实现了几种操作模式。就验证而言，我们选择确认模式下的可靠数据传输服务。该协议使用Spin和我们的基于Spin [4]的电信系统模型检查器ESTO [7]进行建模和验证。在ESTO中，协议的数据方面使用ASN.1 [5]建模，而控制结构与Promela（Spin的输入语言）相同。 为了比较Escort与Spin的性能，我们在两个系统中进行了验证。从验证中获得的数据表明，随着运行时间的增加，Etrance可以使用比Spin更少的内存进行管理86M. Luukkainen等人理论计算机科学电子笔记118（2005）71更复杂的数据类型和数据结构导致了它的运行时间增加。我们已经在[6]中报告了RLC协议某些方面的验证，其中我们验证了协议的简化版本，其中不考虑断开阶段。在早期的工作中，我们使用标记的过渡系统的协议建模。在这个框架中，动态创建这里使用的流程并不容易，所以尽管我们早期的模型缺少断开连接阶段，但它比我们在这里开发的模型稍微复杂一些。此外，建模的动态方面更紧密地描述了引用[1] E.M. Clarke和E.A.爱默生基于分支时间时序逻辑的同步子设计与综合。在程序逻辑研讨会上，计算机科学讲义第131号。Springer-Verlag，1981.[2] E.M. Clarke，E.A. Emerson，and A.P. Sistla.使用时序逻辑规范的有限状态并发系统的自动验证。ACMTransactions on Programming Languages and Systems，第8卷，第244-263页[3] J. 他和S。 Leppéan en.ExplorationTesting.In1stInternationnalConfereceonApplication ofConcurrency to System Design，2001。[4] G.J. Holzmann Spin模型检查器。IEEE软件工程学报，23（5）：279[5] 国际电联/标准化组织。 信息技术----抽象符号1（ASN.1），1994年。[6] S. Leppéan enn and dM. Luuk kainenn. 第三代通用移动通信协议的复杂性。第一届分布式系统验证与验证国际研讨会，2000年。[7] V.K. Shanbhag和K.戈皮纳特 一种基于Spin的电信协议. 2001年第八届国际SPIN软件模型检测研讨会[8] V.K. Shanbhag，K. Gopinath，M. Turunen，A. Ahtiainen和M. 卢克凯宁 集成ASN.1和模型检查。在第13届计算机辅助验证研讨会论文集，计算机科学讲义Springer-Verlag，2001.[9] 第三代合作伙伴计划。RLC协议规范，技术规范3G TS 25.322 V3.2.0，2000。[10] W.托马斯无限对象上的自动机。在J. van Leeuwen，编辑，Handbook of Theoretical ComputerScience，Volume B，Formal Models and Semantics，第133爱思唯尔，1990年。[11] http://www.umts-forum.org网站， 2001年[12] Z. Manna和A.普努埃利反应和并发系统的时序逻辑，规范。Springer-Verlag，1991.