消息序列图在通信协议的规范和自动验证背景下的应用及特性

51理论计算机科学电子笔记65 No.7（2002）URL：http://www.elsevier.nl/locate/entcs/volume 65. html14页s使用消息序列图的多伦·佩莱德德克萨斯大学电气与计算机工程系Austin，TX 78712，USA摘要消息序列图是协议设计者和系统工程师在实践中使用的一种符号。在这次调查中，一些最近的结果与此符号，在通信协议的规范和自动验证的背景下，提出。1介绍软件系统的行为是工程师们的主要兴趣。当涉及到并发时，事情变得更具挑战性。即使在考虑用于规范的实际符号之前，执行模型也有很大的选择。不同的模型在它们所携带的详细信息、它们所提供的直观性以及检查建模系统的属性的难度方面有所在选择了模型之后，我们仍然有很多符号可供选择也许最成功的模型是状态机。该模型具有几个理想的特性。交错执行只是状态机图中的一个序列或路径。线性结构很容易处理。简单的形式主义，如线性时序逻辑是可用的。在有限的情况下，有简单的决策程序来检查这些模型的属性。消息序列图（MSC）是一种基于偏序的标准[6]形式主义。它有一个可视化的符号，清楚地展示了所涉及的并发进程之间的交互。它已经被协议设计者在实践中使用，这一事实使它在技术转移中比其他形式主义更有优势另一方面，使用现有的标准，这是由一个1电子邮件：doron@ece.utexas.edu2002年由ElsevierScienceB出版。 诉操作访问根据C CB Y-NC-N D许可证进行。PELED52联系我们⊆×- MSC;inst P1：进程根，P2：进程根，P3：进程根;实例P1;out M1 to P2;in M5 from P2;in M6 from P3;endinstance;instance P2;in M1 from P1;out M2 to P3;out M3 to P3;in M4 from P3;out M5 to P1;endinstance;instance P3;in M2 from P2;in M3 from P2;out M4 to P2;out M6 to P1;endinstance;endinstance;Fig. 1. MSC的可视化和文本表示委员会，没有算法和复杂性问题的全面视图，可以是挑战性的，另一方面，限制性的。在这篇综述中，我们讨论了使用消息序列图进行规范和验证的几个问题。2预赛每个MSC描述一个场景，其中一些进程相互通信.这样的场景包括对发送的消息、接收的消息、本地事件以及它们之间的顺序的描述。在MSC的视觉描述中，每个进程被表示为垂直线，而消息由从发送进程到接收进程的水平或倾斜箭头表示，如图1的左部分所示MSC的相应文本表示出现在图1的右侧。定义2.1MSCM被给出为元组M，其中• V是一组有限的事件，• 1，MiJ=MiJMi。(Thus，如果i j， MiJ≤Mj（J.）−1设MiJ=<$V i，#bσ1，其中#cσ是词σ中出现的cs的个数。(iii) 如果a和b属于不同的进程，并且它们的类型不像前面的情况那样匹配，那么我们可以用b置换a。(In事实上，我们也可以用a置换b，从这个条件的对称性第一规则的反向排列可以允许接收出现在对应的发送之前。例如，给定图5中MSC的线性化abab，我们不能将第一个a与第一个b置换以获得baab。第二条规则规定了允许反向置换的条件。在这个规则下，相邻的a和b，可以置换，不是一个匹配对。还要注意，对于MSC，不可能像迹理论[9]那样在事件之间使用固定的独立关系。我们可以如下定义HMSC的语言(i) 设L（M）是HMSC节点M的有限语言。(ii) 设为HMSC图形的语言，其中图形中的每个节点都被分配了一些唯一的字母（与字母不相交）。根据Kleene的构造，K语言是正则语言。PELED58→KKK≥≥一BCDP3P2P1见图6。具有上下文无关行为S1P1：sndt1P2：sndP1：snds2S3P1：rcvP2：rcvt2P1和P2见图7。一个简单的两进程协议(iii) 在K中，将对应于节点M的每个字母替换为L（M）。 这仍然是一种规范的语言。 我们得到一种语言K。(iv) 现在，在排列规则下关闭以获得[]。这种置换是通过使用XabY形式XbaY。因此，HMSC的语言是上下文敏感的。注意我们仅根据给定的第一和第三排列规则排列事件以上由于我们对每个单独的MSC节点进行了所有我们看到HMSC语言可以从正则语言（无限执行情况下的ω-正则）通过在给定的排列集合下闭合而获得为了说明HMSC的语言通常不是正则的或上下文无关的，请考虑图6中的示例。这个例子的全局状态有l次a事件、m次c事件和n次d事件，其中lMn（b个事件的数目也与c个事件的数目相同或比c个事件的数目大正好1）。这可以很容易地证明不属于上下文无关（因此也不是正则）语言。我们看到，HMSC可以表示一种不一定是规则的语言，事实上，甚至不是上下文无关的。另一方面，标准的MSC图符号不允许表示有限状态通信协议的所有可能的通信骨架。这使得HMSC无法与常规语言相比。作为一个例子，考虑从简单的PELED59P1P2e1G1e2f1h1g2e3f2h2g3e4f3见图8。不能分解图7中的协议。图8中显示了该协议的（唯一和无限）执行的MSC描述的有限前缀。我们表明，这个无限MSC不能分解成一个串联的有限MSC。 我们从发送事件e1和接收事件f1开始。很明显，由于强制匹配在HMSC中，它们必须属于同一MSC节点。我们有发送事件g1在F1之前，在相同的处理线上，而其相应的接收事件H1在发送事件E1之后。因此，事件g1和h1必须与e1和f1在同一个HMSC节点中。由于同样的原因，我们有，e2和f2必须属于同一个节点，与g1，和h1，等等。问题在于MSC节点包含匹配消息的限制。表达性问题的不同观点是，对应于HMSC中的有限路径的任何全局状态（即，包含完整MSC节点的全局状态）具有一组匹配的发送和接收事件。在图8中的偏序执行中，不存在具有此属性的全局状态因此，我们不能将此执行分解为有限的MSC（这将沿着HMSC的某个路径发生无限HMSC符号的扩展在[4]中描述。它允许MSC节点具有不匹配的发送和接收事件。因此，一个节点中的发送事件可以与稍后节点中的接收4HMSC模型检测的不可判定版本一旦我们将HMSC语言描述为上下文敏感的语言，那么某些决策问题变得不可决策就不足为奇了。特别是，它是已知的两个上下文敏感的语言的交集的空是不可判定的。对于HMSC语言，我们仍然需要证明，因为它们形成了一个子集，PELED60对上下文敏感的语言。出于实际动机，考虑常见的模型检查方法，其中我们使用用于建模系统的形式主义来描述错误的执行序列（通常是无限词上的有限自动机）[5，7，14]。执行的交集包含被检查系统允许的错误序列，需要报告。我们可以尝试沿着这些路线，使用HMSC形式主义来指定系统的坏的或不想要的执行。如果两个HMSC的线性化的交叉是非空的，我们可以很容易地取一个并生成回MSC。相交两个HMSC是不可判定的，如我们下面所示[11]：定理4.1两个HMSC的交问题是不可判定的。证据 后对应问题（Post Correspondence Problem，PCP）PCP的输入是一个有限的词（w1，v1），（w2，v2），.，（w n，v n）问题是要决定是否有一个有限的序列索引i1，i2，. ，我这样w i1 w i2... w im = v i1 v i2. V im.我们构建了两个HMSCs。一个用于连接出现在上述对的左侧组件中的单词，另一个用于连接出现在右侧组件中的单词。考虑左侧组件的HMSC。我们有4个进程P1，... P 4. 对于每个单词wj，我们构造MSC节点Mj，其中从P1到P2的消息由字母wj标记。我们有一个节点Rj，一条消息，从P3到P4，用索引j标记。我们也有一个初始节点E，消息从P1到P4，还有一个节点F，消息从P4到P1。自动机的结构可以由正则表达式E（+j= 1.表示。nMjRj）+F，这也在图9中展示。用于连接正确组件的自动机的构造类似。现在请注意，Mj分量中的事件可以与Rj分量中的事件交换，因为它们涉及不相交的过程。因此，交集中的任何词根据Mjs的序列具有相同的字符，并且根据Rjs的序列具有相同的索引。提供模型检查的另一种尝试是使用有限或无限词上的自动机或使用线性时态逻辑（LTL）来编写规范（或规范的否定，描述错误的执行）不幸的是，HMSC语言与正则语言或满足线性时态逻辑公式的词的语言的交集也是不可判定的。要看到这一点，在前面的证明中，用一个LTL（或正则表达式，或无限词上的有限状态自动机）替换右子词的HMSC，即对于MSC节点M，令lin（M）是M的单个线性化，其包括出现在相邻处的匹配发送和接收事件。(Note这种线性化对于MSC并不总是可能的，参见例如，图8. 但在我们的例子中是可能的，因为在约简中节点的特定构造。）因此，表示字wj=αββα的Mj的线性化将PELED61.........P4P1P1 P4......这是什么？...见图9。PCP减少是sα rα sβ rβ sβ rβ sα rα，其中sρ表示由ρ标记的消息的发送方，并且rρ表示该消息的接收者 LTL公式将表示语言lin（E）（+j= 1. nlin（Mj）lin（Rj））+lin（F）（这是一种无计数器的语言，因此可以使用LTL表示）。HMSC（的语言）的交集，代表PCP问题中的左边单词，和上面的LTL公式的语言，代表右边单词，将准确地包括PCP问题的解决方案的单词因此，HMSC的LTL模型检测是不可判定的。5HMSC模型检测的可判定版本有几个积极的解决方案，为HMSC提供模型检测算法。限制MSC。一种可能性是将消息队列限制为某个固定大小。在这种情况下，HMSC成为有限状态系统，通常的模型检测方法可以使用。另一个约束如下[3，10]：MSCM的通信图包含作为节点的进程，并且P1M1αβP2P3R11P4P1M2βααP2P3P42R2PELED62LL·UL/L/¬ ¬LL如果在M中存在从Pi到Pj的通信，则从Pi到Pj的边缘。M有界连通，如果它的连通图有强连通分支。如果我们要求HMSC中的每个循环具有有界通信，则上述模型检查方法变得可判定。在这种情况下，HMSC语言是常规的。这个结果也与跟踪语言中的星形问题有关[12]。检查有界通信在HMSC的大小上是NP困难的[10]。在规范HMSC的语义中允许“间隙”。表示错误执行的HMSC的解释方式与表示系统的HMSC不同。前者只是事件的一部分具体地，规范HMSC的同一过程线上的两个相邻事件a和b可以匹配系统HMSC中的相同类型的一些不相邻事件这两个HMSC之间的模式匹配问题是可判定的，并且在HMSC的大小中是NP难的[11]。使用基于偏序的规格说明形式。考虑一个具有语言的规范它是正则的，并且在置换规则可以确定这种规范与HMSC语言的交集的空性原因是HMSC语言[P]是通过在置换下关闭正则语言P而生成的如果[]=，则P=当且仅当[P]=。因此，它足以检查的空虚，交叉口使用HMSC语言的常规生成器P涉及基于偏序的形式主义的解决方案是使用逻辑TLC [2]的子集，如[13]中应用于HMSC的那样。根据这个解决方案，我们使用时间模态的原因在MSC系统的事件我们使用与LTL中相同的模态符号，但给予它们不同的解释;在由关系生成的事件路径上，而不是在偏序的线性化上。<因此，断言对于在关系下有直接后继者的事件是成立的。<对于事件e，有一条路径从事件e出发，通向某个事件f，事件f对事件e成立，事件f对事件f成立（因此，e<∈f）。类似地，为了使对e成立，我们要求对沿着从e到某个事件f的路径的每个事件成立，其中成立。最后，为了满足通常的对偶性，我们解释如下：对于事件e满足，对于每个事件f使得e<∈f，f成立。另一种可判定的模型检测方法是基于二阶偏序上的一元逻辑[8]。6其他决策问题MSC出现的一个自然问题是MSC是否包含竞争条件。竞态条件可能是由于我们对至少包括一个接收事件的事件对之间的顺序只有有限的控制（除了根据FIFO语义，对应于从同一进程发送的消息的两个接收）。例如，图1中的MSC包含两个接收PELED63∈进程P1（消息M5和M6）的事件。由于每个过程线都是一维的，因此MSC标记法强制选择一个接收事件出现在另一个接收事件之上。然而，这两个消息是从不同的进程P2和P3发送的，可能会发生M6比M5更快到达的情况。因此，没有理由相信这些消息将以使用MSC描述的特定顺序到达。形式上，我们可以为MSC接收事件p，q对定义竞争条件V表示从不同进程发送的消息，使得L（p）=L（q），即，p和q出现在同一生产线上。如果p q，即，在生产线上，p出现在q的<上方，并且p不等于q，即，根据关系式，没有从p到q的路径。因此，在MSC中检测种族是简单的。我们所需要做的就是计算传递闭包，并将其与关系进行比较。文[1]指出，传递闭包的计算是事件数的二次型，而不是一般情况下的三次型

下载后可阅读完整内容，剩余1页未读，立即下载