软件学报  2018, Vol. 29 Issue (6): 1607-1621   PDF    
消息传递的MSVL通信机制及其实现
王小兵, 郭文轩, 段振华     
西安电子科技大学 计算机学院, 陕西 西安 710071
摘要: 建模、仿真和验证语言(MSVL)是一种时序逻辑编程语言,它是投影时序逻辑(PTL)的可执行子集.MSVL和PTL可用于并发系统的建模和性质验证.然而,MSVL缺少一种消息传递的通信机制,这种机制对于并发分布式系统的建模和验证至关重要.说明了如何在MSVL中开发和实现合适的机制来对分布式系统进行建模和验证.该机制首先定义了通道结构,对通信语句和进程结构进行形式化描述;接着介绍了这些通信语句的实现机制;最后提供了一个关于电子合同签名协议的建模和验证实例,说明消息传递在MSVL中的工作原理.
关键词: 通道     消息传递     通信机制     PTL     时序逻辑程序设计    
Communication Mechanism and Its Implementation for MSVL Based on Message Passing
WANG Xiao-Bing, GUO Wen-Xuan, DUAN Zhen-Hua     
School of Computer Science and Technology, Xidian University, Xi'an 710071, China
Foundation item: National Natural Science Foundation of China (61672430, 61420106004, 61732013, 61402347); Fundamental Research Funds for the Central Universities (JBG160306)
Abstract: The modeling, simulation and verification language (MSVL) is a temporal logic programming language as well as an executable subset of projection temporal logic (PTL). MSVL and PTL are used for modeling and verifying properties of concurrent systems. However, MSVL lacks a mechanism of communication based on message passing which is essential for modeling and verifying concurrent distributed systems. This paper shows how to develop and implement a suitable mechanism in MSVL to model and verify concurrent distributed systems. First, channel structure is defined while communication statements and process structures are formalized. Then, the implementation mechanisms for those communication statements are presented. Finally, a modeling and verification example involving an electronic contract signing protocol is provided to illustrate how the message passing works in MSVL.
Key words: channel     message passing     communication mechanisms     projection temporal logic     temporal logic programming    

形式化验证已成功应用于从数字电路设计到软件工程等领域.在形式化验证中, 时序逻辑是描述和推理并发系统性质的有效工具[1, 2].投影时序逻辑(projection temporal logic, 简称PTL)[3]扩展了区间时序逻辑(interval temporal logic, 简称ITL)[4]并广泛应用于系统的规范和验证[5-7].在大多数情况下, 系统建模技术与时序逻辑无关, 而所需的性质则用时序逻辑公式来描述.所以, 由于不同的逻辑语言有不同的符号和语义, 而导致验证变得困难.为了改善这种情况, 一种方法是使用相同的语言对系统建模和描述性质.建模、仿真和验证语言(modeling, simulation and verification language, 简称MSVL)是一种时序逻辑程序设计语言, 它是PTL的可执行子集, 使用MSVL可以对并发系统进行形式化描述、仿真和验证[8].这种方法用MSVL程序来对并发系统建模, 系统的性质则使用投影时序逻辑(propositional projection temporal logic, 简称PPTL)公式来描述.通过在同一时序逻辑框架内的模型检测方法, 可以验证并发系统是否满足性质.

并发编程模型中, 进程上最重要的两个问题就是进程通信和进程同步[9].指令式编程语言的通信模型通常基于共享变量或消息传递.在基于共享变量的模型中, 同步通常是显式的:除非编程人员进行了特殊处理, 否则接收进程在发送方写入变量之前可以读取变量的旧值.相反, 在基于消息传递的模型中, 同步通常是隐式的:消息必须发送后才能够被接收.如果一个进程试图接收尚未发送的消息, 那么它将等待直到发送方发送消息.

目前, 大多数时序逻辑编程语言都支持基于共享变量的通信机制, 如MSVL, XYZ/E[10], METATEM[4]和Tempura[11].但是在这些机制下, 并发系统的执行可能代价高昂且缺乏可靠性和可预测性[12].这是因为并行进程通过共享变量进行同步会有些棘手, 可能会导致很多问题, 比如互斥.特别是在若干节点都分布于不同地理位置的分布式系统中, 允许一些变量或全部变量共享是不方便的.换言之, 通过消息传递, 多个节点之间的通信和同步会具有更好的特性.为了能够描述并发和分布式系统的行为并对其形式化建模和验证, 我们将使用消息传递的通信机制来扩展MSVL.

本文的理论贡献包括:

(1) 形式化的通道结构用来描述基于消息传递的进程间通信, 它是传输消息的缓冲区, 并且引入面包店算法[13]来解决互斥问题;

(2) 通信语句用来发送或接收进程执行后的消息;

(3) 进程结构被定义为PTL的组合谓词, 用来描述系统的行为模式.因此, 一个系统可以被建模为多个进程的组合;

(4) 提供了这些通信语句的实现机制.

上述概念为时序逻辑编程提供了一种可行的消息传递通信机制.MSVL通过这种机制的扩展, 就能用来对并发和分布式系统进行模拟、仿真和验证.

为了说明上述理论的实用性, 我们将应用扩展的MSVL对电子合同签名协议[14]进行建模与验证.协议中的所有参与方都用进程描述, 各方之间的通信都消息传递并且通过通道传输.然后, 所有进程基于消息传递来运行和通信, 以实现电子合同签名协议.因此, 我们能够检查关注的系统性质是否满足指定协议, 系统性质使用PPTL公式描述.本文将之前的工作[15]扩展到以下几个方面:首先, 增强通道的功能, 一个通道可以用于同步多个发送方和接收方, 而之前的版本一次只能被一个进程访问; 还制定了一组通信语句的锁定策略, 以解决不同的访问进程之间的冲突.

本文第1节回顾PTL相关理论.第2节简要介绍MSVL语言.第3节形式化定义通道结构、消息传递的通信语句和进程结构.第4节给出通信语句的实现机制.第5节提供采用扩展MSVL对电子合同签名协议进行建模和验证的应用实例.第6节对比其他方法, 分析新机制的优劣.最后, 第7节得出结论.

1 投影时序逻辑

V是可数的静态和动态变量的集合, Π是可数的命题集合, 项e和公式p的归纳定义如下:

$\begin{align} &e::=x|{{\rm{ O}}}e|\Theta e|f({{e}_{1}}, ..., {{e}_{m}}) \\ &p::=\pi |{{e}_{1}}={{e}_{2}}|P({{e}_{1}}, ..., {{e}_{m}})|{{p}_{1}}\wedge {{p}_{2}}|{{p}_{1}}\vee {{p}_{2}}|\neg p|\exists v:p|{{\rm{ O}}}p|({{p}_{1}}, ..., {{p}_{m}})\text{ }prj\text{ }p \\ \end{align}$

上述语法中, xV是动态变量或者静态变量, πΠ是命题, 且m≥1.在f(e1, …, em)与P(e1, …, em)中, f是函数, P是谓词.每个函数和谓词都有一个固定的参数数量, 其范围是非负整数.注意, 参数数量为0的函数即常量.一个公式(项)如果不包含任何时态运算符(即O, Θ或prj)就称为状态公式(项); 否则, 它就是一个时序公式(项).

状态s是一个二元组(Iv, Ip), 对于每个变量vs[x]=Iv[x], 每个命题πs[π]=Ip[p].Iv[x]是集合$ D=\mathbb{Z}\cup \mathbb{S}\cup \mathbb{L} $中的值或nil(表示未定义值), $ \mathbb{Z} $表示整数集, $ \mathbb{S} $={0, …, 9, a, …, z, A, …, Z}*表示字符串集, 而$ \mathbb{L}=\left\{ \left\langle {{l}_{0}}, \ldots , {{l}_{n}} \right\rangle |{{l}_{i}}\in \mathbb{Z}\cup \mathbb{S}, n\in {{N}_{0}} \right\} $表示列表集合.Ip[π]是集合B={true, false}中的值.区间σ=〈s0, s1, …〉是一个非空(可能无穷大)的状态序列.区间长度记为|σ|, 当σ为无穷区间时, |σ|为ω, 否则为其状态数减1.为了统一有穷和无穷区间的符号, 我们使用扩展整数作为索引.也就是说, 我们考虑自然数集合ω, 即ω=∪{ω}, 并且扩展比较运算符=, < , ≤到ω, 考虑到ω=ω, 且对于所有i, 有i < ω.⪯定义为≤-{ω, ω}.通过这些符号, 用σ(ij)(0≤ij≤|σ|)表示子区间〈si, …, sj〉, σ(k)(0≤k⪯|σ|)表示〈sk, …, s|σ|〉.用σ·σ′来表示σ和另一区间σ′的连接.为了定义投影操作的语义, 我们需要一个辅助运算符来进行区间运算.设σ=〈s0, s1, …〉是一个区间, n0, …., nh(h≥0)是整数且有0≤n0n1≤…≤nh⪯|σ|.则σn0, …., nh上的投影是一个区间(称作投影区间), 即$\sigma \downarrow ({{n}_{0}}, ..., {{n}_{h}})=\langle {{s}_{{{m}_{_{0}}}}}, ..., {{s}_{{{m}_{k}}}}\rangle $, 其中, m0, …., mk是通过删除n0, …., nh中的所有冗余元素得到的, 比如:〈s0, s1, s2, s3, s4〉 ↓〈0, 0, 2, 2, 2, 3〉=〈s0, s2, s3〉.

PTL项或者公式的解释$ \mathcal{I} $=(σ, i, k, j)是一个四元组, σ=〈s0, s1, …〉是一个区间, ik都是非负整数, j是整数或者ω, 且ikj≤|σ|.我们用(σ, i, k, j)表示一个项或公式在一个当前的状态是sk的子区间σ(ij)上被解释.对于每个项e, e的赋值和解释$ \mathcal{I} $=(σ, i, k, j)相关, 表示为$ \mathcal{I} $[e], 它是集合D中的值.对项的解释归纳定义如下所示:

$ \begin{array}{l} \mathcal{I}[x] = {s_k}[x] = I_v^k[x] \hfill \\ \mathcal{I}[{\rm O}e] = \left\{ {\begin{array}{*{20}{l}} {(\sigma , i, k + 1, j)[e], {{如果 }}k < j} \\ {nil, ~~~~~~~~~~~~~~~~~~~~~{{ 否则 }}} \end{array}} \right. \hfill \\ \mathcal{I}[\Theta e] = \left\{ {\begin{array}{*{20}{l}} {(\sigma , i, k - 1, j)[e], {{如果 }}i < k} \\ {nil, ~~~~~~~~~~~~~~~~~~~~~{{ 否则 }}} \end{array}} \right. \hfill \\ \mathcal{I}[f({e_1}, ..., {e_m})] = \left\{ {\begin{array}{*{20}{l}} {\mathcal{I}[f](\mathcal{I}[{e_1}], ..., \mathcal{I}[{e_m}]), {{ 如果对}}1 \leqslant h \leqslant m, 有\mathcal{I}[{e_h}] \ne nil} \\ {nil, ~~~~~~~~~~~~~~~~~~~~~~~~~~~~{{ 否则 }}} \end{array}} \right. \end{array} $

解释与公式间的满足关系归纳定义如下.

(1) $ \mathcal{I} $π当且仅当$ {s_k}[\pi ] = I_p^k[\pi ] = {\rm{true}} $;

(2) $ \mathcal{I} $e1=e2当且仅当$ \mathcal{I} $(e1)=$ \mathcal{I} $(e2);

(3) $ \mathcal{I} $P(e1, …, em)当且仅当对1≤hm, 有$ \mathcal{I} $[eh]≠nil并且$ \mathcal{I} $[P]($ \mathcal{I} $[e1], …, $ \mathcal{I} $[em])=true;

(4) $ \mathcal{I} $⊨¬p当且仅当$ \mathcal{I} $p;

(5) $ \mathcal{I} $p1p2当且仅当$ \mathcal{I} $p1并且$ \mathcal{I} $p2;

(6) $ \mathcal{I} $⊨∃v:p当且仅当存在区间σ′, 满足|σ′|=|σ|, (σ′, i, k, j)⊨p, 并且σσ′除了在状态kv的解释可以不同外,对其他变量的解释都相同;

(7) $ \mathcal{I} $⊨Op当且仅当k < j并且(σ, i, k+1, j)⊨p;

(8) $ \mathcal{I} $⊨(p1, …, pm) prj q, 若存在整数k=k0≤…⪯kmj使(σ, i, k0, k1)⊨p1, (σ, kh-1, kh-1, kh)⊨ph(对1 < hm)并且对下面的某种情况有(σ′, 0, 0, |σ′|)⊨q:

  km < j并且$\sigma ' = \sigma \downarrow ({k_0}, ..., {k_m}) \cdot {\sigma _{({k_m} + 1 \cdots j)}}$;

  km=j并且σ′=σ ↓(k0, …, kh)(0≤hm).

公式p被称为满足区间σ当且仅当(σ, 0, 0, |σ|)⊨p.如果在某些σ上有(σ, 0, 0, |σ|)⊨p, 那么p是可满足的.如果对于所有的σ有(s, 0, 0, |σ|)⊨p, 那么p是有效的, 记为⊨p.公式pq是等价的, 当且仅当⊨(pq), 记为pq.

连接符∨, →和↔的定义和经典逻辑中的定义相同.特别地, 对于任意公式p, 有true≜p∨¬p和false≜p∧¬p.导出公式和复合谓词如下所示.

$ \begin{align} &empty\triangleq \neg \text{Otrue}\ \ \ \ \ \ \ \ \ \ \ \ \ ~\ \ \ \ \ \ \ \ \ \ more\triangleq \neg empty \\ &p;q\triangleq (p, q)~prj\ empty\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \diamond \triangleq \text{true};p \\ &\square p\triangleq \neg \diamond \neg p\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ halt\left( p \right)\triangleq \square \left( empty\leftrightarrow p~ \right) \\ &keep(p)\triangleq \square (\neg empty\to p)~\ \ \ \ fin(p)\triangleq \square (empty\to p~) \\ &skip\triangleq \text{O}empty~\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {{p}^{*}}\triangleq empty\vee (p;{{p}^{*}})\vee p\square more \\ &len\left( 0 \right)\triangleq empty\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ ~len(n)\triangleq \text{O}len(n-1)(n>0) \\ \end{align} $
2 建模、仿真和验证语言MSVL

MSVL是PTL的一个可执行子集, 使用MSVL可以对并发系统进行建模.MSVL的算术表达式e和布尔表达式b都是PTL的项, 语法定义如下:

$ \begin{align} &op::=+|-|*|/|\bmod \\ &e::=n|x|{{\rm{ O}}}x|\Theta x|\max ({{e}_{0}}, ..., {{e}_{m}})|\min ({{e}_{0}}, ..., {{e}_{m}})|{{e}_{0}}\text{ }op\text{ }{{e}_{1}} \\ &b::=\text{true}|\text{false}|{{e}_{0}}={{e}_{1}}|{{e}_{0}}<{{e}_{1}}|\neg b|{{b}_{0}}\wedge {{b}_{1}} \end{align} $

其中, n是整数, x是变量.p, q是PTL公式, MSVL语句或程序定义如下.

●  整型声明语句:int(x)≜x;

●  字符串声明语句:str(x)≜x$ \mathbb{S} $;

●  列表声明语句:list(x)≜x$ \mathbb{L} $;

●  立即赋值语句:xex=eπx;

●  下一状态赋值语句:x:=eskip∧Oxe;

●  顺序语句:p; q;

●  条件语句:if b then p else q≜(bp)∧(¬bq);

●   While语句:while b do p≜(bp)*∧□(empty→¬b);

●  合取语句:pq;

●  选择语句:pq;

●  并行语句:p||qp∧(q; true)∨q∧(p; true);

●   Next语句:Op;

●   Always语句:□p;

●  区间长度语句:empty, skip, len(n);

●  存在语句:∃x:p;

●  状态框架语句:lbf(x)≜¬af(x)→∃b:(Θx=bx=b);

●  区间框架语句:frame(x)≜□(more→Olbf(x));

●  投影语句:(p1, …, pm) prj q;

●  等待语句:await(b)≜(frame(x1)∧…∧frame(xh))∧□(emptyb), 其中, xiVb={x|xb中}.

上述语句中, int(x), str(x), list(x), xe, x:=e, empty, skip, len(n), frame(x), await(b)是基础语句, 而其他的则是复合语句.声明语句int(x), str(x), list(x)分别表示x的值为整数、字符串、列表.MSVL有两种赋值语句.

●  立即赋值语句xee的值赋给变量x, 并将特殊命题πx置为true.对于每个变量x, 用πx来指示x是否被赋值, 因此也称作x的赋值标志.赋值标志可以用来实现重要的框架技术, 该技术保持变量从一个状态到下一状态的值不变[16];

●  另一种赋值方法是下一状态赋值x:=e, 应用于长度为1的区间, 即只有两个状态.下一状态赋值将前一个状态中e的值赋给第2个状态中的x, 并将相应的赋值标志设置为true.

区间长度语句empty, skip, len(n)采取了PTL公式的形式, 分别表示区间长度为0, 1, n.状态框架语句lbf(x)表示变量x若未赋值, 则其当前值与前一状态值相同.区间框架语句frame(x)表示变量x在区间上保持值不变, 除非它被显式地赋值.等待语句await(b)中, 表达式b包含若干变量, 当其他进程改变这些变量使得表达式为真时, 该进程才跳过等待语句继续执行.因此, 等待语句可以实现进程间的同步.复合语句中, ∃x:p表示局部变量x的范围为p.Op和□p分别表示p的值在当前区间的下一状态或所有状态上成立.合取语句pq表示pq并行执行, 在共同执行期间共享相同的区间和变量, 而选择语句pq表示p或者q执行.和合取语句相似, 并行语句p||q表示pq并行执行, 但是允许pq在不同的时间节点终止.也就是说, p的区间可能只是q区间的一个前缀, 反之亦然.例如, len(3)||len(4)是可满足的, 而len(3)∧len(4)是不可满足的.顺序语句p; q表示pq顺序执行.if b then p else q和while b do p语句的含义与传统命令式编程语言相同.

为了避免括号数量过多, 给出操作符优先规则见表 1.数字越小的运算符具有更高的优先级, 而数字相同的运算符具有相同的优先级.

Table 1 Precedence rules of MSVL 表 1 MSVL操作符优先级

MSV平台是用Visual C++实现的, 有建模、仿真和验证3种工作模式.第1种模式下, 用MSVL程序来描述系统并在平台中执行.系统的所有模型都会以范式图(normal form graph, 简称NFG)[16]的形式给出.如图 1(a)所示, NFG中的一条路径终止于双环节点.仿真类似于建模, 但是只输出NFG的一条路径, 即程序的一个模型.只要给出描述系统的MSVL程序和描述期望性质的PPTL公式, 平台就能自动验证系统是否满足性质.如果系统不满足性质, 还会给出反例路径.如图 1(b)所示, NFG中不满足性质的路径终止于终止节点; 而如图 1(c)中, NFG中满足性质的路径终止于圆节点.

Fig. 1 Three types of nodes 图 1 节点的3种类型

3 基于消息传递的通信

本节中, 我们为MSVL开发了一种消息传递的通信机制, 该机制的核心概念是通道、通信语句以及进程.

3.1 通道

通道的概念可以用来描述同步和异步通信[17].在同步通信中, 发送方通过通道发送消息后等待, 直到接收方接收消息.而异步通信中, 通道在通信实体之间起一个消息缓冲区的作用, 这样, 一个通信实体可以在不考虑其他通信实体的情况下发送或接收消息.

MSVL中, 消息传递的通信机制的非形式化描述如下:两个MSVL进程需要相互通信, 第1个进程是发送方而第2个是接收方.两个进程之间有一个通道, 该通道被视为一个消息缓冲区, 这是一个有界先入先出(first-in- first-out, 简称FIFO)队列.通道变量可以作为一个实参在两个进程间传输, 因此, 进程都可以通过访问它来进行通信.当发送方发送消息时, 它检查通道中是否至少有一个可用空间:如果是, 那么将信息附加到通道的队尾; 否则它可以等待, 直到有可用空间来发送消息, 或撤销发送操作.当接收方准备接收消息时, 它检查通道中是否存在至少有一条消息:如果是, 那么将该消息从通道队头移除; 否则它可以等待, 直到新消息进入通道, 或者撤消接收操作.

有界FIFO队列可以由一个列表来实现[18].受此思想启发, 我们定义了以下符号.

$ \begin{align} &|l|\triangleq \left( \begin{array}{*{35}{l}} 0, \text{ 如果 }l=\langle \rangle \\ n, \text{ 如果 }l=\langle {{l}_{1}}, ..., {{l}_{n}}\rangle , n\ge 1 \\ nil, \text{否则 } \\ \end{array} \right. \\ &head(l)\triangleq \left\{ \begin{array}{*{35}{l}} {{l}_{1}}, \text{ 如果 }l=\langle {{l}_{1}}, ..., {{l}_{n}}\rangle , n\ge 1 \\ nil, \text{否则 } \\ \end{array} \right. \\ &\text{ }tail(l)\triangleq \left\{ \begin{array}{*{35}{l}} \langle \rangle , \text{ 如果 }l=\langle {{l}_{1}}\rangle \\ \langle {{l}_{2}}, ..., {{l}_{n}}\rangle , \text{ 如果}l=\langle {{l}_{1}}, {{l}_{2}}, ..., {{l}_{n}}\rangle , n>1 \\ nil, ~~~~~~~~~~~~~~\text{ 否则 } \\ \end{array} \right. \\ \end{align} $

一个通道上的进程之间基于消息传递的通信如图 2所示.

Fig. 2 Channel structure 图 2 通道结构

通道c有maxlc大小的空间来存储发送方和接收方之间的消息.通信最多允许maxsc个发送进程${{P}_{1}}, ..., {{P}_{\max {{s}_{c}}}} $通过向通道c的队尾写入值来发送消息.另一方面, 最多允许maxrc个接收进程$ {{Q}_{1}}, ..., {{Q}_{\max {{r}_{c}}}} $通过head(c)从通道c的队头中读出值来接收消息.Lamport的面包店算法用于解决多个进程同时通过通道发送消息或接收消息时的互斥问题.面包店锁无死锁并满足互斥, 且有先到先得的特性:每个进程获取一个号码, 然后等待, 直到前面没有号码比自己小的进程试图进入临界区.如果这些进程读取相同的最大标签并选择了相同的标签, 那么进程ID小的将获得锁.通道的形式化定义如下:

$ \begin{align} &chn\text{ }c(n, s, r)\triangleq frame(c, sfla{{g}_{c}}, slabe{{l}_{c}})\wedge frame(rfla{{g}_{c}}, rlabe{{l}_{c}})\wedge c= \\ &\langle \rangle \wedge \underset{i=1}{\overset{s}{\mathop{\wedge }}}\, (sfla{{g}_{c}}[i]=0\wedge slabe{{l}_{c}}[i]=0)\wedge \\ &\underset{i=1}{\overset{r}{\mathop{\wedge }}}\, (rfla{{g}_{c}}[i]=0\wedge rlabe{{l}_{c}}[i]=0)\wedge \max {{l}_{c}}=n\wedge \max {{s}_{c}}=s\wedge \max {{r}_{c}}=r, \\ \end{align} $

其中, chnchannel的保留字, chn c(n, s, r)表示一个通道(即一个列表)名为c容量为n, 最多可以被s个发送方和r个接收方访问.这3个值分别被设置为3个静态变量maxlc, maxsc和maxrc.这里的c是框架变量.面包店算法中, ID为i的进程标志sflagc[i]是用来指示进程是否要进入临界区发送消息, 而slabelc[i]是整数, 用于指示进程进入临界区接收消息时的相对顺序.在初始状态, 所有进程的sflagcslabelc都设置为0.rflagcrlabelc在进程从通道接收消息时起类似的作用.

3.2 通信语句

为了判断一个进程的锁的状态, 定义了两个谓词如下.

●   isslocking(i, c)≜sflagc[i]=1;

●   isrlocking(i, c)≜rflagc[i]=1.

这里isslocking(i, c)表示ID为i的进程正在获取或已经获取通道c的发送锁, isrlocking(i, c)表示ID为i的进程正在获取或已经获取通道c的接收锁.

面包店算法发送和接收信息的锁形式化定义6条语句如下所示:

$ \begin{array}{l} slock(i, c) \buildrel \Delta \over = sfla{g_c}[i]: = 1 \wedge slabe{l_c}[i]: = \max (slabe{l_c}[1], ..., slabe{l_c}[\max {s_c}]) + 1;\\ await(\neg (\mathop \vee \limits_{j = 1}^{i - 1} (sfla{g_c}[j] = 1 \wedge slabe{l_c}[j] \Leftarrow slabe{l_c}[i]) \vee \\ \mathop \vee \limits_{j = i + 1}^{\max {s_c}} (sfla{g_c}[j] = 1 \wedge slabe{l_c}[j] < slabe{l_c}[i])))\\ tryslock(i, c) \buildrel \Delta \over = sfla{g_c}[i]: = 1;{\rm{ if }}\left( {\mathop \wedge \limits_{j = 1, j \ne i}^{\max {s_c}} (sfla{g_c}[j] = 0)} \right){\rm{ }}\\ {\rm{then }}\{ skip\} {\rm{ else }}\{ sfla{g_c}[i]: = 0\} \\ unslock(i, c) \buildrel \Delta \over = sfla{g_c}[i]: = 0;\\ rlock(i, c) \buildrel \Delta \over = rfla{g_c}[i]: = 1 \wedge rlabe{l_c}[i]: = \max (rlabe{l_c}[1], ..., rlabe{l_c}[\max {r_c}]) + 1;\\ {\rm{ }}await(\neg (\mathop \vee \limits_{j = 1}^{i - 1} (rfla{g_c}[j] = 1 \wedge rlabe{l_c}[j] \Leftarrow rlabe{l_c}[i]) \vee \\ \mathop \vee \limits_{j = i + 1}^{\max {r_c}} (rfla{g_c}[j] = 1 \wedge rlabe{l_c}[j] < rlabe{l_c}[i])))\\ tryrlock(i, c) \buildrel \Delta \over = rfla{g_c}[i]: = 1;{\rm{ if }}\left( {\mathop \wedge \limits_{j = 1, j \ne i}^{\max {r_c}} (rfla{g_c}[j] = 0)} \right){\rm{ then }}\{ skip\} {\rm{ else }}\{ rfla{g_c}[i]: = 0\} \\ unrlock(i, c) \buildrel \Delta \over = rfla{g_c}[i]: = 0. \end{array} $

每次ID为i的进程调用slock(i, c)为发送消息获取锁时, 将sflagc[i]置为1, 并生成一个比最大标签大1的slabelc[i], 这就确定该进程相对于其他尝试获取锁的进程的顺序.当多个发送进程同时执行slock时, 拥有最小标签的进程获得锁.如果这些进程读取到相同的最大标签并选择相同的标签, 那么进程ID最小的进程将获得锁.这种情况由slock中的await语句来定义.slock直到进程调用它获得锁后才会终止.进程发送消息后, 通过执行unslock来释放锁.相反, 如果没有其他进程尝试获取锁时, tryslock才会将sflagc置为0并获得发送锁; 否则, 将sflagc置为0并返回.谓词isslocking可用于判断通道的发送锁的状态:如果它为真, 那么进程能够发送消息; 否则, 进程需要再次调用tryslock对通道加锁.因此, 使用tryslockisslocking可以获取具有时间约束的锁, 而slock没有这种能力.当进程尝试从通道接收消息, rlock, tryrlock, isrlockingunrlock的用法同前面发送锁的语句一样.

获取通道的发送锁后, 如果通道未满, 发送方可以使用通信语句将消息发送到通道.同样, 在获得通道的接收锁后, 如果通道不为空, 那么接收方可以接收消息.为了判断通道的状态, 定义了两个谓词如下.

●   isfull(c)≜|c|=maxlc;

●   isempty(c)≜|c|=0.

isfull(c)在通道c为满时值为真, 否则为假; 而isempty(c)在通道c为空时值为真, 否则为假.

通信语句sendreceive对于同步和异步通信都适用:在前者中, 发送方必须要收到接收方发送到通道中的应答消息, 而后者并不需要.sendreceive定义如下.

●   send(c, x)≜awaitisfull(c)); c:=c·〈x〉;

●   recevie(c, y)≜awaitisempty(c)); y:=head(c)∧c:=tail(c).

send(c, x)语句将会阻塞直到通道c最终有空位为止.awaitisfull(c))在c未满时才会返回, 然后, x的值会在下一状态被附加到c的队尾.recevie(c, y)语句将会阻塞直到通道c最终有消息为止.awaitisempty(c))在c为非空是才会返回, 然后, 通道c队头的值会在下一状态被分配给y.如果谓词isfull在开始状态为假, send的区间长度至少为2.但是如果isfull总是为真, send将会一直阻塞, 区间长度无穷长.同样的, recevie的最小区间长度也是2, 区间长度在isempty总为真的情况下也是无穷长.

在分布式并发系统中, 当接收方在限定时间内没有接收到消息时, 它将放弃等待.发送方也有类似的情况.根据sendrecevie的定义, 它们的区间可能无限长, 所以它们不适合用于分布式并发系统的建模.因此, 定义另一对通信语句来处理超时机制, 如下:

●   put(c, x)≜if (¬isfull(c)) then {c:=c·〈x〉} else {skip};

●   get(c, y)≜if (¬isempty(c))then {y:=head(c)∧c:=tail(c)} else {skip}.

putget语句用if-else结构测试通道状态, 避免无限制时间的等待.如果当前状态isfull为真, put语句中的skip执行且put返回; 如果当前状态isempty为真, get语句中的skip执行且get返回.putget可以在限定时间内执行, 否则返回.这对通信语句适合用于具有时间约束的分布式并发系统的建模, 而另一对通信语句的发送和接收则容易应用于其他系统进行建模.

3.3 进程

通常来说, 进程可以用来描述对象的行为模式[19].在MSVL中, 进程被定义为一个复合谓词:

proc ProcName(fid, x1, …, xn)=ProcBody.

其中,

$ \begin{align} &ProcBody\triangleq int(x)|str(x)|list(x)|x\Leftarrow e|x:=e|\text{if }b\text{ then }{{P}_{1}}\text{ else }{{P}_{2}}| \\ &\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \text{while }b\text{ do }P|{{P}_{1}}\wedge {{P}_{2}}|{{P}_{1}}\vee {{P}_{2}}\text{ }|\bigcirc P|\square P| \\ &\text{ }empty|skip|len(n)|{{P}_{1}};{{P}_{2}}|\exists x:P|lbf(x)|frame(x)|{{P}_{1}}||{{P}_{2}}|({{p}_{1}}, ..., {{p}_{m}})\text{ }prj\text{ }q|await(b)| \\ &\text{ }chn\text{ }c(n, s, r)|slock(fid, c)|tryslock(fid, c)|send(c, e)|receive(c, y)|put(c, e)|get(c, y) \\ &ProcName(aid, {{y}_{1}}, ..., {{y}_{n}})\triangleq (aid, {{y}_{1}}, ..., {{y}_{n}}/fid, {{x}_{1}}, ..., {{x}_{n}})ProcBody. \\ \end{align} $

这里, ProcBody就是进程ProcName声明的主体.进程的结构由声明部分和调用部分组成.

●  声明部分proc ProcName(fid, x1, …, xn)=ProcBody包括进程名ProcName、形参列表fid, x1, …, xn以及进程主体ProcBody, 它是一个通常的MSVL的声明或通信语句.特殊地, 第一个形参fid是一个表示进程ID的自然数;

●  调用部分ProcName(aid, y1, …, yn)定义了一个进程的调用, 这是通过将进程主体ProcBody中的形参fid, x1, …, xn分别替换为实参aid, y1, …, yn得到的.

值得一提的是:除了一般的程序语句之外, 一个进程还可能涉及与其他进程通信的通信语句.通过互相通信的进程组合, 可以描述复杂的并发系统.

4 通信的实现机制

本节重点介绍在MSV平台中具有重要作用的通信语句的实现机制.为了以严格的方式对程序进行形式化验证和分析, 需要对通信语句进行归约.语句或程序的归约包括两个阶段:状态归约和区间归约[20].状态归约主要是指如何将程序转换成一个状态内的范式, 而区间归约则涉及程序从一种状态到另一种状态的执行.在MSVL中引入通信机制, 只需要考虑通信语句在状态归约时如何转换为范式, 区间归约与一般语句的处理相同.

定义1. MSVL程序q是范式, 如果:

$ q\triangleq \left( \underset{i=1}{\overset{k}{\mathop{\vee }}}\, {{q}_{ei}}\wedge empty \right)\vee \left( \underset{j=1}{\overset{h}{\mathop{\vee }}}\, {{q}_{cj}}\wedge \bigcirc {{q}_{fj}} \right), $

其中, k+h≥1, 且有以下规则:

(1) qeiqcj为true, 或形为p1∧…∧pm, pl(1≤lm)是type(x), 其中, xV, type∈{int, str, list}或x=e, 其中, eDπx或¬πx;

(2) qfj为内部程序, 即:一个变量可以引用前一种状态, 但不超过该程序当前执行区间的第1状态.

MSVL程序qk+h=1成立时是确定, 否则k+h > 1成立.我们将合取qeiemptyqcj∧Oqfj称为基本积:前者称为终止分量, 后者称为将来分量.此外, 我们将执行在当前状态下的qeiqcj称为当前部分, 执行于后继状态的Oqfj则称为将来部分.任何MSVL程序包括通信语句都能可以归约为一个逻辑等价的范式.

定理1.设P是扩展了类型声明和通信语句(如通道声明、加锁语句、通信语句、进程声明和调用)的MSVL程序.存在一个程序Q是范式, 使得PQ.

证明:通过对语句结构的归纳能得出证明.对于MSVL的无类型声明、通道声明、加锁语句、通信语句、进程声明和调用的证明可以在文献[16, 21]中找到.

整型声明int(x)的证明如下所示:

$ \begin{align} &int(x)\equiv int(x)\wedge (empty\vee \neg empty)\text{ }\ \ \ \ \ \ \ \ \ \ \ \ \ ~~~~(\text{i}) \\ &~~~~~~~~~~\equiv int(x)\wedge empty\vee int(x)\wedge \neg empty\ \ \ \ \ \ (\text{ii}) \\ &~~~~~~~~~~\equiv int(x)\wedge empty\vee int(x)\wedge \bigcirc \text{true}\ \ \ \ \ \ \ \ \text{ }(\text{iii}) \\ \end{align} $

上述证明过程中, 公式(ⅰ)遵从文献[20]中的T1、公式(ⅱ)文献[21]中的定理2.1、公式(ⅲ)以及empty的定义.另外两个类型声明str(x)和list(x)可以用相同的方法来证明.

通道声明chn、加锁语句slock, tryslock, unslock, rlock, tryrlockunrlock、通讯语句seng, recevie, putget都能根据它们的定义被重写为等价的MSVL语句, 然后转换为等价的范式.同样, 进程调用语句ProcName(aid, y1, …, yn)能被(aid, y1, …, yn/fid, x1, …, xn)ProcBody替代, 且能归约为等价的范式.

我们在MSV平台上实现了这些通信语句.考虑如下所示的实例程序:

$ \begin{align} &proc\text{ }p(id, c)=\{exists\text{ }x:\{frame(x)\text{ and }x=id+1\text{ and } \\ &(slock(id, c);send(*c, x);unslock(id, c))\}\}; \\ &proc\text{ }q(id, c)=\{exists\text{ }y:\{frame(y)\text{ and }y=id+3\text{ and} \\ &\text{ }(rlock(id, c);receive(*c, y);unrlock(id, c))\}\}; \\ &chn\text{ }c(1, 2, 2)\text{ and }(p(1, \And c)||p(2, \And c)||q(1, \And c)||q(2, \And c)). \\ \end{align} $

该程序说明了在容量为1的通道上两个发送方和两个接收方之间基于消息传递的通信.指针操作符 & 和*的定义在文献[22]中.该实例程序的MSVL代码及其执行结果如图 3所示.MSV平台执行实例程序并生成10个状态.这里省略了繁琐的归约过程, 结果如表 2所示.表中列出了每个状态上相关变量的值.首先, 进程p1p2都请求发送锁, 但是因为p1的进程ID比p2小, 所以p1获得发送锁并将x发送到通道c.同时, q1q2都请求接收锁, q1获得锁, 但是q1必须等待直到通道为非空.然后, q1接收p1的消息后在状态s3y设置为2.在p1释放发送锁后, p2获得发送锁, 并且在q1接收p1的消息并清空通道前等待发送消息.最后, q2获得接收锁并接收p2发送的消息.

Fig. 3 MSVL code of example program and its execution results 图 3 实例程序的MSVL代码和运行结果

Table 2 States of the program 表 2 程序的状态

5 多方电子合同签名协议的建模与验证

多方电子合同签名协议的目标是允许n个参与方通过网络来签署数字合同.该协议应该满足一些重要的性质, 比如公平性和乐观性[14].公平性确保协议中只有两种情况发生:要么所有参与方都收到签名的合同, 要么没有任何一方能收到签名的合同.实现公平性的一个简单方法是, 让可信的第三方(trusted third party, 简称TTP)参与该协议.TTP简单地收集各方的签名, 然后将它们分发给各方.由于TTP将参与所有各方的通信, 那么TTP很容易成为系统的瓶颈.这个缺点需要引入乐观性来解决:仅当存在参与方试图欺骗或网络发生不可恢复的异常的情况下才需要TTP参与仲裁.乐观的情况是:在没有TTP的介入下, 各方和通信网络的行为表现都是正确的.多方电子合同签名协议由两部分组成:主协议和恢复协议.由参与方执行的主协议在所有参与方之间有两轮通信.经证明:如果欺骗方少于所有参与方的一半, 则该协议至多需要两轮[14].如果没有欺骗方或网络异常, 则不涉及TTP所执行的恢复协议.协议细节描述如下.

1) 主协议

●  第1轮:

  Pi发送m[1, i]=signi(1, c)给其他参与方;

  Pi尝试从所有m[1, j]类型的消息生成向量M1=(m[1, 1], …, m[1, n]).如果成功且每个m[1, j]都是有效的签名, 那么Pi进入第2轮; 否则, Pi等待TTP发来消息;

●  第2轮

  Pi发送m[2, i]=signi(2, c)给其他参与方;

  Pi尝试从所有m[2, j]类型的消息生成向量M2=(m[2, 1], …, m[2, n]).如果成功且每个m[2, j]都是有效的签名, 那么Pi决定签署合同和并终止协议; 否则, Pi发送m[3, i]=signi(3, M1)给TTP并等待回复.

2) 恢复协议

●    TTP:如果TTP接收到至少一条消息m[3, i], 其中包含一个完整且连续的M1, 那么TTP会发送消息Mttp= signttp(M1)给所有参与方, 且每个收到该消息的Pi都会签署合同; 否则, TTP不发送任何消息.如果等待TTP应答消息的Pi没有接受到消息, 合同签署失败, 或者在接收Mttp后签署合同, 协议终止.

图 4所示, 我们讨论了同步网络中的合同签名协议.为了提高效率, 任何两个不同的参与方通过两个单向通道进行通信.当没有异常发生时, TTP不参与协议.不失一般性, 假定各方之间的所有消息都是简单的字符串.

Fig. 4 Protocol structure for three parti 图 4 3个参与方的协议结构

在第2轮中, 参与方可能不发送消息, 因为它不可信或网络不可靠.按第1轮中不发送消息的参与方数量, 协议中的参与方总共可分为4种情形.

●  情形1:第1轮中, 所有三方都向其他各方发送信息.进入第2轮后, 三方都可以向其他方各方发送或不发送消息, 总共有23=8个实例.但是, 所有三方最终都可以得到一份已签名的合同;

●  情形2:第1轮中, 所有三方中只有两个能发送信息.因此, 只有第3个参与方能获得所有消息并进入第2轮.根据恢复协议, 第3个参与方发送一个恢复请求给TTP, 然后, TTP广播已签名的合同, 所以所有三方都可以获得签名的合同.在发送恢复请求之前, 第3方可以选择发送消息或不发送消息, 因此有$ C_{3}^{2}\times 2=6 $个实例;

●  情形3:第1轮中, 只有一个参与方能发送消息, 因此有$ C_{3}^{1}=3$种情况.所有三方都不能计算M1, 所以不能进入第2轮; 那么所有的三方都等待TTP发来消息.由于没有一个参与方能进入第2轮并向TTP发出恢复信息, 因此TTP不会发送应答信息.三方均不能在限定时间内收到已签名的合同;

●  情形4:第1轮中, 所有三方都不能发送信息, 因此只有1个实例.像前一种情形一样, 没有参与方进入第2轮, 所有三方都没有收到已签名的合同.

经上述分析可知:该协议的算法在只有3个参与方和TTP的情况下, 一共有$ {{2}^{3}}+C_{3}^{2}\times 2+C_{3}^{1}+1=18 $种可能的执行路径, 即模型NFG路径数.

我们使用一个基于NFG的PPTL统一模型检测方法[8].统一模型检测方法首先用MSVL程序P对协议进行建模; 然后, 用PPTL公式Φ来描述每条关注的性质.在PTL逻辑框架下的MSV平台执行P并检查协议是否满足性质Φ.建模模式下, 扩展的MSV平台执行建模程序, 并生成如图 5所示的18条执行路径.仿真模式下, 输出18条路径其中一条的NFG.如图 5所示, 18条终止于圆节点的路径就是协议的模型.

Fig. 5 Modeling result of the protocol 图 5 协议的建模结果

在验证模式下, 我们需要用PPTL公式来描述公平性和乐观性.将程序以及这些性质输入到MSV平台, 然后输出验证结果.

●  公平性

  define a: sign1=“nil”;

  define b: sign2=“nil”;

  define c: sign3=“nil”;

  define d: sign1=“signed”;

  define e: sign2=“signed”;

  define f: sign3=“signed”;

  fin(a and b and c) or (d and e and f).

命题signi=“nil”表示第i个参与方没有获得签名的合同, 而signi=“signed”表示第i个参与方已经获得了签名的合同.公式fin(a and b and c) or (d and e and f)代表公平性, 即:所有三方都没有得到签名的合同, 或都获得签名的合同.图 6中, 有18个以圆节点结束的路径, 因此协议满足公平性.

Fig. 6 Verification result of the fairness property 图 6 公平性的验证结果

●  乐观性

  define a: comp1=1;

  define b: comp2=1;

  define c: comp3=1;

  define d: nottp=1;

  fin((a and b and c)→d).

命题compi=1表示第i个参与方已经进入了第2轮且获取了其他参与方的消息, 并成功计算出了向量M2.命题nottp=1表示TTP没有参与协议.公式fin((a and b and c)→d)表示乐观性, 它意味着如果所有三方都能够计算向量M2, 那么TTP将不参与最终的状态.图 7中, 有18个以圆节点结束的路径, 因此协议满足乐观性.

Fig. 7 Verification result of the optimism property 图 7 乐观性的验证结果

●  一个测试的性质

  define a: sign1=“signed”;

  define b: sign2=“signed”;

  define c: sign3=“signed”;

  fin(a and b and c).

命题signi=“signed”表示第i个参与方已经获得了签名的合同.而公式fin(a and b and c)代表的性质表示所有三方都能在最后一个状态获得签名的合同.根据前面情形分析, 在情形3和情形4下, 性质明显不满足.图 8中, 有4个反例, 4条路径的结束于终止节点, 所以该协议不满足此性质.

Fig. 8 Verification result of an unsatisfiable property 图 8 不满足性质的验证结果

以上分析都是基于只有3个参与方和TTP参与的情况, 在分析了4~6个参与方(存在TTP)之后, 我们可以得到如下的表 3图 9.

Table 3 Four different modeling situations 表 3 4种不同的建模情况

Fig. 9 Four different modeling and verification situations 图 9 4种不同建模和验证情况

根据图 9(a)可知:在有TTP参与的情况下, 模型的状态数与参与方数量n大致成指数关系.而在图 9(b)中, 根据3~6个参与方的可能执行路径数类推可得, n个参与方的模型NFG路径数Pathn

$ Pat{{h}_{n}}={{2}^{n}}+C_{n}^{n-1}\times 2+C_{n}^{n-2}+...+C_{n}^{2}+C_{n}^{1}+1. $

上式经化简计算可得:Pathn=2n+1+n-1.所以, 模型NFG路径数Pathn和参与方数量n呈指数关系.对于建模耗时, 由于建模与验证使用的是基于PPTL统一模型检测方法, 该方法基于PPTL的可满足性, 经粗略计算, 其时间复杂度为非基本时间.但如果模型中没有嵌套的¬(×; ×)结构, 那么算法的时间复杂度是指数级的.从图 9(c)中可以看出, 建模耗时和验证耗时大致符合这一规律.而验证相对于建模, 状态越多就要花费更多额外的时间, 显然也符合常理.

6 相关工作

目前, 大多数时序逻辑编程语言, 如前文提到过的METATEM, XYZ/E和Tempura, 也支持基于消息传递的通信机制, 用于描述并发和分布式系统中的通信, 但都存在一定的不足.METATEM代理之间通过广播或多播消息传递来相互通信, 且由于METATEM代理的组件互相独立, 所以对于同步和异步系统都适用[23].虽然从逻辑的角度来看这是个合理模型, 但这种方法代价大并且不适合表示非扁平化和结构化系统.XYZ/E中用一个变量表示通道, 这个通道被视为一次存储一条信息的单缓冲区, 基于消息传递的通信机制的实现依赖于两个通道:一个用于进程输出数据的写通道, 一个用于进程读入数据的读通道[10].这种方法虽然灵活, 但当一个通道同时被多个进程访问时, 就会产生冲突[15].而Tempura中通过引入一个带端口的流包来对并行进程之间的同步通信进行建模, 相关文献[11]中也给出了相应的通信语句和简单示例, 但具体的实现细节在文献中并没有提及.在经典进程代数中, 如CCS[24]、π-演算[25]和CSP[19], 只支持同步通信, 没有消息缓冲区或通道来连接通信代理, 但是异步通信可以通过在两个通信实体之间引入缓冲代理进行建模.本文实现的MSVL通信机制同样基于消息传递, 但是与上述方法不同, 采用先进先出队列表示通道, 引入面包店算法解决互斥问题, 并给出了通道结构、通信语句和进程结构的形式化定义, 适用于同步系统和异步系统的建模与验证.

7 结论

为了更好地对分布式并发系统进行建模与验证, 给MSVL增加了消息传递的通信机制, 给出了通信的形式化定义, 包括通道结构、面包店算法、通信语句和进程结构.通道被定义为一个存储消息的有界FIFO队列.面包店算法及通信语句用于对通道进行加锁及访问, 解决了互斥问题.进程定义为MSVL的组合语句, 用来描述系统的行为模式.研究了消息传递的通信机制在MSV平台中的实现机制.在MSV平台中, 对多方电子合同签名协议进行建模与验证, 表明该通信机制是有效的.验证了该协议的公平性与乐观性, 验证了一个不可满足的测试性质并给出了反例.将来的研究工作包括将具有通信机制的MSVL应用到更多实际的通信系统中, 如社交网络.

参考文献
[1]
Leeuwen JV. Handbook of Theoretical, Computer Science, Vol.B:Formal Models and Semantics. London: The MIT Press, 1994: 298-306. DOI:10.1016/0167-6423(95)90009-8
[2]
Baier C, Katoen J. Principles of Model Checking. London: The MIT Press, 2008.
[3]
Tian C, Duan ZH. Expressiveness of propositional projection temporal logic with star. Theoretical Computer Science, 2011, 412: 1729–1744. [doi:10.1016/j.tcs.2010.12.047]
[4]
Fisher M. An Introdution to Practical Formal Methods Using Temporal Logic. Wiley Publishing, 2011.
[5]
Wang M, Duan ZH, Tian C. Simulation and verification of the virtual memory management system with MSVL. In: Hou JL, Trappey AJC, eds. Proc. of the CSCWD 2014. Danvers: IEEE, 2014. 360-365. [doi:10.1109/cscwd.2014.6846870]
[6]
Zhang P, Duan ZH, Tian C. Simulation of CTCS-3 protocol with temporal logic programming. In: Shen WM, Li WD, eds. Proc. of the CSCWD 2013. Piscataway: IEEE, 2013. 72-77. [doi:10.1109/cscwd.2013.6580942]
[7]
Yu Y, Duan ZH, Tian C, Yang MF. Model checking C programs with MSVL. In: Liu SY, ed. Proc. of the SOFL 2012. LNCS 7787. London: Springer-Verlag, 2013. 87-103. [doi:10.1007/978-3-642-39277-1_7]
[8]
Duan ZH, Tian C. A unified model checking approach with projection temporal logic. In: Liu SY, Maibaum T, Araki K, eds. Proc. of the ICFEM 2008. LNCS 5256. London: Springer-Verlag, 2008. 167-186. [doi:10.1007/978-3-540-88194-0_12]
[9]
Scott ML. Programming Language Pragmatics. 3rd ed. San Francisco: Morgan Kaufmann Publishers, 2009. DOI:10.1016/b978-0-12-374514-9.x0001-8
[10]
Ma HD, Liu SQ. Multimedia data modeling based on temporal logic and XYZ system. Journal of Computer Science and Technology, 1999, 14(2): 188–193. [doi:10.1007/bf02946527]
[11]
Moszkowski B. Executing Temporal Logic Programs. New York: Cambridge University Press, 1986. DOI:10.1017/s0022481200029169
[12]
Lee EA. The problem with threads. IEEE Computer, 2006, 39(5): 33–42. [doi:10.1109/mc.2006.180]
[13]
Herlihy M, Shavit N. The Art of Multiprocessor Programming. San Francisco: Morgan Kaufmann Publishers, 2012. DOI:10.1145/1146381.1146382
[14]
Baum-Waidner B. Optimistic asynchronous multi-party contract signing with reduced number of rounds. In: Orejas F, Spirakis PG, Leeuwen JV, eds. Proc. of the ICALP 2001. LNCS 2076. London: Springer-Verlag, 2001. 898-911. [doi:10.1007/3-540-48224-5_73]
[15]
Mo DP, Wang XB, Duan ZH. Asynchronous communication in MSVL. In: Qin S, Qiu Z, eds. Proc. of the ICFEM 2011. LNCS 6991. London: Springer-Verlag, 2011. 82-97. [doi:10.1007/978-3-642-24559-6_8]
[16]
Duan ZH, Yang XX, Koutny M. Framed temporal logic programming. Science of Computer Programming, 2008, 70(1): 31–61. [doi:10.1016/j.scico.2007.09.001]
[17]
Charronbost B, Mattern F, Tel G. Synchronous, asynchronous, and causally ordered communication. Distributed Computing, 1996, 9(4): 173–191. [doi:10.1007/s004460050018]
[18]
Cormen T, Leiserson C, Rivest R. Introduction to Algorithms. 3rd ed. London: The MIT Press, 2009.
[19]
Hoare CAR. Communicating Sequential Processes. Upper Saddle River: Prentice-Hall, 1985. DOI:10.1007/978-3-662-09507-2_19
[20]
Yang XX, Duan ZH. Operational semantics of framed tempura. The Journal of Logic and Algebraic Programming, 2008, 78(1): 22–51. [doi:10.1016/j.jlap.2008.08.001]
[21]
Duan ZH. Temporal Logic and Temporal Logic Programming. Beijing: Science Press, 2006.
[22]
Luo L, Duan ZH, Tian C, Wang XB. A structural transformation from p-π to MSVL. Journal of Combinatorial Optimization, 2015, 29(1): 308–329. [doi:10.1007/s10878-014-9779-0]
[23]
Fisher M. MetateM: The story so far. In: Bordinni RH, ed. Proc. of the ProMAS 2005. LNAI 3862. London: Springer-Verlag, 2005. 3-22. [doi:10.1007/11678823_1]
[24]
Milner R. A Calculus of Communicating Systems. New York: Springer-Verlag, 1980. DOI:10.1007/3-540-10235-3
[25]
Milner R. Communicating and Mobile Systems:The π-calculus. New York: Cambridge University Press, 1999. DOI:10.1016/s0167-6423(00)00008-3