基于博弈语义和CSP的软件模型检测方法的研究与评估 - 2005年计算机科学电子笔记.

理论计算机科学电子笔记128（2005）105-125www.elsevier.com/locate/entcs基于博弈语义和CSP1的软件模型检测AleksandarDimovskiandRankoLazi'c英国考文垂大学计算机科学系CV47AL摘要提出了一种基于游戏语义和CSP的软件模型检测方法。开放程序片段的CSP进程，代表他们的游戏语义组成建模。这种翻译是由一个原型编译器执行的。通过使用FDR工具进行跟踪细化来检查观察等效性和属性验证。 有效性 我们的方法进行了评估的几个例子。关键词：软件模型检测，游戏语义，CSP进程代数，FDR细化检查器1介绍模型检查[6]是一种基于语义的系统验证技术：验证者检查给定系统的语义是否满足某些属性。它已经获得了工业界的认可，因为与模拟，测试和定理证明的方法相比，模型检查可以自动和详尽地验证，并且它还报告了反例。模型检测的成功主要是针对硬件和通信协议。近年来，软件模型检测已成为一个活跃而重要的研究和应用领域（如[5]）。不幸的是，将模型检查应用于软件是复杂的，有几个因素，1我们感谢EPSRC的支持（GR/S52759/01）。第二位作者也得到了英特尔公司的支持。1571-0661 © 2005 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2005.04.007106A. 季莫夫斯基河Lazic '/Electronic Notes in Theoretical Computer Science 128（2005）105从建模程序的困难（由于与硬件描述语言相比编程语言的复杂性）到使用通常的时间逻辑形式主义来指定软件的有意义属性的困难。另一个原因是状态爆炸问题：工业程序很大，模型检查需要计算。上述许多问题是由于难以获得软件的健全和完整的语义模型，并以适合于自动分析的算法方式表示这些模型游戏语义有潜力克服这些问题，因为它已经为各种编程语言和逻辑系统产生了第一个准确的，即完全抽象和完全完整的模型（例如[1]）。最近，有研究表明，完全抽象的基于博弈的二阶有限理想化大陵五模型（即有限数据类型和没有递归）与迭代可以只用正则表达式表示[10]，这可以用于有效的程序分析和验证[3]。游戏语义有几个非常适合软件模型检查的特性它产生具有最高抽象级别的观察上完全抽象的模型，因为计算期间的内部状态变化被抽象掉了。它可以在组成上对上下文中的术语进行建模，即打开程序片段。这种能力对于分析包含未定义（自由）变量和过程的软件组件的属性至关重要我们提出了一种基于游戏语义和CSP进程代数（例如[15]）的组合软件建模和验证方法。 我们专注于二阶有限理想化的大陵五与迭代。任何上下文中的术语的游戏语义都表示为CSP过程。通过检查CSP过程之间的跟踪细化，可以确定项之间的观测等价性和常规属性的验证。与正则表达式方法[10]相比，这种基于CSP的方法有几个好处。使用CSP中可用的各种运算符，程序项以清晰和组合的方式表示为过程对项进行建模的过程被定义为对其子项进行建模的过程的并行组合，同步事件被隐藏。CSP过程之间的跟踪细化可以通过FDR工具自动检查[9]，该工具针对过程的并行网络的验证进行了高度优化。FDR还提供了一系列组合状态空间约简算法[14]，使更小的模型能够在细化检查之前或期间生成。我们已经实现了一个原型编译器，给定任何条款的上下文中，输出一个CSP过程表示其游戏语义。可将输出加载到ProBe工具中进行交互式探索，或加载到FDR工具中A. 季莫夫斯基河Lazic '/Electronic Notes in Theoretical Computer Science 128（2005）1051079自动分析。FDR还包含一个交互式调试器，当对细化查询的回答是否定的时。我们的方法的有效性进行评估的两个例子的几个变种 一些实验结果表明，对于最小模型生成，我们优于基于正则表达式的方法[3]。本文的组织结构如下。第2节和第3节简要回顾了程序设计语言，其游戏语义的CSP表示，以及观察等价性的验证。进一步的细节可以在同伴论文[7]中找到，该论文集中于理论，而本文则专注于应用和属性验证。第4节展示了如何在有限迹上或作为有限自动机的线性时序逻辑中给出的性质可以被验证。在第5节和第6节中，我们将介绍编译器和两个案例研究。2编程语言我们编译器的输入是一个二阶有限代数迭代的上下文中的项。Idealised Algol[12]是一种紧凑的编程语言，类似于Core ML，它结合了命令式语言的基本特征和完整的高阶过程机制。该语言具有基本数据类型τ，即布尔型和整数的有限子集。该语言的短语类型是表达式、命令和变量，以及一阶函数类型。τ：：= int | boolσ：：= exp[τ]| Comm| var[τ]θ：：= σ|σ×σ×···σ→ σ使用形式为Γ M：θ的类型判断来引入项，其中Γ={i1：θ1，· · ·，ik：θk}。表达式类型的术语由常量和算术/逻辑运算符（E1E2）构建。命令类型的术语由标准的命令操作符构建：赋值（V：=E），条件（如果B，则M1，否则M2），while循环（当B做C时），排序（CoM，注意命令不仅可以与命令排序 ， 还 可 以 与 表 达 式 或 变 量 排 序 ） ， no-op （ 跳 过 ） 和 非 终 止 命 令（diverge）。也有用于解引用变量的术语形成器（！V）、一阶自由标识符对参数的应用（iM1···Mk）、局部变量声明（C中的new [τ] i）和函数定义构造函数（leti（i1：σ1，.，k：σk）= N（M）。全打字可以在[7]中找到规则。108A. 季莫夫斯基河Lazic '/Electronic Notes in Theoretical Computer Science 128（2005）105θexp[τ]var[τ]var[τ]σj一Q^3CSP模型在这里，我们回顾了CSP表示的游戏语义的程序术语的主要属性。这种表示的细节和一些例子可以在[7]中找到。游戏语义的介绍可参见[2]。关于CSP的全面文本是[15]。3.1类型和术语对于每一种类型θ，我们将一组可能的事件联系起来，即字母表Aθ。 类型的字母表包含称为问题的事件q∈Qθ，其被附加到具有名称Q的通道，并且对于每个问题q，存在一组事件a∈Aq称为应答，其被附加到具有名称A的通道。Aint={0，···，Nmax− 1}，bool={true，false}Qexp[τ]={q}，Aq=AτQ={run}，A={done}CommQvar[τ]={read，write. X|x∈ Aτ}，A读Qσ1×···×σk →σ0 ={j. Q|q ∈ Qσj，0 ≤j ≤ k}，=Aτ，A写。x={ok}J. Qσ1×···×σk→σ0 ={j. 一|a∈Aq}，其中0≤j≤ kAθ= Q。Qθ= A。q∈Qθ我们通过CSP过程[[ΓM：σ]]CSP解释任何类型的上下文项Γ M：σ，LCSP（Γ_M：σ）={t|不 <$C <$∈迹（[[Γ<$M：σ]]CSP）}是该术语的所有完整博弈策略的集合。这个过程的事件来自字母表AΓσ，定义为：A1：θ= 1。Aθ={1.α| α∈ Aθ}Ar=i：θ∈rAi：θArσ=ArAσ过程[[ΓM：σ]]CSP的合成定义在附录A中给出。3.2观测等价两个项M和N在观测上等价，记为M<$σN，当且仅当对于任何上下文C[−]，使得C[M]和C[N]都是n型闭项，C[M]收敛当且仅当C[N]收敛。文[1]证明了这与M和N的策略的完全对策集相等一致，即：博弈模型是完全抽象的一A. 季莫夫斯基河Lazic '/Electronic Notes in Theoretical Computer Science 128（2005）105109Γ►σΓ►σ^F对于本文中处理的编程语言片段，在[7]中表明，观察等价性由两个跟踪细化捕获：定理3.1（观测等价性）我们有：（一）Γ <$M <$σN 惠[[ΓM：σ]]CSPQRUNA±T[[Γ<$N：σ]]CSP[[Γ<$N：σ]]CSPQRUNA±T [[Γ<$M：σ]]CSP其中RUNA=？x：A→运行A。 Q在[7]中还证明了表示任何项的过程是有限状态，因此观测等价性是可以使用FDR判定4财产核查除了检查两个程序项的观测等价性之外，还希望能够检查项的属性。 回想一下，对于任何术语， ΓM：σ，CSP过程[ΓM：σ]]CSP具有如下性质：终端迹线LCSP（Γ_M：σ）={t|不 <$C <$∈迹（[[Γ<$M：σ]]CSP）}是策略为ΓM：σ的所有完全对策的集合。因此，我们专注于有限迹的性质，并认为，当且仅当LCSP（ΓM：σ）中的所有迹都满足它时，ΓM：σ满足这样的性质4.1线性时序逻辑一个标准的书写线性行为属性的方法是线性时态逻辑。给定一个有限集合，我们考虑下面的公式。除了命题连接词之外，线性逻辑还包含时间运算符φ：：=真实|虚假|a∈Σ|¬φ|φ1∨φ2|Ⓧφ|φ1Uφ2我们称之为LTL逻辑，因为我们给它的语义超过有限的痕迹（即序列）的elements的f。特别地，对于多个a，φ 1，φ2和φ1，φ2要求迹为非空的。对于任何长度为k的迹t，我们将其元素110A. 季莫夫斯基河Lazic '/Electronic Notes in Theoretical Computer Science 128（2005）105F作为t1，...，tk，我们把它的第i个子集写成ti，.，tk.不|=true t| =false不|= a我的t=/且t1=a不|=<$φ我的不|= φ不|= φ1φ2我的不|= φ1或t| = φ2不|= φ我的t= /t2|=φ不|= φ1Uφ2我的存在i∈ {1，.、|不|}使得ti|= φ2并且对于所有j∈ {1，.，i− 1}，tj|= φ1The ‘eventually’ and ‘always’ operators can be defined as abbreviations inthe usualQφ=真Uφ Qφ=<$Q <$φ“下一次”和“直到”操作符的对偶·φ=<$$> φ1Vφ2=<$（<$φ1U<$φ2）它们的语义如下：不|=·φit=或t2|=φ不|= φ1V φ2 i， 对于所有i∈ {1，.、|不|}，ti|= φ2，或者存在i∈ {1，.、|不|}使得ti|= φ1并且对于所有j∈ {1，.，i}，tj|= φ2项ΓM：σ满足LTL AΓσ的公式φ 当且仅当对于每个迹t∈ LCSP（Γ <$M：σ），t| = φ。例4.1考虑以下项：b：bool，C：bool ► while b do C：本学期CSP工艺的过渡系统如图1所示。由于b和C都是自由标识符，因此这个过程的成功终止跟踪都是对应于当b的值为真时执行C零次或更多次，以及当b的值为假时完成的跟踪。因此，这一项满足Qb。A. false，但不满足QC。Q. 运行.它也满足Q（b）。A. 真→QC。Q. 运行），但不满足Q（b. Q. q→QC。Q. 运行）。A. 季莫夫斯基河Lazic '/Electronic Notes in Theoretical Computer Science 128（2005）105111FφFφJJ0φ• CSP工艺P被设计成使得t| = φ当且仅当t^$> C <$∈迹（P<$）;φC.A.doneC.Q.runb.A.trueQ.runb.Q.qb.A.falseA.doneFig. 1. while b do C的用法有一种算法，给定LTL的任何公式φ，构造：φ φ• 一个有限过渡系统，它具有与P的相同的有限迹线。这类似于构造一个接受有限迹的有限自动机t当且仅当t| = φ。 详情见附录B。因此，我们有一个判定过程，给定一个规划项Γ<$M：σ和LTLAΓ <$σ的一个公式φ，它检查满足。它的工作原理是构造CSP过程[[Γ<$M：σ]]CSP和PAΓ<$σ，并检查traces refinement2（二）PAΓσQ运行A±T[[ΓM：σ]]CSPφΓ►σ4.2有限自动机更一般地说，任何性质，使得满足它的所有有限迹的集合是正则的，都可以在CSP中表示。假设A是一个自动机，它有有限个字母表，有限个状态集Q，转移关系T<$Q×<$Q，初始状态Q0<$Q，接受状态F<$Q。对于任何q∈Q\F，我们定义对于任何q∈F，我们定义Pq=Q（q， a，q）∈Ta→PqJPq=（Qa→PqJ）QSKIP（q， a， q）∈T这是一个有效的递归CSP过程定义系统，因此我们可以让PA=QPqq∈ Q于是我们知道PA有无限多个状态，t被Ai <$t^$>C <$∈迹（PA）2如果φ包含U运算符，则用于构造转换的标准FDR过程P AΓ <$σ系统可能不会终止。 在这种情况下，上面的跟踪细化可以是由FDR检查，或者通过表示为CSP过程，附录B中的算法或4.2节中的方法产生的P A Γ σ。112A. 季莫夫斯基河Lazic '/Electronic Notes in Theoretical Computer Science 128（2005）105Γ►σFa，ca，b，cB图二. 有限自动机例4.2考虑图2中的自动机A， 他的字母表是{a，b，c}。 它接受有限迹t当且仅当t |= Qb.CSP工艺PA定义为：PA=P1P1=（a→P1）Q（b→P2）Q（c→P1）P2=（a→P2）Q（b→P2）Q（c→P2）QSKIP因此，给定一个程序项ΓM：σ和一个字母表为AΓσ的有限自动机A，我们可以通过检查（例如，使用FDR）跟踪细化（3）PAQRUNA±T[[ΓM：σ]]CSP这也提供了另一种确定满足公式φ的方法，LTL AΓσ：构造一个接受有限迹t的有限自动机A，当且仅当t| = φ，然后检查上面的跟踪细化。5编译器我们已经在Java中实现了一个编译器[4]，它自动将上下文中的术语（即开放程序片段）转换为表示其游戏语义的CSP进程。输入是代码，带有简单的类型注释来指示有限整数数据类型的大小。由此产生的CSP进程由编译器输出的机器可读CSP [15]中的脚本定义。编译器输出的脚本可以加载到工具ProBE中，用于过渡系统的交互式探索，FDR用于自动分析和交互式调试[9]。FDR的功能之一是检查两个有限状态进程之间的跟踪细化。正如我们上面看到的，这可以用来决定两个项（1）、线性时态逻辑公式（2）的满足和正则语言（三）、FDR提供了许多分层压缩算法，可在模型生成或细化检查期间应用。我们的编译器生成的脚本通常包含将菱形消除和强互模拟应用于子进程的指令，这些子进程对局部变量声明子项进行这利用了游戏语义学A. 季莫夫斯基河Lazic '/Electronic Notes in Theoretical Computer Science 128（2005）105113隐藏局部变量和作为其作用域的子项之间的交互。这些相互作用成为无声（即τ）转换，使模型能够简化。本文中考虑的编程语言片段具有有限数据类型，而不是所有整数的无限数据类型。我们处理的是模k的整数集合。每个整数变量都声明为int%k类型，一些k和不同的k值可以用于不同的变量。 具有不同整数类型int%k1和int%k2的变量之间的运算被解释为对k1和k2的最小值取模。6应用我们现在考虑上述方法的应用，并讨论两种示例的实验结果：排序算法和抽象数据类型实现。6.1排序算法在本节中，我们将分析冒泡排序算法，其实现如图3所示。代码包含一个Meta变量n，表示数组大小，它将被几个不同的值替换。数组中存储的整数类型为int%3，由值0、1和2组成。索引i的类型是int%n+1，即比数组的大小大1。冒泡排序的实现是标准的。程序首先将输入数组x[]复制到局部数组a[]中，然后对其进行排序并复制回x[]。被有效排序的数组a[]在程序外部不可见，因为它是局部定义的，在模型中只能看到非局部数组x图4中示出了n= 2的模型CSP过程的过渡系统。左半部分表示从x[]读取所有可能的值组合，而右半部分表示按排序顺序写入相同的值。表1包含最小模型生成的实验结果。实验包括在冒泡排序实现上运行编译器，然后让FDR为结果进程生成一个转换系统后一个阶段涉及许多层次压缩，如第5节所述。我们以分钟为单位列出了执行时间，最大生成的转换系统的大小，以及最终转换系统的大小我们在Research Machines 2.5 GHz Xeon和2GBRAM上运行FDR。基于正则表达式的工具的结果是在具有2GB RAM的Sun-Blade 100上获得的[3]。结果证实，这两种方法114A. 季莫夫斯基河Lazic '/Electronic Notes in Theoretical Computer Science 128（2005）105x.1.A.2x.0.Q.write.2x.1.A.1x.1.Q.qx.0.A.okx.0.A.2x.0.Q.write.0x.1.Q.write.2x.1.A.2Q.runx.0.Q.q x.0.A.1x.1.Q.qx.0.A.okx.1.Q.write.1x.1.x.0.Q.write.1x.1.A.2x.1.Q.write.0x.0.A.0x.1.Q.qx.0.A.okx.1.A.0x[n]：var int%3在new int%n中的newint%3a[n]+1i在while（i10，世代不成功。 显示的时间是FDR用来处理规范、处理实现和执行细化检查。除了检查给定项的外部行为的属性之外，我们还可以检查引用内部数据的断言断言可以使用局部函数assert添加到术语中，该局部函数的参数是布尔表达式。如果参数为true，assert函数不执行任何操作，否则它将调用非本地函数错误。在扩充项的游戏语义中，任何事件的发生都是错误的。0的情况。运行和错误0的情况。done表示断言违规。例如，我们可以检查，每当一个值y被添加到队列中，然后除了一个项目之外的所有项目都从队列中删除时，剩余的项目具有值y。我们通过将图6中的ANALYSE函数的调用替换为以下代码来实现：A. 季莫夫斯基河Lazic '/Electronic Notes in Theoretical Computer Science 128（2005）105119public int findDuplicate（int findDuplicate）{if b thenskip;else error（）;}在public void run（）{new int%ny iny=p;return（i）;while（队列大小>1）下一个（）;return（）;}在解析（add（p），next（），assert（validate（）：其中error（）和ANALYSE（int，int%n，int）是非本地命令。然后我们检查这个修改后的队列实现是否满足特性<$Qerror。我们在FDR上针对大小为m= 2的数据集和最大队列大小n= 2执行此操作。正如预期的那样，生成了一个反例跟踪，表明在n次ADD调用之后，即队列已满时，违反了此特定断言。 当断言被更正为仅应用于未满队列时，检查成功。7结论在本文中，我们将[7]中提出的软件模型检查方法扩展到检查线性时态逻辑公式或有限自动机的属性，并在两种示例上对其进行了评估：排序算法和抽象数据类型实现。实验结果表明，具有大的内部状态空间的开放程序片段可以被验证，部分原因是FDR工具用于并行进程网络的实时检查的效率。他们还表明，这种方法可以优于基于正则表达式的方法[3]。作为未来的工作，我们打算扩展编译器，使参数化的程序条款（如参数多态程序）被翻译成单参数化CSP过程。这样的过程可以通过结合CSP和数据规范形式主义的技术来分析（例如，[8，13]）或基于数据独立性的算法[11]。引用[1] S.Abramsky和G.McCusker，线性，共享和状态：具有主动表达式的理想化Algol的完全抽象游戏语 义 。 在 P.W. O 'Hearn 和 R.D.Tennent 编 辑 的 “Algol-like la n g u ages” 中 。 1997 年，《Birkhúauser》。[2] 林志玲，游戏语义学，国立台湾大学，2001。120A. 季莫夫斯基河Lazic '/Electronic Notes in Theoretical Computer Science 128（2005）105[3] S.Abramsky，D.Ghica，A.Murawski和C.- H.L.Ong，将游戏语义应用于组合软件建模和验证。在TACAS的会议记录中，LNCS2988，421[4] A.W.Appel和J.Palsberg，《Java中的现代编译器实现》，第2版。剑桥大学出版社，2002年。[5] T.Ball和S.K.Rajamani，SLAM项目：通过静态分析的可重构系统软件。在POPL的诉讼中，ACM SIGPLAN Notices37（1），2002年1月。[6] E.M.Clarke，O.Grumberg和D.Peled，模型检验。麻省理工学院出版社，2000年。[7] A. 我也是。Lazic，CSP代表GameSemanticsforsecccorderIdealzedAlgol。在ICFEM会议记录中，LNCS，2004年11月。[8] A.Farias，A.Mota和A.Sampaio，《高效CSP-Z数据抽象》。In Proceedings of IFM，LNCS2999，108[9] Formal Systems（Europe）Ltd，Failures-Divergence Refinement：FDR2 Manual，2000.[10] D.Ghica和G.McCusker，二阶理想化大陵五的正则语言语义学。Theoretical Computer Science309（1[11] R. Lazic，ASemanticSudyofDataIndepenndencewithApp l icationstoModelCecking. 博士论文，计算机实验室，牛津大学，1999。[12] J.C.雷诺兹，大陵五的本质。In Proceedings of ISAL，345-372，Amsterdam，Holland，1981.[13] M.Roggenbach，CSP-CASL - A new Integration of Process Algebra and AlgebraSpecification。在AmiLP的会议记录中，TWLT21，2003。[14] A.W.罗斯科，P.H.B.Gardiner，M.H.Goldsmith，J.R.Hulance，D.M.Jackson和J.B.Scattergod，用于模型检查CSP的分层压缩或如何检查1020吃哲学家们的饭来解决僵局在TACAS的会议记录中，LNCS1019，133[15] A.W.Roscoe，《并发的理论与实践》。 Prentice Hall，1998年。A. 季莫夫斯基河Lazic '/Electronic Notes in Theoretical Computer Science 128（2005）1051219σA术语流程表达构建体[[τv：exp[τ]CSP=Q。q→A。v→SKIP，v∈Aτ是一个常数[[ΓnotB：exp[bool]]]CSP=[[ΓπB：exp[bool]]]CSP[Q1/Q，A1/A]π{|Q 1，A 1|}（Q. q→Q1。q→A1？v：Abool→A. （not v）→SKIP）\ {|Q1，A1|}[[r∈E1·E2：exp[τ]CSP=[[ΓεE1：exp[τ]CSP[Q1/Q，A1/A]π{|Q 1，A 1|}（[[ΓεE2：exp[τ]CSP[Q2/Q，A2/A]π）{|Q2，A2|}（Q. q→ Q1。q→A1？v1：Aτ→ Q2. q→A2？v2：Aτ→A. （v 1·v 2）→跳过）\ {|Q2，A2|}）|Q1，A1|}CSP= Q。q→1。Q. q→1。一个？v：Aτ→A. v→跳过命令结构CSP= Q。运行→A。完成→跳过[[Γdiverge：]]CSP=STOP[[ΓωCoM：σ]]CSP=[[ΓπC：comm]]CSP[Q1/Q，A1/A]{|Q 1，A 1|}（[[Γ<$M：σ]]CSP[Q2/Q，A2/A]<${|Q2，A2|}（Q？q：Qσ→Q1。运行→A1。完成→Q2。q→A2？a：Aq→A。a→跳过）\ {|Q2，A2|}）|Q1，A1|}122A. 季莫夫斯基河Lazic '/Electronic Notes in Theoretical Computer Science 128（2005）105σσ[[rif B then M1else M2：σ]]CSP=[[ΓπB：exp[bool]CSP[Q0/Q，A0/A]π{|Q0，A0|}（[[Γ<$M1：σ]]CSP[Q1/Q，A1/A]QSKIP）{|Q 1，A 1|}（（[[Γ<$M2：σ]]CSP[Q2/Q，A2/A]QSKIP） <${|Q2，A2|}（Q？q：Qσ→Q0。q→A0？v：Abool→（Q1. q→A1？a：Aq→A。a→跳过<|问题2.|Q2. q→A2？a：Aq→A。a→跳过））\{|Q2，A2|}）|Q1，A1|{\fn黑体\fs22\bord1\shad0\3aHBE\4aH00\fscx67\fscy66\2cHFFFFFF\3cH8080}|Q0，A0|}[[r= 0，B = 0，C =0]]CSP=（µ pJ. （[[B：A]] CSP[Q/Q，A/A] o pJ）Q（A. 完成→跳过））1 19{|Q 1，A 1，A|}.（µ pJJ. （[[C：N]] CSP[Q/Q，A/A] o pJ J）Q（A. 完成→跳过））2 29{|Q 2，A 2，A|}（Q. run→µp。问题1. q→A1？v：Abool-（Q2. run→A2. 完成→p<|v>|A. 完成→跳过））\ {|Q2，A2|{\fn黑体\fs22\bord1\shad0\3aHBE\4aH00\fscx67\fscy66\2cHFFFFFF\3cH8080}|Q1，A1|}CSP= Q。运行→1。Q. 运行→1。A. 完成→A。完成→跳过可变结构[[ri：var[τ]CSP=（Q. 读取→1。Q. 读取→1。一个？v：Aτ→A. v→跳过）Q（Q. 写什么？v：Aτ→1。Q. 写. v→i。A. ok→A.ok→SKIP）[[ΓV：=M：]]CSP=[[rM：exp[τ]CSP[Q1/Q，A1/A]{|Q 1，A 1|}（[[ΓV：var[τ]CSP[Q2/Q，A2/A]）{|Q2，A2|}（Q. 运行→ Q1。q→A1？v：Aτ→ Q2. 写. v→ A2。好→A. 完成→跳过）\ {|Q2，A2|}）|Q1，A1|}.A. 季莫夫斯基河Lazic '/Electronic Notes in Theoretical Computer Science 128（2005）105123.σjFφFFF99σ• CSP工艺P被设计成使得t| = φ当且仅当t^$> C <$∈迹（P<$）;[[I'm sorry！V：exp[τ]CSP=[[ΓV：var[τ]CSP[Q1/Q，A1/A]{|Q 1，A 1|}（Q. q→ Q1。读→A1？v：Aτ→ A. v→ SKIP）\{|Q1，A1|}[[r=new [t]iin M：n]]CSP=([[[[]]CSP]]{|I，A|}其中，aint= 0，abool=false，并且：Ui：var [τ]，aτ）\{|ι|}Ui：var[τ]，v=（i. Q. 读取→1。A！v→Ui：var[τ]，v）Q（i. Q. 写什么？vJ：Aτ→1。A. ok→Ui：var[τ]，vJ）Q（A. 完成→跳过）应用和功能[[（M1. Mk）：σ]]CSP=Q？q：Qσ→1。0的情况。Q. q→微升。（Qkj=1（[[Γ]Mj ：σj]]CSP{|Q、A|}I. J. Q？q：Qσj→Q。q→