理论计算机科学电子笔记255（2009）159-176www.elsevier.com/locate/entcs通过翻译成FSP来分析Chor规范Nima Roohi1谢里夫理工伊朗德黑兰GwenSalauên2马拉加大学计算机科学系马拉加Seyyed Hassan Mirian3谢里夫理工伊朗德黑兰摘要编排从全局的角度指定一组服务之间的活动和交互。 从这个规范中，可以自动生成本地实现或对等点。生成精确实现编排规范的对等点并不总是可能的：这个问题被称为可实现性。本文提出了一种编码的Chor编排演算到FSP进程代数。这种编码允许：（i）使用FSP工具箱（LTSA）验证和验证Chor规范(ii)从Chor中指定的编排生成对等协议，（iii）测试Chor规范的可实现性，以及（iv）从FSP生成Java代码以用于快速原型设计。我们的建议是支持和完全自动化的原型工具，我们已经实现。关键词：编舞，WS-CDL，Chor，FSP1引言编排描述语言的目的是从全局的角度来指定新应用中涉及的一组服务之间的几种形式1电子邮件地址：roohi@ce.sharif.edu2电子邮件：salaun@lcc.uma.es3电子邮件地址：hmirian@sina.sharif.edu1571-0661© 2009 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2009.10.030160N. Roohi等人/理论计算机科学电子笔记255（2009）159已经有人提出来指定编排：WS-CDL、协作图、BPMN、SRML等。从这些规范中，可以自动生成本地实现，即对等体。然而，生成精确实现编排规范的对等体并不总是可能的：这个问题被称为可实现性。最近关于这个主题的工作[7，12，4，2]提倡检查可实现性的技术 或者定义在编写编排规范时要应用的格式良好的规则，以确保其可实现性。然而，这些方法大多集中在理论方面，缺乏工具支持。此外，这些工作主要集中在可实现性问题上，但不允许检查编排（以验证组合的总体目标是否实现）或从这些规范生成代码。在本文中，我们使用Chor演算[12]作为编排语言，因为它是WS-CDL的一个抽象模型，具有正式的语法和语义（而不是WS-CDL的例子）。我们提出了一种从Chor到FSP进程代数的编码[9]。我们选择FSP是因为它依赖于一种简单的语言，但表达能力足以编码Chor运算符。此外，FSP还配备了LTSA工具箱，为状态空间探索和验证提供了有效的工具。这种编码允许：（i）使用LTSA工具箱验证和验证Chor规范，（ii）从Chor中指定的编排生成对等协议，（iii）测试Chor规范的可实现性，以及（iv）从FSP生成Java代码以用于快速原型设计。我们的建议是支持和完全自动化的原型工具，我们已经实现。本文的其余部分组织如下：第2节介绍Chor和FSP结石。第3节介绍了Chor到FSP的编码。 第4节扩展了FSP编码，将节点生成考虑在内，并重点讨论了可实现性问题。第5节概述了支持我们的方法和Java代码生成的原型工具。第6节将我们的建议与相关的工作进行了比较，第7节以一些结论结束了本文2歌手：Chor and FSP2.1ChorChor [12]是一种简单的过程语言，也是WS-CDL的简化模型，用于从全局角度描述对等点。从这个全局规范中，可以通过投影生成对等体的虚拟规范。在本节中，我们将概述[12]中介绍的Chor语言（全局视图）和Peer语言（局部视图）。首先，让我们定义本文中使用的跟踪运算符。定义2.1本文中使用的迹运算符定义如下（t，t1和t2是任意迹，T，T1和T2是任意迹集，S是动作集，R是Action→Action类型的部分函数4，并且domR代表一般来说，R可以是一个部分关系，但我们只在它是一个部分一对一函数时使用它。N. Roohi等人/理论计算机科学电子笔记255（2009）159161^12⎪⎩\.⟨⟩.关于我们^12==^^t1i=如果t = t，则t=t/R我的天⎧⎪{t1}ift2=⟨⟩∧⎪22t1，t0{}其他2t仅限于S：t由S：t0我不知道-我不知道t1与T2相关：t的闭合：T的闭合：{t2} ift1 = 0⎪0J00⎪^111112对于R的域：#t：tt0：t的头（t的第一个动作）tJ：t的尾部（从t去除头部得到的迹线）t[i] ：i-t的第i个元素（0≤i#t）s（t）：t（{t [i]）中的动作集合|（0 ≤ i <#t}）t1与t2（长度为#t1+#t2的跟踪）：t重命名为R：.[]如果联系我们0Jt/R如果t=0，12t2[i−#t1]else^⎪⎩ R（t0）∈/domRt1与t2交错：t1与S上的t2同步：s（t1）S=⎧⎪{t1}ift2=⟨⟩s（t2）S=公司简介1{t2}if t1={t j d}{t j d}{tJd}|atJ） if t0= t0t da t=⎪⎩t0-（tJda t2）elset1d|at2=^1 20∈St0-（t1DatJ）S⎪22t1-（t1D|at2）如果t1= t2<$St0-（t1D|（J）t0∈/S0∈/S如果t= 0，则tj如果t= 0，则tjtfSfSift⎩⟨⟩∧t∈/St\S=^t Sift⎩⟨⟩ ∧t ∈St（i）如果i= 0^t-t（i−1）elseT（i）如果i= 0T-T（i−1）elseT重命名为R：T限制为S：T过滤为S：T/R={t/R|t∈T}TfS=^{tfS|T\S=^{t\S|t∈T}t-T={t1}-T2t^i≥0t（i）T^i≥0T（i）T1与T2连接：T1-T2={t|t1∈T1 t = t1-t2}T1与T2交错：T1Da T2={t|t1∈T1 t ∈ t1da t2}T1与S上的T2同步：ST1D|在2S^{t|t1∈ T1 t ∈ t1d|在2}表1显示了Chor的语法和语义（C、C1和C2是任意Chor规范）。它使用弱迹（隐藏τ操作）来指定其===（=-t）i#t1tconcatenatedi times with itself：Tconcatenatedi times with itself：不^162N. Roohi等人/理论计算机科学电子笔记255（2009）159因此，R−1也是一个部分函数，可以用于定义的运算符。N. Roohi等人/理论计算机科学电子笔记255（2009）159163∗关于我们关于我们关于我们∈†⇒⇒^ ^您的位置：skip/^α = α /αJ =.如果 α =αJ，^ ^您的位置：语义（其中[C]代表C的弱迹集）。对语言的更多细节感兴趣的读者可以参考[12]。表1Chor的语义skip意味着什么都不做，它的跟踪集等于ai是对等点i执行的任意本地活动，其跟踪集为aic[i，j]是两个对等点i（发送者）和j（接收者）之间通过信道c进行的通信，其迹集为c[i，j]C1;C2表示先C1，然后C2，[[C1;C2]]=[[C1]]-[[C2]]C1HC2表示C1或C2，[[C1HC2]]=[[C1]]=[[C2]]C1<$C2 表示C1和C2同时运行，[C1<$C2]]=[[C1]]Da[[C2]]C表示执行C任意次数，[C]] =[[C]]循环操作符““在其他操作符中具有最高的优先级。在此之后，顺序组合运算符“;”的优先级高于其他运算符，例如，“C1HC2;C3”不是二义性的。并行优先“||“和选择“H”运算符相等，例如，C1<$$>C2HC3=（C1<$（<$C2））HC3（左结合性）。Chor是通过一组独立的进程的协调来实现的 Peer语言是描述这些过程的简单演算。在这种语言中，是一个empty过程，其中h意味着什么都不做，对于任意迹t，如果P=我们有t[[P]（我们用来表示死锁）。 表2给出了Peer语言的语法和语义。在表2中，P、P1和P2是对等规范。Peer语言与Chor语言的主要区别在于对交互的描述。Peer从本地的角度对它们进行具体化。因此，在对等体级别，交互活动是发射或接收，并且对等体通过握手通信（相同的信道，相反的方向）进行交互使用表2中定义的规则，如下获得对等进程的跟踪集P−σ→PJP=σPJP−σ→PJPJ=σJPσ=-σJPJJPJJ最后，operator/：Peer×Activity→Peer返回af-在执行输入活动之后，函数fst（first的缩写）：Peer→P（Activity），其中P（Activity）是所有可能活动的幂集，计算Peer进程中可以首先执行的活动。操作符“/“和函数fst的正式定义fst（跳）= fst（跳）= fst（P1H P2）= fst（跳P）=跳fst（α）={α}fst（P1;P2）=fst（P1）fst（P1<$P2）=^fst（P1）<$fst（P2）如果α/=αJ，（P1;P2）/α=P.1/α;P2（P1HP2）/α=（P1 H P 2）/α=（P1H P2）/α=（P1<$P2）/α=^^P1/α<$P2若α∈fst（P1）P1<$P2/α，若α∈fst（P2）埃塞尔164N. Roohi等人/理论计算机科学电子笔记255（2009）1592−→12121表2Peer的语义P：：=||||BPP;P PHPP PCUP（基础）（顺序）（选择）（并行）（循环）BP：：=|||skipac！c？是的(no行动）（local）（send）（receive）Skip：skip−→ϵ当地人：aPizzaP1−σ→PJ−→π顺序：σ1;P −→PP1;P2 −→P1J;P2选择：P1HP2−→ P1P1HP2−→ P2第二节：−→P1−σ→PJϵc！∈fst（P1）c？∈fst（P2）P1<$P2−σ→PJ<$P2阿利什卡σ1P1<$P2−→P1/c！P2/c？P2−→P2JP1<$P2−σ→P1<$PJc？是的∈fst（P1）c！∈fst（P2）PP cP /C？PutP/c！Lo op：P−→skipP−→磷，磷例2.2在本文中，我们将以金属股票市场为例。在我们的示例中有三个对等点。 首先，同行经纪人选择两种金属之一，即铁和钢，然后根据需要多次观察市场，直到所选金属的销售成为可能。 经纪人发送他/她的出价， 将选定的金属传递给我们示例中的第二个对等体（市场）。 接到 Market同时执行以下两个任务：将出价保存在自己的数据库中，并检查此出价是否优于当前最佳出价或不. 然后，市场将检查结果和经纪人名称发送给公告板（我们示例中的第三个对等体）。如果这个出价是迄今为止最好的，董事会将改变目前的赢家，并通知经纪人。否则，Board什么也不做（跳过）。在下面的Chor规范中，bk，bd，bd分别代表经纪人，市场和董事会：库存=（铁bkH钢bk）;看bk;看bk;出价[bk，];（保存||check（）;result[bd，bd];（changebd;notify[bd，bk] Hskip）2.2FSPFSP是一种进程演算，其灵感来自Milner FSP最初是为分布式软件体系结构规范而设计的，并区分了顺序过程和复合过程。表3介绍了本文其余部分使用的FSP运算符（x和y是动作，P和Q是FSP过程）。在下面的引理中，我们展示了FSP算子的迹集如何被表示为 表3中的引理可以计算（本文后面将使用该引理的N. Roohi等人/理论计算机科学电子笔记255（2009）159165|||\{···}···∪· ··∪αP1<$αP2···nD|一\\αP2<$αP3···nD|一αPn−1<$ αPnD|一[[P1···Pn]]=[[P1]][[P2]]···[[Pn]]表3FSP算子与非形式语义（x−>P）描述了一个进程，它首先执行动作x，然后表现为P。（P;Q）描述了一个过程，它首先表现为P，然后（在P的完备化）表现为Q。（x−>Py−>Q）描述了一个过程，要么执行动作x，然后P，或作用y，然后是Q。（P Q）表示P和Q的并发执行。这个操作者承担了P和Q的共同作用。x：P将P的字母表中的每个标签前缀为x。P/{新1/旧1，···，新n/旧n}重命名动作标签。P中的每个旧标签都被新标签替换。Px1，，xn删除动作名称x1，，xn从P的字母表并使这些动作“无声”。这些无声的动作被标记为τ。不同进程中的静默操作不共享。P@{x1，···，xn}隐藏了P的字母表中不属于集合{x1，·· ·，xn}。这些运算符的形式语义是使用LTS定义的，可以在[9]中找到引理2.3（FSP的迹集）每个FSP算子的迹如下获得，其中P，P1，···，Pn是FSP过程标识符，αP代表P的字母表，αPi···j代表αPiαPj，END是没有过渡和一个起始和最终状态的最简单的FSP过程：[[EN D]]={简体中文}[[P1; ···;Pn]]=[[P1]]-···-[[Pn]][[b a1−>P1| · · ·|b an−>Pn]]=（b a1-[[P1]]）···（b an-[[Pn]]）[[p1：P1···pn：Pn]]=[[P1]]/{（x，p1. x）的|x∈αP1}DA·· ·DA[[P.n]]/{（x，pn.x）|X.∈αPn}[[(P;结束）/R]]=[P]]/R[[（P;END）S]]=[P]]S[[(P;END）@S]]=[[P]]fS3将Chor翻译成FSP在本节中，我们将介绍我们的Chor编码到FSP中，它允许使用现有的工具支持FSP。因此，生成的FSP规范可以编译成LTS（标记转换系统），并使用LTSA（动画，LTL模型检查）进行检查。这种编码也将用于生成对等体和检查可实现性（参见第4节）。首先，活动skip隐藏在Chor轨迹中，因此我们使用τ进行编码跳过活动到FSP5。 Chor的每个本地或通信活动都被编码5可以首先从Chor规范中删除跳过活动，然后执行编码。 它也可以证明，对于每个Chor规范C，存在Chor规范CJ和CJJ，166N. Roohi等人/理论计算机科学电子笔记255（2009）159ǁǁ^^^H|联系我们=ac（C1;···;Cn）=ac（C1H···HCn）==c2 fp i（C1C2）=（z−>c2 fp i（C1）;ENDz−>c2 fp i（C2）;END）z.假设z既不在αc2fpi（C1）中，也不在αc2fpi（C2）中。∗∗|联系我们使用FSP流程，其中单个操作对应于该活动。Chor顺序运算符使用FSP顺序运算符进行编码。至于选择操作符，我们通过τ操作来前缀每个操作数，因此类似于Chor和Peer语言，选择操作数是非确定性执行例如，如果选择操作符的一个操作数中的第一个动作是c[i，j]，则c[i，j]也可能在另一个FSP过程的字母表中。我们将在第4节中看到，这些FSP进程可以使用FSP并行运算符（没有任何重命名）组合。选择操作数的选择必须以独立的方式执行。因此，如果一个FSP进程选择以c[i，j]作为动作执行操作数，而另一个进程不执行，则可能发生死锁。就并行运算符而言，平移更为复杂。在FSP中，两个操作数的字母表中的动作只能通过同步来进化，但Chor的并行操作符不同步活动其操作数（交织）。因此，我们首先用一个唯一的值（例如，，p1：P1p2：P2而不是P1P2），因此不发生同步。然后，我们使用FSP的重命名操作符将这些新的动作名称替换为它们的原始值。为了在编码并行运算符时执行最终重命名，我们需要为每个操作数找出所有非跳过的基本活动。这些活动是使用定义3.1计算的。定义3.1[包含的基本活动]我们定义ac，Chor类型的函数→P（活动），如下所示：ac（skip）= {}ac（ai）={ai} c[i，j]=0{c[i，j]}ac（C1· ·Cn）=^ac（C1）··ac（Cn）循环运算符（C）在FSP中使用非确定性选择来指定在执行skip或执行C然后递归调用FSP之间，对循环运算符进行编码的过程定义3.2[Chor到FSP]使用函数c2f：Chor→FSP描述实现将Chor规范C编码到FSP中，如下所示：c2 f（s ki p）=SKIP=（s ki p−>END）\{s ki p}.c2f（ai）c2f（c[i，j]）1c2 fp i（ai）=（ai−>END）。=^c2 fp i（c[i，j]）=（cij−>END）.（C;C）=c2f（C）;C21 2c2f（CH）=π1 2Pi1Pi2c2f（C1<$C2）^不好意思。c2fpi（C1<$C2）= （p 1：c2fpi（C1）p 2：c2fpi（C2））。c2fpi（C1 <$C2）= T. c2fpi（C1<$C2）;SKIP;END/{ba1/p 1.ba1|ba1∈ ac（C1）}<${ba2/p 2.ba2|ba2∈ ac（C2）}.c2f（C）^c2 fp i（C）=（z−>SKIP;ENDz−>c2 fp i（C）;SKIP;c2 fp i（C）） z.假设z不在αc2fpi（C）中。我们在每个顺序组合的操作数之间添加了SKIP，因为其中[C]]=[[CJ]且CJ= skip，CJ= skip H CJJ，或CJ= CJJ（CJJ在其规范中没有skip）。=c2f（C;C）=c2fN. Roohi等人/理论计算机科学电子笔记255（2009）159167{|∈}{|{|∈}{|∈}规则P−P→P 表2中的P。我们也把z−>SKIP;END而不是z−>END因为规则是： skip和skip−→ 塞林那张桌子。这些规则中的每一个都有一个−→ 转换，我们使用额外的SKIP过程。这些附加的SKIP过程对于在将对等体编码到FSP中时保持对等体的语义是有用的（参见定理4.5）。FSP不允许动作有下标或上标。因此，我们将ai和c[i，j]分别转化为a i和c ij。c2fpi是Chor~ProcessIdentifier类型的一对一函数，生成新的标识符（对于相同的Chor规范，相同的标识符）作为输出，其遵守FSP进程标识符的命名规则6T.c2fpi返回一个进程标识符，该标识符是通过将c2fpi的结果用T进行前缀来获得的。对于所有C和CJ，使得c2f（C）在其规范中有一个过程标识符c2fpi（CJ），c2f（CJ）的结果必须包含在c2f（C）的结果中，因为每当我们在规范中使用一个FSP标识符时，我们必须在最终规范中包含该过程在下面的定理中，我们证明了Chor语义被定义的翻译所保持。由于Chor语义是使用弱迹集定义的，我们证明了我们的编码使用定理3.3保留了这种语言的语义。定理3.3（Chor和FSP之间的弱迹等价给定Chor规范C和相应的FSP过程c2fpi（C），两个规范是弱迹等价的：[[C]] =[[c2fpi（C）]]证据 我们利用引理2.3和C语言中关于算子结构的归纳法证明了这个定理。归纳法的基础（C=skip，C=ai，或C=c[i，j]）是空的。同样对于C等于C1;C2和C1HC2的情况，可以分别检查[c2fpi（C）]]等于[C1]]-[[C2]]和[[C1]]-[[C2]]当C=C1 → C2然后[T. c2fpi（C）]]=（[[c2fpi（C1）]]/R1）da（[[c2fpi（C2）]]/R2）和[c2fpi（C）]]=[[T. c2fpi（C）]]/R，其中R1、R2和R定义如下：R1= （x，p1.x）x αc2fpi（C1）R2= （x，p2.x）x αc2fpi（C2）R = （p1.ba1，ba1）ba1ac（C1）（p2.ba2，ba2）ba2 ac（C2）R将每个Activity重命名为其原始值（当R1或R2尚未应用）。由于操作符Da不对其操作数[c2fpi（C）]]=[[c2fpi（C1）]]Da[[c2fpi（C2）]]=[[C1]]Da[[C2]]=[[C]]。当C=<$CJ时，我们有[c2fpi（C）]] = [[SKIP]]<$[[c2fpi（CJ）]]-[[c2fpi（C）]]={\displaystyle{\cHFFFFFF}{\cHFFFFFF}{\3cH2F2F2F}{\4cH000000}}{\cHFFFFFF}{\3cH2F2F2F}{\4cH000000}{\4cH000000}}{\cHFFFFFF}{\3cH2F2F2F}{\4cH000000}{\4cH00000}{\4cH000000}{\4cH000000}{\4cH000000}{\cHFFFFFF}{\3cH2F2F2F2F}{\4cH0000000}{\4cH000000}}{\cHFFFFFF}{\3cH2F2F2F}{\4cH0000000}{我们可以看到，t ∈ [[c2fpi（C）]]。t∈ [[CJ]]-···-[[CJ]] = [[CJ]]（i），其中i≥0.所以，我们有[c2fpi（C）]<$[[CJ]]<$。对于相反的方向，通过对n的归纳，我们证明了对所有n≥0，[c2fpi（C）]=168N. Roohi等人/理论计算机科学电子笔记255（2009）1590≤i≤n[[CJ]]（i）[[CJ]]-[[c2fpi（C）]]。归 纳 的 基础是[c2fpi（C）]=[CJ]]（0）6这些规则在[ 9 ]附录B第2节中定义。N. Roohi等人/理论计算机科学电子笔记255（2009）159169∪ ⇒⊆Tau1 steel_bk保存_ 5检查_tau0look_bk2查看bk3bid_bk_46结果_bd_bd7tau11铁_bk检查_10保存_10Enotify_bd_bk9tau8change_bd[[CJ]]-[[c2fpi（C）]]={}[[CJ]]-[[c2fpi（C）]]，这是平凡的真理。 因此，作为─求和[c2fpi（C）]]=0≤i n [[CJ]]（i）<$[[CJ]]-[[c2fpi（C）]]，对所有n>0，我们证明了[[c2fpi（C）]]=0≤i≤n[[CJ]]（i）[[CJ]]-[[c2fpi（C）]]。把右手边在 [c2fpi （ C ） ] 定 义 中 的 前 件 ， 证 明 了 后 件 因 此 ， 我 们 有 ： [c2fpi（C）]]=[CJ]<$[[CJ]]-[[c2fpi（C）]] [[CJ]<$[[c2fpi（C）]]。因此，[CJ]]π和[c2fpi（C）]]都是彼此的子集，因此相等。Q示例3.4让我们用为我们的示例生成的一些FSP过程来说明我们的编码。在表4中，我们可以看到例如choice操作符是如何通过将choice的操作数前缀为z然后隐藏此操作来 非 确 定 性 地 执 行 的 图 1 显 示 了 通 过 使 用 LTSA 编 译 生 成 的 FSP 代 码 （ c2fpi（Stock））获得的最小化LTS。首先，经纪人决定他想要什么金属，铁或钢。然后，他根据需要多次查看市场，直到所选金属的销售变得可用（在状态上有一个循环 2在LTS中）。之后，他将他/她的出价发送到市场。接下来，Market保存价格并同时检查它（LTS中从状态4到状态6有两条不同的路径）。然后，市场将执行检查的结果发送给董事会。最后，Board要么什么都不做（如果结果显示出价不够好），要么改变自己并通知经纪人（如果结果显示出价是迄今为止最好的）。这个LTS使用LTSA动画技术运行了几次，系统的行为符合预期。这里不需要模型检查，因为为了便于理解，我们在本文中选择了一个简单的例子表4为运行示例生成的一些FSP进程Chor规范FSP过程规范skipSKIP =（skip−>END）\{skip}.铁bk铁bk =（铁bk−>END）。look bkLook bk =（look bk−>END）.bid[bk，]Bidbk =（bid bk −>END）.铁bkH钢bkCh =（z−>铁bk;结束|z−>Steel bk; END）\{z}.l oo kbkL=（z−>SKIP;END|z−>L ookbk;SKIP;L）\{z}.（铁bkH钢bk）;看bk S=Ch;跳过;看bk;结束。保存||支票支票||TP =（p1：检查||p2：保存）。P= TP; SKIP; END/{检查是否有错误/p1。检查表，保存/p2。save}。Fig. 1. 最小化股票市场的LTS案例研究170N. Roohi等人/理论计算机科学电子笔记255（2009）159^ǁ···ǁ4Peer生成和可实现性4.1对等体生成给定Chor规范，可以使用自然投影生成每个Peer的规范。一个Chor规范到PeerP的自然投影7用τi替换每个可观察的动作，而P不执行该动作。Chor和Peer共享并行、顺序、选择和循环运算符。对于这些算子，自然投影首先用其等价物替换每个Chor算子 在Peer中，然后递归地应用于它们的操作数。基本活动从Chor规范C到Peer规范P的预测实现如下：(i) 每个不是由P执行的活动都由跳过代替，(ii) 由P执行的局部活动保持不变，(iii) 涉及P的通信活动被通道输入活动替换(ifP是接收方）或通道输出活动（如果P是发送方）。任意Chor规范的FSP过程的生成使用第3节中定义的函数c2f执行。通过将所有动作隐藏在对应的FSP（c2fpi（C））中来生成编排C中的每个对等体P的行为。P不参与（定义4.1）。定义4.1给定Chor规范C和Peer标识符p，对应于nproj（C，p）的FSP过程，Chor规范C到Peerp的自然投影，如下所示生成（p2fpi的定义类似于c2fpi）：p2f（C，P）= p2fpi（C，p）= c2fpi（C）@{b|b是p的活性。如[12]中所述，为了将Chor投影到peers，每个Peer的名称都被作为每个活动名称的一部分（例如，这里我们将其添加为su_x）。因此，不同对等点的本地活动是成对不同的，并且对等点使用独占信道来彼此通信。 因此，每个通道仅跟踪两个对等体的活动。因此，我们认为， 在p2fpi（C，1）p2fpi（C，n）中，只有表示通信活动的动作彼此同步，并且这些动作中的每一个属于并行运算符的操作数的恰好两个FSP处理的字母表与第3节类似，为了证明我们的编码方法保留了Peer语言的语义，我们需要一些初步的定义和一个引理。而不是证明我们的编码方法保留跟踪语义，我们证明了编码的对等体的并行组成是强bisimilar的输入对等体的paral- lel组成，因为它是一个更强的结果，但更容易证明。FSP过程F的语义是使用LTS（lts（F）8）定义的，因此在下面的定义、引理和定理中，我们使用LTS而不是FSP（对于FSPs的定义，我们没有过渡关系（“-a →“）的定义[7]关于自然投射的正式定义，读者可以参考[12][8] FSP的LTS语义在[ 9 ]中定义。 在本文中，我们使用LTSA来计算不同的LTSFSP规格。N. Roohi等人/理论计算机科学电子笔记255（2009）159171†我们在互模拟关系定义中需要这个关系）。Peer和LTS之间的强互模拟关系定义如下：定义4.2[Peer和LTS之间的强互模拟关系（强互模拟关系）]我们设置互模拟lts（END）和互模拟lts（STOP）9。 对于任何其他对等体规范P和LTSL，当且仅当以下两个条件满足10时，我们才有PL：• B. P−→• B. L−→PJLJ. L−→bLJPJ. P−→bLJPjLJPJP jLJ只有当对等体与它们的互补活动并行时，它们之间的交流活动才能发生。例如，没有过渡关系，定义为C！， 但如果它是d和c的混合物呢？与此同时，我们将有一个VEC！什么？−→c。因此，为了将个体Peer指定的行为与其相应的FSP过程进行比较，我们需要另一个定义。定义4.3[Peer和LTS之间的相似行为（Similar Behavior（Eij）]我们将PeerP和LTSL之间的相似行为关系定义为EIJlts（END），<$EIJlts（STOP），对于既不是Eij也不是<$Eij的所有其他Peer，该关系定义如下：埃普湖PJL惠c（c） c！ ∈fst（P）<$L−→cLJ<$P/c！LJ）（c）c？是的∈cfst（P）<$L−→LJ <$P/c？LJ）（c） L−→aLj（c！ ∈fst（P）<$P/c！ V（c？ ∈fst（P）<$P/c？Lj））（J.P.J. P−→PjLJ. L−a→LJ<$PJ<$JLJ）<$（J.J. L−a→LjPJ. P−a→PJ<$PJ<$LJ）<$（<$P J.P − τ → P j LJ.L − τ → LJ<$PJ<$LJ ）<$（<$LJ. L − τ → Lj P J. P − τ → P j<$PJ<$JLJ）引理4.4对于每个Chor规范C和Peerp，我们有nproj（C，p）Jlts（p2fpi（C，p））.证据 为了便于理解，我们只证明了Peer p的行为可以由相应的LTS表示（反向的证明是类似的，因此很简单）。我们对nproj（C，p）的算子使用归纳法归纳法的基础（nproj（C，p）等于a，，ap，c[p，pJ]或c[pJ，p]的情况）是空的。接下来，我们证明以下归纳步骤：P=nproj（C，p）=P1;P 2C1C2 C = C1; C2 nproj（C1，p）=P1nproj（C2，p）= P2nproj（C1，p）Jlts（p2fpi（C1，p））nproj（C2，p）Jlts（p2fpi（C2，p））lts（p2fpi（C，p））=lts（p2fpi（C1，p））;lts（SKIP）;lts（p2fpi（C2，p））若P1=<$$>P−τ →P2<$lts（p2f（C1，p））<$lts（END）<$Pilts（p2fpi（C，p））{lts（SKIP）;lts（p2fpi（C2，p））}τBB172N. Roohi等人/理论计算机科学电子笔记255（2009）159PiJ.lts（p2f（C，p））−→ LJ <$LJ <$lts（p2fpi（C2，p））<$P J <$LJ.9lts（ST OP）有一个 初 始 状态，但不是最终状态，并且没有转换。10两个对等体之间或两个LTS之间的互模拟关系[9]是类似的和直接的，因此它们在这 里没有呈现。N. Roohi等人/理论计算机科学电子笔记255（2009）159173∧ ∼/ǁ···ǁ11111PiPiPiPiPiPiPi如果P1/=a，则aP− → P j LJ。 lts（p2f（C1，p））−a→LJ<$LJJP一J. lts（p2fpi（C1，p））; lts（SKIP）; lts（p2f（C2，p））−→ LjLJ<$LJ1;lts（SKIP）;lts（p2fpi（C2，p））<$PJ<$LJτ案件的证据C！∈fst（P），c？∈fst（P），或P−→PJ，且情形P=P1<$P2，P = P1HP2，或P = P1HP1是类似的，在此省略.Q定理4.5对于具有n个对等点的每个ChorC，PS=nproj（C，1）···对等点2 =对等点;跳过;结束。并且P2Peers =（p2fpi（C，1）P2.P2fpi（C，n））。证据 如果PS = n， 则 n ≤ i ≤ n。 lts（p2fpi（C，i））lts（END），因此一个ττ可以看到lts（p2 fpi（C，1）<$··<$p2f（C，n））<$lts（END）。 因此PS−→ε和L−→LJLJlts（结束）。 对于所有其他情况下，其中PS =无菌证明如下：F或所有P SJ都满足ch，P S−→b1≤i≤n。nproj（C，i）−→PSJ（b代表当地活动或τ）nproj（C，i）jBlts（p2f（C，i））−→lts（p2fpi（C，i））Jnproj（C，i）JJlts（p2fpi（C，i））JBb=τji. b∈αp2f（C，j）∈LJ. L−→LJ<$PSJ<$LJ（归纳）F或所有P SJ满足chP S−→cP SJ（c代表通信活动）n≤ i，j ≤ n。i/= jnproj（C，i）/c！=nproj（C，i）J<$nproj（C，j）/c？=nproj（C，j）jClts（p2f（C，i））−→lts（p2fpi（C，i））J<$nproj（C，i）J <$<$Jlts（p2fpi（C，i））J<$Clts（p2f（C，j））−→lts（p2fpi（C，j））J<$nproj（C，j）J <$$> Jlts（p2fpi（C，j））J<$C$ki，j。 c ∈ αp2f（C，k）∈ LJ. L −→ LJ<$PSJ<$LJ（归纳）反向的证明与正向的证明类似，因此省略了 这里.Q推论4.6互模拟是比（弱）迹等价更强的关系，因此对于具有n个对等体的每个Chor规范C，以下关系在对等体规范及其对应的FSP规范之间成立：[[nproj（C，1）··nproj（C，n）]] = [[p2fpi（C，1）··p2fpi（C，n）]]4.2实现性定义4.7正式定义了我们在本文中使用的编排可实现性的概念。为了实验的目的，我们选择了一个强可实现性[2，7]，但也可以使用弱概念[7]。定义4.7[Chor在自然投影下的可实现性]对于具有n个对等体的Chor规范C，我们说C在自然投影下是可实现的，当且仅当以下两个条件成立：(i)[C]] = [[nproj（C，1）···nproj（C，n）]](ii) $t。nproj（C，1）· ·nproj（C，n）=t<$BPi174N. Roohi等人/理论计算机科学电子笔记255（2009）159----ǁ ǁǁChor和Peer语言都使用跟踪语义。因此，为了检查Chor规范的可实现性，我们需要将Chor规范的迹集与所有对等点的并行组合的迹集进行比较。 我们证明在定理3.3中，Chor规范的迹集等于FSP编码。我们在推论4.6中表明，我们的编码也保留了Peer语言的语义。因此，我们必须检查Chor和peers的FSP规范是否产生相同的轨迹集（其中隐藏了τ动作）并终止。 虽然Chor的规范是无死锁的，但由交互对等体（使用自然投影生成）组成的最终系统的规范可能会导致死锁。除了检查两个规范具有相同的轨迹集之外，不同对等点的并行组合也必须是无死锁的。使用LTSA工具箱可以轻松计算此检查。此外，可以执行LTSA提供的任何类型的测试，例如检查Chor和Peer规范中不同活动之间的Magee和Kramer在[9]中解释了如何从FSP生成一些Java代码。因此，在我们的方法中，可以遵循这些指导方针以实现快速原型化，从而从FSP规范实现真正的对等体，并将其部署在具体系统的上下文中。在第5节中，我们将展示如何自动生成Java代码。从抽象描述中实现可执行服务也可以使用Pi4SOA技术[1]或遵循[10]中提出的指南例4.8对于每个PeerP，c2fpi（Stock）中所有不涉及P的操作都被隐藏。我们的示例中的三个对等体由以下FSP规范编码：1. 经纪人=2.c2f pi（库存）;结束@{铁箱，钢箱，投标箱，看箱，通知箱}。市场=c2f pi（股票）;结束@保存，检查，出价，结果，bd。Board=c2f pi（Stock）; END @ result = bd，notify bd bk，change bd.图2显示了从上述FSP过程生成的这些对等体的最小化LTS。tau1steel_bk查看bkτE经纪人0tau8铁_BK2tau3tau4bid_bk_5tau通知_bd_bk7板结果_bd_bdtau3change_bd市场save_202check_204bid_bk_204结果_bd_bd014 0 1 3 EtauEnotify_bd_bkcheck_5save_图二. 股票市场：最小化同行最后，我们并发地运行所有这些对等点。整个系统的FSP流程是：Peers=（Broker Market Board）。至于可实现性测试，首先，我们使用LTSA从FSP流程Stock和Peers计算LTS。接下来，我们使用ltscompare（属于3.N. Roohi等人/理论计算机科学电子笔记255（2009）159175mCRL 2工具集[6]，并发现它们产生相同的轨迹集（第
我的内容管理
展开
