CSP是研究并发的重要理论及构建并发系统的经典方法^[1].随着CSP在分布式系统、网络安全协议方面的应用,对CSP的形式化验证显得尤为重要.目前,CSP验证主要采用两种方法:程序正确性证明和模型检测.其中,程序正确性证明^{[2, 3, 4]}能够解决并发系统无穷序列验证问题,但通常采用手工证明或者半自动化证明方式,且需领域专家参与.模型检测是一种自动的、基于模型、面向性质、用于有限状态系统的自动化验证技术,通过检测系统模型的所有可能状态,验证模型是否符合性质要求.当模型满足相应的性质时,输出满足;反之,则输出不满足,并提供相关反例,用于模型的精炼^[5].一般情况下,模型检测的对象是有限状态系统,但是基于不动点理论^[6]、Craig interpolation技术^[7]以及归纳原理^[8],可以对某些无穷状态系统进行验证.

传统的模型检测一般使用3种层次的系统模型:高层语言模型、语义模型和实现模型^[9].其中,

· 高层语言模型是一种高度抽象的形式化描述语言,可作为模型检测工具前端的描述语言,如Promela^[10],CSS^[11],CSP等;

· 语义模型是一种较为直观的形式化规范方式,可表示高层语言模型的含义,也可作为模型检测算法的输入模型,还可作为高层语言模型与实现模型间的中介模型,常见的语义模型,如Petri网模型^[12]、CSP的迹模型^[13]等;

· 实现模型用于模型验证算法的具体实施,分为显式和符号模型两种,其中,显式模型直接采用语义模型进行验证;符号模型是语义模型的一种隐式表示形式,具有较高的空间表示效率,如基于二叉决策图(BDD)、基于约束和基于表的模型检测,即是通过相应的符号模型进行验证的^{[14, 15, 16]}.

语言模型可通过操作语义或指称语义生成相应的实现模型.CSP发展过程中,Hoare提出了迹模型的概念,并指出了它的两方面用途:(1) 可为CSP语言提供清晰的、一致的定义;(2) 可通过迹模型完成性质验证^[13].现有CSP验证工具主要通过操作语义生成迹语义模型,如:FDR^{[17, 18]}通过操作语义将进程转化为相应的迁移系统,并依据迁移系统显式导出迹模型;ARC^[19]和PAT^[20]则是通过操作语义得到进程的BDD符号模型,然后依据符号模型导出相应的迹模型,并完成验证.基于操作语义的模型转化方法通常比较复杂,不易修改和扩展,且须领域专家的参与.与以上工作不同,本文提出了一种基于指称语义——关键迹模型的CSP验证方法,以关键迹模型为语义模型和实现模型,底层实现则采用ASP技术,实现策略简单、易于理解、可扩展性好.

通用模型检测采用时态逻辑(temporal logic)来描述待验证性质^{[21, 22, 23]},然而在现有多数CSP模型检测工具中,待验证性质和模型都采用进程形式进行描述,性质使用进程描述虽有助于模型精炼,但通用性不强,且对活性不能很好地描述.本文采用线性时态逻辑LTL来描述性质,可方便地对待验证性质进行描述,并通过可满足性求解技术对CSP模型进行验证.

模型检测技术面向应用的主要瓶颈是状态爆炸问题,目前存在多种解决途径,如偏序规约^{[24, 25]}、有界模型检测^[26]、模块化方法^[27].为缓解状态爆炸问题,CSP检测工具也采用了相应策略,如:SymFDR^[28]采用有界模型检测方法来缩减验证空间,并利用归纳的方法完成无界模型的验证;ARC通过BDD符号模型来降低存储空间; PAT则通过BDD符号模型和有界模型相结合的方法来解决状态爆炸问题.本文提出的关键迹模型是面向迹语义的抽象模型,与迹模型相比,其包含的数据量较小,一定程度上缓解了状态爆炸问题.

我们已对基于ASP的CSP模型检测技术进行了初步研究,如:文献^[29]提出了进程和性质的知识表示方法以及把性质验证归约为回答集求解的思想,但是,该验证体系对语义模型的解释不够明确,缺乏系统的验证方法,自动化程度不高;文献^[30]提出了基于进程迹的CSP模型验证框架,该方法明确了待验证的语义模型(迹模型),但是该模型规模庞大,包含大量冗余信息,增加了验证复杂度.鉴于上述问题,提出了CSP进程的关键迹模型,该模型只关注进程所发生的迹,减小了待验证语义模型规模,并利用ASP技术实现了关键迹模型自动化生成及基于关键迹模型的自动化验证,实现了CSP模型检测原型系统——T_ASP.

本文第1节介绍ASP和CSP.第2节给出关键迹模型及其递归计算方法,并论证基于关键迹模型验证的可靠性.第3节讨论如何自动生成关键迹模型,并提出基于迹的并发机制.第4节详述基于关键迹模型的LTL自动验证方法,介绍原型系统T_ASP的整体结构及其组件功能.第5节探讨哲学家就餐问题的CSP模型,并使用T_ASP验证模型性质.第6节分析相关研究工作.最后总结本文工作,指出后续的研究方向和策略.

1 基础知识 1.1 ASP编程

ASP是一种声明式程序设计(declarative programming)方法^[31],由稳定模型语义(stable model semantics)^[32]扩展而来.ASP作为新型程序设计方法有其独特的优点:(1) 编码紧凑、易理解;(2) 能够有效地对信息不完全问题进行刻画和计算;(3) 适合解决知识密集型、复杂计算问题;(4) 存在高效ASP求解器,可对问题自动求解^[33].经多次扩展,ASP具有强大的知识表示能力.下面介绍扩展析取逻辑程序的语法以及相应的ASP语义.

若A是一个原子,则A或~A称为文字,其中,A为正文字,~A为负文字,A和~A称为一对互补字.一个扩展析取逻辑程序P是一个规则集,且每条规则r满足如下形式:

\[{{L}_{1}}\vee \ldots \vee {{L}_{k}}\leftarrow {{L}_{k}}{{_{+}}_{1}},\ldots ,{{L}_{m}},not{{L}_{m}}{{_{+}}_{1}},\ldots ,not{{L}_{n}},\]

其中,n≥m≥k≥0,L_i是一个文字,not表示失败即否定(negation as failure).head(r)={L₁,…,L_k}表示r头部的文字集合,pos(r)={L₁,…,L_m}表示r体部的正文字集合,neg(r)={L_m+1,…,L_n}表示r体部的负文字集合.当头部为空时,称此r为约束规则.

Generate-and-Test^{[34, 35]}是ASP程序设计的经典方法,包括generate,define和test这3个模块.其中,generate模块由一组普通规则构成,可计算出问题的潜在解;test模块由一组约束规则构成,主要消除generate模块生成的无效解.对于复杂程序,generate和test模块并不能完全消除不合理的解,test可结合define模块解决这一问题. define模块通常由一组头原子为辅助谓词的规则组成.

本文ASP程序的书写规范采用DLV^[36]系统的相关规定(用:-代替-;每条规则以英文句号结束).例如,程序a-b,not c可表示为a:-b,not c.

1.2 CSP基础理论

CSP理论中,进程是描述客体的基本单位,进程间通过事件进行交互.设x是一个事件,P是一个进程,aP表示进程P的字母表,若x∈aP,则x→P表示一个进程,该进程首先执行事件x,然后按照进程P的行为进行.进 程的基本结构包括:前缀、递归、一般选择、非确定选择.

· 前缀:对于进程x→P,若P是可终止的或P=STOP(STOP表示空进程),则x→P属于前缀进程;

· 递归:X是不可终止进程,F(X)表示进程X的卫式,即,F(X)满足(a→X)形式,则X=F(X)属于递归进程,形式表示为mX.F(X).此类进程可表示无穷行为的客体;

· 一般选择:P.Q是两个进程,则P☐Q属于一般选择进程.P☐Q可选P行为,也可选Q行为,具体选择由环境控制.假设P:x→T,Q:y→S,若环境提供选择事件x,则选择P;若环境提供选择事件y ,则选择Q.a(P☐Q),满足:a(P☐Q)=aP=aQ;

· 非确定选择:P,Q是两个进程,则P∏Q属于非确定进程.P∏Q可选择P的行为,也可选择Q的行为,它的选择是任意的,不受外界控制.a(P∏Q)满足:a(P∏Q)=aP=aQ.

进程的并发方式是构造并发系统的核心.

假设有事件a,b,c,d,进程P,Q,且a∈(aP-aQ),b∈(aQ-aP),c,d∈(aQÇaP ),可以得到并发规则CR_csp.

· CR_csp-1: (c→P)||(c→Q)=(c→(P||Q));

· CR_csp-2: (c→P)||(d→Q)=STOP,若c≠d;

· CR_csp-3: (a→P)||(c→Q)=(a→(P||(c→Q));

· CR_csp-4: (c→P)||(b→Q)=(b→((c→P)||Q));

· CR_csp-5: (a→P)||(b→Q)=(a→(P||(b→Q))|b→((a→P)||Q)).

定义1. 一个CSP进程P可递归地定义为

\[P=STOP|x\to {{P}_{1}}|\mu {{P}_{2}}.F({{P}_{2}})|{{P}_{3}}☐{{P}_{4}}|{{P}_{3}}\Pi {{P}_{4}}|{{P}_{3}}||{{P}_{4}},\]

其中,进程P₁是可终止进程.

CSP存在多种指称语义模型,如迹模型(trace model)、失败/发散集模型(failure-divergence model),它们分别提供了进程的不同行为信息.本文主要讨论CSP的迹模型,该模型包含一系列迹,其中每条迹表示进程的一条行为序列,该序列由进程可执行的事件组成,并以事件发生的先后顺序进行排列.该模型显式地提供了进程的所有可能行为序列.为了自动验证的需要,本文只在有穷迹语义下对进程进行解释.

定义2(有穷迹语义)^[37]. 给定进程P,P的有穷迹语义是从语言模型CSP_M(P)到P的迹模型的一个函数.

定义3(迹模型)^[37]. 给定进程P,P的迹模型记为traces(P),traces(P)包含进程P所有可能的迹.

traces(P)的构建有两种途径:一是以递归方式由进程P所含组件进程的迹来计算traces(P);二是通过CSP的操作语义将进程转化为相应的迁移系统,进而提取进程的traces(P).文献^[37]已经证明这两种方法的等价性.本文采用递归求解方式来构造迹模型,下面给出基本结构进程的迹模型计算方式,复杂的CSP进程可递归地调用基本结构模型计算规则进行求解.

· 若进程P为STOP进程,则P的迹模型为

\[traces(STOP)=\{t|t=\left\langle {} \right\rangle \};\]

· 若进程P为P=a→STOP,则P的迹模型为

\[traces\left( P \right)=\{\left\langle {} \right\rangle \}\cup \{\left\langle a \right\rangle \};\]

· 若进程P为P=a→Q(其中,进程Q=a→…→STOP的形式),则P的迹模型为

\[traces(P)=\{\left\langle {} \right\rangle \}\cup \left\{ {{\left\langle a \right\rangle }^{\wedge }}t|t\in traces(Q) \right\}\left( \text{^是迹之间的连接算子} \right)\]

· 若进程P为P=a→…→b→P,设进程Q=a→…→b→STOP,进程Q的最长迹为q,q的所有子迹模型为sub_T,则P的迹模型为

\[\begin{align} & traces(P)=\left\{ \left\langle {} \right\rangle \right\}\cup \left\{ {{\left( {{q}^{\wedge }}\left\langle b,a \right\rangle \right)}^{n}} \right\} \\ & \cup \left\{ t|t={{r}^{\wedge }},r\in sub\_T,n=0,1,2,... \right\}; \\ \end{align}\]

· 若进程P为Q☐T,Q和T为前缀进程或递归进程,则进程P的迹模型为

\[traces(P)=\{q|q\in traces(Q)\}\cup \{t|t\in traces(Q)\};\]

· 若进程P为Q∏T,Q和T为前缀进程或递归进程,则进程P的迹模型为

\[traces(P)=\{q|q\in traces(Q)\}\cup \{t|t\in traces(Q)\};\]

· 若进程P为Q||T,Q和T为前缀进程或递归进程,则进程P的迹模型为

\[\begin{align} & traces(P||Q)=\{t|(t\uparrow \alpha P)\in traces(P)\wedge (t\uparrow \alpha Q) \\ & \in traces(Q)\wedge t\in {{(\alpha P\cup \alpha Q)}^{*}}\}. \\ \end{align}\]

其中,t↑aP表示t中属于aP的事件组成的新迹,(aP∪aQ)*表示字母aP∪aQ任意排列组成的迹集合.

2 关键迹模型

文献^[38]给出了评价语义模型的两个标准:一是语义模型能够很好地区分不同的程序;二是语义模型要尽可能地精简,摒弃无关信息.从模型检测角度看,语义模型的规模是主要的评价因素.迹模型为CSP进程提供了大量的可能行为,通常规模庞大,包含大量不影响性质验证结果的冗余信息.所以在CSP进程验证时,只关注有影响的关键迹是提高验证效率的有效途径.为此,下文首先构建一种新的模型——关键迹模型,该模型是迹模型的一个特殊子集,数据量远小于迹模型;然后论证基于关键迹模型验证的可靠性.

2.1 关键迹模型的定义

定义4(子迹). 设s,t分别为两条迹,若存在任意一条迹r,满足s^r=t(^是迹之间的连接算子),则称s是进程t的子迹,形式化地记为s∈prefix(t).

定义5(最长迹(max-trace)). s,t是进程P的任意两条迹,即s∈traces(P),t∈traces(P),若对于t∈traces(P),不存在s∈prefix(t),则s属于进程P的一条最长迹,形式化地记为Max-trace_P(s).

定义6(关键迹模型(critical-trace model)). 进程P的关键迹模型定义如下:

\[critical-traces\left( P \right)=\{s|s\in traces\left( P \right)\wedge \text{Max}-trac{{e}_{P}}\left( s \right)\}.\]

可见,进程的关键迹模型由迹模型中所有最长迹构成.下面给出基本进程关键迹模型的计算规则.

· 若进程P为STOP,则P的关键迹模型为

\[critical-traces(STOP)=\{t|t=\left\langle {} \right\rangle \};\]

· 若进程P为P=a→STOP,则P的关键迹模型为

\[critical-traces(STOP)=\{t|t=\left\langle {} \right\rangle \};\]

· 若进程P为P=a→Q,且进程Q=b→…→STOP,则P的关键迹模型为

\[critical-traces(P)=\left\{ {{\left\langle a \right\rangle }^{\wedge }}\left\langle {} \right\rangle \right\}=\left\{ \left\langle a \right\rangle \right\};\]

· 若进程P为P=a→…→b→P,设进程Q=a→…→b→STOP,则进程P的关键迹模型为

\[critical-traces(P)=\left\{ {{\left\langle a \right\rangle }^{\wedge }}t|t\in critical-traces(Q) \right\};\]

· 若进程P为QT,Q和T为前缀进程或递归进程,则P的关键迹模型为

\[critical-traces(P)=\left\{ s|s={{({{t}^{\wedge }}\left\langle b,a \right\rangle )}^{n}}\wedge t\in traces(Q),n=0,1,2,... \right\};\]

· 若进程P为QPT,Q和T为前缀进程或递归进程,则P的关键迹模型为

\[critical-traces\left( P \right)=\{q|q\in critical-traces\left( Q \right)\}\cup \{t|t\in critical-trace\left( T \right)\};\]

· 若进程P为Q||T,Q和T为前缀进程或递归进程,则P的关键迹模型为

\[\begin{align} & critical-traces(P)=\{t|(t\uparrow aQ)\in traces(Q) \\ & \wedge (t\uparrow aT)\in traces(T)\wedge t\in {{(aQ\cup aT)}^{*}} \\ & \wedge Max-trac{{e}_{P}}(t)\wedge t\in C{{R}_{csp}}(Q||T)\}. \\ \end{align}\]

其中,函数CR_csp(P)表示进程P符合CR_csp的迹的集合(当P不是并发进程时,CR_csp(P)表示P的最长迹的集合).可见,CR_csp(Q||T)表示进程Q和T并发时,符合CR_csp的迹的集合.

2.2 基于关键迹模型验证的可靠性

定义7(前缀封闭)^[1]. 给定进程P,s,t为两条迹,若s^t是P的一条迹,则s也为P的一条迹.

性质1^[1]. 给定进程P,traces(P)满足如下性质:(1) traces(P)是非空集合;(2) traces(P)是前缀封闭的.

定理1. 给定进程P,对于任意t∈traces(P),必存在唯一的迹s满足:t∈prefix(s)∧Max-trace_P(s).

证明:由定义6可得,critical-traces(P)⊂traces(P).

可知:对于任意的t∈traces(P),t∈critical-traces(P)或t∈traces(P)-critical-traces(P).

(1) 若t∈critical-traces(P),即,t满足Max-trace_P(t).由性质1可得:存在迹s∈traces(P),且s=t^r.由定义5可 知,traces(P)中的任何最长迹是唯一的,所以存在r= $\left\langle {} \right\rangle$,s=t;

(2) 若t∈traces(P)-critical-traces(P),即,t∈trace(P),t∉critical-traces(P).由性质1可得:存在迹s∈traces(P),s=t^r.由t不满足Max-trace_P(t),则一定存在迹r≠$\left\langle {} \right\rangle $满足(s=t^r)∧Max-trace_P(s).traces(P)中的最长迹是唯一的,所以r也是唯一的.

定理2. 给定进程P,t∈traces(P)且t是P所发生的迹,则t满足:

(1) t可由最长迹复合或并发生成;

(2) Max-trace_P(t).

证明:

1) 如果P不是并发进程,即P无需与其他进程交互.

(1) 若P为基本进程,则P将按照最长的行为序列一直进行,因此,P所发生的迹t一定满足:

Max-trace_P(t);

(2) 若P为由基本进程组成的复合进程,则P所发生的迹可由基本进程经过复合操作生成.基本进程所发生的迹是最长迹,且最长迹经过所有复合操作仍生成最长迹,故,P所有发生的迹也为最长迹;

2) 如果P为并发进程,设P=Q||R.

(1) 若Q,R为基本进程,假设t由r和s并发生成,即t=CR_csp(r||s),r∈traces(Q),s∈traces(R).由定理1可知:存在p∈traces(Q)∧r∈prefix(p)∧Max-trace_Q(p),q∈traces(R)∧s∈prefix(q)∧Max -trace_R(q).综上可得t=CR_csp(p||q).假设t=CR_csp(p||q)不满足Max-trace_P(t),即:存在迹w∈traces(P),t∈prefix(w),且满足Max-trace_P(w).如果w=CR_csp(u||v),则满足r∈prefix(u)∧u∈traces(Q),s∈prefix(v) ∧v∈ traces(R).由定理1可知:存在p∈traces(Q)∧u∈prefix(p)∧Max-trace_Q(p),q∈traces(R)∧v∈prefix(q)∧ Max-trace_R(q)满足w=CR_csp(p||q).由Max-trace_P(w)可知,CR_csp(p||q)生成的迹为最长迹.与已知矛盾,假设不成立.综上可得,t=CR_csp(p||q)满足Max-trace_P(t);

(2) 若进程Q或R是并发进程,则Q,R可以通过递归调用归结为基本进程的并发.通过情形(1)中类似方法容易证得t=CR_csp(p||q)满足Max-trace_P(t).

通过定理2可知:进程所发生的迹一定是最长迹,且这些迹一定可由相应子进程的最长迹生成.

基于迹模型进行性质判定时,需首先计算进程的迹模型,然后逐条判断每条迹是否符合CR_csp及是否满足相应性质要求.待验证性质采用LTL公式描述,其语法结构如下:

\[y::=p\in A|\neg \psi |{{\psi }_{1}}\wedge {{\psi }_{2}}|{{\psi }_{1}}\wedge {{\psi }_{2}}|G\psi |F\psi |X\psi .\]

简要起见,这里只采用G,F,X这3个时态算子,其中,G算子表示未来的所有状态,F算子表示未来的某一状态,X算子表示下一个状态.基于迹模型的LTL公式可满足如下语义定义:

定义8(基于迹模型的LTL公式可满足语义(traces(P)|=S_LTL)). 给定进程P和任意LTL公式S_LTL,π_t∈trace(P)

且π_t∈CR_csp(P),π_t满足S_LTL(记做π_t|=S_LTL)定义如下:

π_t|=p iff ∃i.p=π_t(i)

π_t|=¬p iff π_t|≠p

π_t|=Ψ₁∧Ψ₂ iff π_t|=Ψ₁且π_t|=Ψ₂

π_t|=Ψ₁∨Ψ₂ iff π_t|=Ψ₁或π_t|=Ψ₂

π_t|=XΨ iff π_t(2)|=y

π_t|=FΨ iff ∃i.π_t(i)|=Ψ

π_t|=GΨ iff π_t|=¬F¬Ψ

其中,π_t(i)表示进程迹π_t的第i个事件,π_t(i)=π_t(i)→π_t(i+1)→…是从π_t中删除前(i-1)个事件后所得到的子迹.如果对

任意π_t∈trace(P)且π_t∈CR_csp(P)均满足π_t|=S_LTL,则称P的迹模型满足S_LTL,记做traces(P)|=S_LTL.

性质2. 给定进程P,{t|t∈traces(P)∧Max-trace_P(t)}=critical-traces(P).

证明:由定义6可得上述性质.

定理3. 给定进程P、LTL公式S_LTL,traces(P)|=S_LTL当且仅当critical-traces(P)|=S_LTL.

证明:

(1) 充分性.

由性质2可得,critical-traces(P)={t|∀t∈traces(P)∧Max-trace_P(t)}.由此可得:

critical-traces(P)|=S_LTL⇔{t|=S_LTL|∀t∈trace(P)∧Max-trace_P(t)}.

由定理2可知,进程发生的迹t一定属于最长迹,即,t∈CR_csp(P)满足Max-trace_P(t).整理后得到:

{t|=S_LTL|∀t∈trace(P)∧t∈CR_csp(P)}.

通过定义8可得,traces(P)|=S_LTL.综上可得,critical-traces(P)|=S_LTL⇒traces(P)|=S_LTL.

(2) 必要性.

由定义8可知,traces(P)|=S_LTL,即{t|=S_LTL|∀t∈trace(P)∧t∈CR_csp(P)}.通过定理2可得,traces(P)|=S_LTL,即:

{t|=S_LTL|∀t∈trace(P)∧Max-trace_P(t)}.

由性质2可得,{t|=S_LTL|∀t∈trace(P)∧Max-trace_P(t)}⇒critical-traces(P)|=S_LTL.

综上可得:traces(P)|=S_LTL⇒critical-traces(P)|=S_LTL.

由定理3可知:对于LTL公式的验证而言,进程的关键迹模型和迹模型是等价的.

3 关键迹模型的自动生成方法 3.1 关键迹模型的生成框架

利用ASP技术实现关键迹模型的自动生成包括以下过程:(1) 知识的翻译,即,把CSP进程转化为对应的ASP规则;(2) 生成基本进程的关键迹模型,即,利用ASP构造基本进程到关键迹模型的生成规则;(3) 并发操作下关键迹模型的生成,即,利用ASP构造基于迹的并发规则,通过此规则生成并发系统的关键迹模型.本节主要讨论过程(2)和过程(3),分别对应ASP平台下关键迹模型生成机制的两个模块:基本进程和并发操作模块.基本进程模块包括前缀进程、递归进程、一般选择进程和非确定选择进程的生成规则.并发操作模块包括:(1) 选择模块,为基本进程模块中的选择进程提供相应的选择知识,从而实现自动生成关键迹模型;(2) 迹的并发规则库,该规则库与CR_csp有等价作用,已知两进程的关键迹模型,调用此规则库可生成其并发进程的关键迹模型.

为了更直观地描述上述设计,图1给出了关键迹模型的自动生成机制,其中,空心箭头表示数据的输入或输出,实线箭头表示数据流向,虚线箭头表示数据访问.下文框图约定与此相同,这里不再赘述.

3.2 基本进程关键迹模型的生成 3.2.1 进程和迹的ASP表示

为了刻画进程和迹,引入谓词flow(X,Y,P)表示在进程P的事件X比事件Y先发生,preset(P,Q)表示进程P是进程Q前缀式中所有事件组成的可终止进程(如Q=x→…→z→S,则P=x→…→z→STOP),invoking(P,Q)表示进程P的执行过程中将调用进程Q,repeat(P,Q)表示进程Q的行为由进程P的自调用形成.

例如:

· 进程Q的一条迹为<u,v,w,x,y,z>,可用ASP表示为

flow(u,v,q);

flow(v,w,q);

flow(w,x,q);

flow(x,y,q);

flow(y,z,q);

· 前缀进程P=w→x→y→z→STOP,可用ASP表示为

flow(w,x,q);

flow(x,y,q);

flow(y,z,q);

preset(q,p);

其中,q表示前缀式构成的可终止进程,p表示进程P;

· 递归进程P=w→x→y→z→P,可用ASP表示为

flow(w,x,q);

flow(x,y,q);

flow(y,z,q);

preset(q,p);

repeat(p,q).

一般选择进程的每条分支可采用前缀或递归进程的描述方法加以表示,此外,还需刻画不同分支形成的中间进程知识.引入谓词pre(X,Y,P)表示在进程P中先执行事件X,然后执行事件Y,isset(M,N)表示进程M是N的子进程,且M由N的若干前缀事件序列构成.aux_ invoking(P,Q)表示在进程P的执行过程中可能调用进程Q.

一般选择进程P=u→v→(w→x→y→STOPy→w→x→P),可用ASP表示为

· pre(u,v,p₁);

· pre(v,w,p₂);

· pre(w,x,p₂);

· pre(x,y,p₂);

· isset(p₁,p₂);

· preset(p₂,p);

· pre(v,y,p₃);

· pre(y,w,p₃);

· pre(w,x,p₃);

· isset(p₁,p₃);

· preset(p₃,p);

· aux_invoking(p₃,p).

非确定选择进程的知识刻画与一般选择进程相同,这里不再赘述.

为了生成进程的关键迹模型,引入辅助谓词event(X,P)表示事件X属于进程P,first(X,P)表示P进程前缀表示式的第1个事件是X,not_first(X,P)表示X不是P中第1个发生的事件,not_last(X,P)表示X不是P中最后发生的事件,pre_last(Y,P)表示事件Y是进程P的前缀式的最后一个事件.它可用ASP表示为

· event(X,P):-flow(Y,X,P);

· event(Y,P):-flow(Y,X,P);

· first(X,P):-not not-first(X,P),event(X,P);

· not_first(X,P):-flow(Y,X,P);

· not_last(X,P):-flow(X,Y,P);

· pre_last(Y,P):-not not_last(Y,P),event(X,P).

3.2.2 前缀进程的关键迹模型生成

前缀进程表示有限行为的客体,进程执行到前缀式的尾事件将正常终止.由于此类进程属于线性可终止结构,所以到关键迹模型的转化比较简单.引入last(X,P)表示X是进程P的最后一个事件,即X是P正常结束的标志.转化过程可用ASP表示为

last(Y,P):-flow(X,Y,P),pre_last(Y,P),not invoking(P,Q),not repeat(S,P).

3.2.3 递归进程的关键迹模型生成

递归进程表示无穷行为的客体,可视为前缀表示式基础上形成的循环进程.递归进程执行完前缀表示式的最后一个事件,将继续调用自身或其他进程.

· 若调用自身,可表示为

flow(X,Y,Q):-flow(X,Y,P),preset(P,Q);

flow(X,Y,Q):-pre_last(X,P),first(Y,P),not flow(X,Y,P),repeat(P,Q);

· 若调用其他进程,可表示为

flow(X,Y,Q):-flow(X,Y,P),invoking(Q,P);

flow(X,Y,Q):-invoking(Q,P),preset(R,P),preset(T,Q),pre_last(X,T),first(Y,R),not flow(X,Y,P).

3.2.4 一般选择进程的关键迹模型生成

一般选择进程到关键迹模型的转化需经过两个步骤:选择进程的路径以及处理正常终止或递归调用.下面引入谓词choice(X,N)表示选择N进程中的X事件,choice_p(N)表示进程N将被选择.下节中给出的选择机制可提供相应的选择知识——choice(X,N).一般选择进程的路径选择需经过以下3个步骤.

(1) 根据选择机制提供的选择知识,完成分支进程的选择,可表示为

flow(X,Y,N):-pre(X,Y,N),choice(Y,N);

(2) 已被选择的分支,其后续路径也将被选择,可表示为

flow(Y,Z,N):-flow(X,Y,N),pre(Y,Z,N);

(3) 当在选择结构中嵌套了选择结构时,需构造如下规则完成整个进程的选择:

choice_p(P):-choice(X,P);

flow(Y,Z,N):-flow(Y,Z,M),isset(M,N),choice_p(N).

执行上述3个步骤,进程将得到确定的路径.在路径的终端,进程或正常终止或递归调用.正常终止的处理方法与前缀进程相同.递归调用时,进程的处理方式与上文相同,但需先将递归调用的进程激活,可用ASP实现为

invoking(P,Q):-pre_last(X,P),aux_invoking(P,Q).

按照上述递归机制,进程可调用进程的任何分支,进程迹会产生多个环形路径,增加了性质验证复杂度.因此,建模时宜加强对模型的限定,如规定递归调用时,进程只调用已经选择的分支进程,该方式可表示为

repeat(P,Q):-pre_last(X,P),aux_repeat(P,Q).

3.2.5 非确定选择进程的关键迹模型生成

与一般选择进程不同,非确定选择进程的路径选择由进程内部完成,而内部选择方式可以是随机选择,也可人为制定.简化起见,采用不确定问题确定化的方法处理路径选择问题,其基本思想是:把非确定选择进程任意随机选择得到的模型作为确定性模型的子模型,合并所有子模型,并用确定性模型代替非确定模型.显而易见,非确定性模型的行为一定包含在确定性模型中,这保证了模型验证的可靠性.引入谓词un_choice(X,P)表示进程P的事件X是非确定进程的一个随机选择方式,则相应的选择知识un_choice(X,P) v…v choice(Y,M)可由进程 自身提供,具体过程由第4.4节给出的翻译程序1中实现.

非确定选择进程到关键迹模型的转化与一般选择进程类似,也需经过上述两个步骤.当运用非确定选择来描述进程时,主要采用两种形式:包含非确定选择嵌套的方式和不包含非确定选择嵌套的方式.

· 如果进程描述采用不包含非确定选择嵌套的形式,则关键迹模型的生成过程可表示为

flow(X,Y,N):-pre(X,Y,N),choice(X,N);

flow(Y,Z,N):-flow(X,Y,N),pre(Y,Z,N);

repeat(P,Q):-pre_last(X,P),aux_repeat(P,Q).

· 如果进程描述采用包含非确定选择嵌套的方式,其生成过程可表示为

choice(X,N):-undefined_choice(Y,M),undefined_choice(X,N),isset(M,N);

choice(Y,M):-undefined_choice(Y,M),undefined_choice(X,N),isset(M,N);

flow(X,Y,N):-pre(X,Y,N),choice(X,N);

flow(Y,Z,N):-flow(X,Y,N),pre(Y,Z,N);

choice_p(P):-choice(X,P),choice(Y,Q),isset(P,Q);

choice_p(Q):-choice(X,P),choice(Y,Q),isset(P,Q);

flow(Y,Z,N):-flow(Y,Z,M),isset(M,N),choice_p(N);

repeat(P,Q):-pre_last(X,P),aux_repeat(P,Q).

3.3 并发操作下关键迹模型的生成 3.3.1 选择机制的ASP实现

为构建选择机制,引入辅助谓词aux_p(P,Q),aux_c(P,Q),process(Q),small(P),nsmall(P),auxn_first(X,P),auxfirst(X,P),其中,aux_p(P,Q)表示进程P是进程Q的子进程,aux_c(P,Q)表示进程P与进程Q进行并发,process(Q)表示Q为一个进程,small(P)表示进程P为不含子进程的进程,auxfirst(X,P)表示X是子进程P的首事件.利用上述谓词构造如下辅助规则:

· aux_p(P,Q):-preset(P,Q);

· aux_p(O,Q):-aux_p(P,Q),isset(O,P);

· event(X,P):-pre(X,Y,P);

· event(Y,P):-pre(X,Y,P);

· event(X,Q):-event(X,P),aux_p(P,Q);

· process(P):-isset(P,Q);

· process(Q):-isset(P,Q);

· auxn_first(X,P):-pre(Y,X,P);

· small(P):-not nsmall(P),process(P);

· auxfirst(X,P):-not auxn_first(X,P),event(X,P);

· nsmall(Q):-isset(P,Q);

· aux_choice(X,N,Y,M):-pre(T,X,N),pre(T,Y,M),auxfirst(T,N),auxfirst(T,M),s_layer(N,M).

选择机制通过并发环境对路径进行选择,因而只能为一般选择进程提供相应的选择知识.设进程P是一般选择进程,Q为任意进程,P和Q并发时,P的选择方式分为3种情况.

(1) P有一条分支路径由P与Q的共有事件构成,并由此生成相应的选择知识,可用ASP表示为

choice(Y,M):-aux_choice(X,N,Y,M),small(N),small(M),aux_p(N,P),aux_p(M,P),aux_c(P,Q),event(Y,Q),not event(X,Q),X!=Y,N!=M;

choice(Y,M):-choice(Z,R),aux_choice(X,N,Y,M),isset(R,N),isset(R,M),aux_p(N,P),aux_p(M,P),aux_c(P,Q),event(Y,Q),not event(X,Q),X!=Y,N!=M;

choice(X,N):-choice(Z,R),aux_choice(X,N,Y,M),isset(R,N),isset(R,M),aux_p(N,P),aux_p(M,P),aux_c(P,Q),not event(Y,Q),event(X,Q),X!=Y,N!=M;

(2) P的所有分支都是私有事件,无需Q的参与.路径的选择由内部提供,可用ASP表示为

choice(X,N) v choice(Y,M):-aux_choice(X,N,Y,M),small(N),small(M),aux_p(N,P),aux_c(P,Q),not event(Y,Q),not event(X,Q),X!=Y,N!=M;

choice(X,N) v choice(Y,M):-choice(Z,R),aux_choice(X,N,Y,M),isset(R,N),isset(R,M),aux_p(N,P),aux_p(M,P),aux_c(P,Q),not event(Y,Q),not event(X,Q),X!=Y,N!=M;

(3) P的多条分支都由P与Q的共有事件构成,每个分支都需Q的参与.此时,环境提供了多条路径选择,也转化为非确定选择,可用ASP表示为

choice(Y,N) v choice(Z,M):-pre(X,Y,N),pre(X,Z,M),aux_p(N,P),aux_p(M,P),aux_c(P,Q),event(Y,Q),event(X,Q),N!=M;

alic>(Y,M):-choice(Z,R),aux_choice(X,N,Y,M),isset(R,N),isset(R,M),aux_p(N,Q),aux_p(M,Q),aux_c(P,Q),event(Y,P),event(X,P),X!=Y,N!=M.

3.3.2 CSP的并发机制与基于进程迹的并发机制

进程并发时,最重要的任务是调用CR_csp生成进程所发生的迹.CR_csp提供了抽象的并发方式,可简洁地显示出进程的并发状况.但其不足之处是:只关注当前的并发事件,而后续的并发仍采用抽象方式描述,为了得到语义模型,需要频繁地调用CR_csp,在语言模型和语义模型间加以转换.为此,提出一种基于迹的并发机制.

为了构建基于迹的并发规则,需关注两方面问题:(1) CR_csp的并发思想;(2) 迹并发的基本结构.其中,CR_csp的总体思想是:共同事件共同参与,私有事件随机发生.迹并发的基本结构将在下节给出.在构建此种并发规则时,先确定迹并发的基本结构,然后确定该结构遵循的CR_csp的并发思想,进而设计相应的并发规则.

图2给出了CR_csp与基于迹的并发规则之间的关系.可见,基于迹的并发规则与CR_csp的作用是等价的.与之不同,基于迹的并发规则只在语义模型上计算,通过规则的匹配生成新进程的迹.该并发方式无需步步进行递归调用,因而可避免生成大量中间变量.此外,充分地利用已生成的关键迹模型,提高了知识重用.

3.3.3 基于迹的并发规则

进程并发时,需特别考虑以下情况:参与并发的两个进程,一个已经发生了若干事件,另一个还处于初始事件.为了准确定位将要参与并发的事件,需对参与并发的进程的事件流进行标记.

为此,引入谓词initial_flow(X,Y,P)表示当前参与并发的事件流为flow(X,Y,P),next_flow(X,Y,P)表示参与并发的下一事件流为flow(X,Y,P).并发事件的定位方法是:首先标记两进程初始参与并发的事件,发生事件的进程的标记后移一位,另一进程标记不变.事件的定位策略可用ASP如下表示:

· initial_flow(X,Y,P):-flow(X,Y,P),first(X,P);

· next_flow(Y,Z,P):-initial_flow(X,Y,P),flow(X,Y,P),flow(Y,Z,P);

· initial_flow(Y,Z,P):-initial_flow(X,Y,P),next_flow(Y,Z,P),flow(X,Y,T),concurrent(P,Q,T).

为了等价地实现CR_csp的并发功能,本节给出了迹并发结构的最小完备集,共10种基本结构.进程的所有并发情况都可归纳为这10种基本结构.下面分3组情况分别来定义并发规则.

1. 图3给出了第1组基本结构,该结构需遵循规则CR_csp-1和CR_csp-2,可用ASP表示为

flow(X,Y,T):-initial_flow(X,Y,P),initial_flow(X,Y,Q),not fail_flow(X,Y,P),not fail_flow(X,Y,Q),event(X,P),

event(Y,P),event(X,Q),event(Y,Q),concurrent(P,Q,T);

:-initial_flow(X,Y,P),initial_flow(X,Z,Q),not fail_flow(X,Y,P),not fail_flow(X,Z,Q),

event(X,P),event(Y,P),event(X,Q),event(Y,Q),event(Z,P),concurrent(P,Q,T);

:-initial_flow(X,_,P),initial_flow(Y,_,Q),not fail_flow(X,_,P),not fail_flow(Y,_,Q),event(X,P),

event(Y,P),event(X,Q),event(Y,Q),concurrent(P,Q,T).

其中,谓词fail_flow(X,Y,P)表示事件流flow(X,Y,P)已经失效,可生成辅助规则:

fail_flow(X,Y,P):-flow(X,Y,T),concurrent(P,Q,T).

2. 图4给出了第2组基本结构,共包含4种形式.其中,形式(1)、形式(2)和形式(4)都需遵循规则CR_csp-1~ CR_csp-4,形式(3)需遵循CR_csp-3和CR_csp-4.下面分别加以描述.

· 图4-(1)可用ASP表示为

flow(X,Y,T):-initial_flow(X,Y,P),initial_flow(X,Z,Q),not fail_flow(X,Y,P),not fail_flow(X,Z,Q),event(Y,Q),not event(Z,P),concurrent(P,Q,T);

:-initial_flow(X,Y,P),initial_flow(Z,R,Q),not fail_flow(X,Y,P),not fail_flow(X,Y,Q),event(X,Q),event(Z,P),event(Y,Q),not event(R,P),concurrent(P,Q,T);

· 图4-(2)可用ASP表示为

flow(X,Y,T):-initial_flow(X,Y,P),initial_flow(Y,Z,Q),not fail_flow(X,Y,P),not fail_flow(Y,Z,Q),not event(X,Q),event(Y,P),event(Z,P),concurrent(P,Q,T);

:-initial_flow(X,Y,P),initial_flow(R,Z,Q),not fail_flow(X,Y,P),not fail_flow(R,Z,Q),not event(X,Q),event(Y,Q),event(R,P),event(Z,P),Q≠Y,concurrent(P,Q,T);

· 图4-(3)可用ASP表示为

flow(Y,Z,T):-initial_flow(X,R,P),initial_flow(Y,Z,Q),not fail_flow(X,R,P),not fail_flow(Y,Z,Q),event(X,Q), event(R,Q),not event(Y,P),not event(Z,P),concurrent(P,Q,T);

· 图4-(4)可用ASP表示为

flow(X,Y,T):-initial_flow(X,Y,P),initial_flow(Y,Z,Q),not fail_flow(X,Y,P),not fail_flow(Y,Z,Q),not event(X,Q),event(Y,P),not event(Z,P),concurrent(P,Q,T);

:-initial_flow(X,Y,P),initial_flow(R,Z,Q),not fail_flow(X,Y,P),not fail_flow(R,Z,Q),not event(X,Q),event(Y,Q),event(R,P),not event(Z,P),Q≠Y,concurrent(P,Q,T).

3. 图5给出了第3组基本结构,共包含5种形式.

图5-(1)可用ASP表示为

flow(X,Y,T) v flow(X,Y,T):-initial_flow(X,Y,P),initial_flow(X,Z,Q),not fail_flow(X,Y,P),not fail_flow(X,Z,Q),

not event(Y,Q),not event(Z,P),concurrent(P,Q,T);

:-initial_flow(X,Y,P),initial_flow(R,Z,Q),not fail_flow(X,Y,P),not fail_flow(R,Z,Q),

event(X,Q),not event(Y,Q),not event(Z,P),concurrent(P,Q,T);

图5-(2)可用ASP表示为

flow(X,Y,T) v flow(Y,X,T):-initial_flow(X,Z,P),initial_flow(Y,Z,Q),not fail_flow(X,Z,P),not fail_flow(Y,Z,Q),

not event(X,Q),not event(Y,P),concurrent(P,Q,T);

图5-(3)可用ASP表示为

flow(X,Y,T) v flow(Y,X,T) v flow(Y,X,T):-initial_flow(X,R,P),initial_flow(Y,Z,Q),not fail_flow(X,R,P),

not fail_flow(Y,Z,Q),not event(X,Q),not event(Y,P),event(R,P),

not event(Z,P),concurrent(P,Q,T);

图5-(4)可用ASP表示为

flow(X,Y,T) v flow(Y,X,T) v flow(Z,X,T) v flow(X,Z,T):-initial_flow(X,Y,P),initial_flow(Z,R,Q),not fail_flow(X,R,P),

not fail_flow(Y,Z,Q),not event(X,Q),not event(Y,Q),

not event(R,P),not event(Z,P),concurrent(P,Q,T);

图5-(5)可用ASP表示为

flow(R,Z,T):-initial_flow(X,Y,P),initial_flow(R,Z,Q),not fail_flow(X,Y,P),not fail_flow(R,Z,Q),event(X,Q),

not event(Y,Q),not event(R,P),not event(Z,P),concurrent(P,Q,T).

4 基于关键迹模型的自动化验证 4.1 ASP框架下LTL验证的基本思想

通过关键迹模型的生成机制,可将并发系统CSP模型转化为相应的关键迹模型,且每条回答集对应于关键迹中的一条迹.因此,通过验证回答集是否满足某性质,即可确定相应并发系统是否满足该性质.验证的基本思想是:当要验证一个模型是否满足性质Ψ时,先对性质取反(即¬Ψ),接着构造性质变换目标程序∏_ans(¬Ψ),然后调用求解器验证模型是否满足¬Ψ:若无回答集,则说明该模型满足性质Ψ;若存在回答集,则说明该模型不满足性质Ψ,且相应的回答集为不满足的反例.验证流程如图6所示.

4.2 回答集模型下LTL的可满足性语义

ASP框架下得到的回答集与待验证进程关键迹模型中的迹是一一对应的,故可把关键迹模型下的可满足性语义归结为回答集模型下的可满足性语义.下面定义基于回答集模型的LTL可满足性语义.

定义9. 给定待验证进程Q,M_ans是与critical-traces(Q)对应的回答集的集合,LTL公式在回答集π_ans∈M_ans下的可满足性定义为

π_ans|=p iff ∃X.flow(X,p,Q)∈π_ans∨flow(p,X,Q)∈π_ans

π_ans|=¬p iff π_ans|≠p

π_ans|=Ψ₁∧Ψ₂ iff π_ans|=Ψ₁且π_ans|=Ψ₂

π_ans|=Ψ₁∨Ψ₂ iff π_ans|=Ψ₁或π_ans|=Ψ₂

π_ans|=FΨ iff ∃X.π_ans(X)|=Ψ

π_ans|=XΨ iff first(X,Q)∧flow(X,Y,Q)∈π_ans∧π_ans(Y)|=Ψ

π_ans|=GΨ iff _ans π_ans|=¬F¬Ψ

其中,p,y,y₁,y₂的含义与定义8中相同,集合π_ans(X)的构造如下:若存在事件X,Y满足flow(X,Y,Q)∈π_ans,则π_ans(X)={flow(X,Y,Q)}∨π_ans(Y);若不存在事件X,Y满足flow(X,Y,Q)∈π_ans,则π_ans(X)=∅.如果对任意π_ans∈M_ans均满足π_ans|=S_LTL,则称回答集模型满足公式y,记作M_ans|=S_LTL.

4.3 性质变换目标程序∏_ans(¬Ψ)

为了构建性质y的目标程序∏_ans(¬Ψ),需用ASP刻画基于回答集模型的LTL可满足语义.由关键迹模型的生成机制可知,回答集与关键迹模型中的迹有一一对应关系.关键迹模型的迹包含下面两种结构:带环的递归结构和不带环的前缀结构,如图7所示.因此,回答集也只包含这两种结构,即,系统提供的反例包含这两种情形.

为了刻画基于回答集模型的LTL可满足语义,还需引入辅助谓词le,el(X,T),nl(X,Y,T),bel(X,Y,T).其中,le表示迹中存在环结构,el(X,T)表示事件X是进程T中环形路径的入口,nl(X,Y,T)表示flow(X,Y,T)是前缀表示式末端到前缀中某一原子的流关系,bel(X,Y,T)表示flow(X,Y,T)属于环形路经中的一个流关系.

当回答集中包含一个环时,可用ASP规则表示为el(X,T):-flow(Y,X,T),flow(Z,X,T).

辅助谓词间的相互关系可用ASP表示为

· le:-el(X,T);

· nl(X,Y,T):-flow(X,Y,T),el(Y,T);

· bel(X,Y,T):-el(X,T),flow(X,Y,T);

· bel(Y,Z,T):-flow(X,Y,T),bel(Y,Z,T).

依据上述辅助规则,LTL可满足语义的转化结果见表1,其中,pl(X,T)表示X是待验证进程T发生的事件.

通过表1,可构建性质变换目标程序∏_ans(¬Ψ),进而把性质验证归结为回答集求解.∏_ans(¬Ψ)的构建过程如下:对所有待验证的LTL公式Ψ取反,为¬Ψ;然后,由外向内分析¬Ψ的基本结构;最后,递归调用表1中的相应规则,即可得到目标程序∏_ans(¬Ψ).下面举例说明.

给定待验证进程P及LTL公式h=F1.up∧F2.up∧F3.up,其中,1.up,2.up和3.up是进程P的原子事件.构建步骤如下:

(1) 取反,设f=¬h=G¬1.up∨G¬2.up∨G¬3.up;

(2) 由外向内分析f,设f=f₁∨f₂∨f₃,f₁=G¬1.up,f₂=G¬2.up,f₃=G¬3.up,t₁=¬1.up,s₁=¬2.up,r₁=¬3.up;

(3) 依上面(2)中的结构调用表1,可得如下目标程序:

· f:-f₁;

· f:-f₂;

· f:-f₃;

· f₁:-le,not q;

· q:-t₂(X,Y,T);

· t₂(X,Y,T):-not t₁(X,Y,T),flow(X,Y,T);

· t₁(X,Y,T):-not t₃(X,Y,T);

· t₃(X,Y,T):-flow(X,Y,T),pl(X,T);

· pl(1.up,p);

· f₂:-le,not p;

· p:-s₂(X,Y,T);

· s₂(X,Y,T):-not s₁(X,Y,T),flow(X,Y,T);

· s₁(X,Y,T):-not s₃(X,Y,T);

· s₃(X,Y,T):-flow(X,Y,T),pl(X,T);

· f₃:-le,not o;

· o:-r₂(X,Y,T);

· r₂(X,Y,T):-not r₁(X,Y,T),flow(X,Y,T);

· r₁(X,Y,T):-not r₃(X,Y,T);

· r₃(X,Y,T):-flow(X,Y,T),pl(X,T);

· pl(2.up,p);

· pl(3.up,p).

其中,p表示进程P.

4.4 CSP模型检测原型系统——T_ASP

T_ASP系统的结构如图8所示,其输入为CSP模型和LTL公式:CSP模型用来描述并发系统;LTL公式用来表示待验证性质,由用户提供.性质可满足时,系统输出Yes;性质不满足时,输出No+反例集CE.

T_ASP主要含有两大核心组件:关键迹模型自动生成机制和LTL的自动验证机制,其中,

· 关键迹模型生成机制包括基本进程转化规则库、选择机制规则库以及迹的并发规则库,具体结构如图1所示;

· LTL的自动验证机制包括基于迹结构的辅助规则、LTL可满足语义规则库以及构建性质变换目标程序π_ans(LTL),具体结构如图6所示.

此外,T_ASP还包含辅助组件翻译程序1和翻译程序2,它们为相应的输入提供接口.

· 翻译程序1的任务是:对CSP进程进行编译,将其转化为ASP求解器可以识别的进程知识.其基本思想是:先将CSP模型转化为进程并发树CTP(CTP中包含一棵主树CTP_Host、若干棵子树CTP_Sub);然后,逐个分析CTP_Host的所有节点,并生成相应的知识,具体算法如图9所示,该算法所调用的函数ConcurTree_ofProcesses(CSP_M,P)如图10所示;

· 翻译程序2的作用为:将LTL公式y取反,从外向内依次匹配可满足语义规则(即表1),生成性质变换目标程序∏_ans(¬Ψ).其基本思想是:递归地分析LTL公式的具体结构,并构造出相应的基本结构库;然后,根据这些基本结构和可满足语义规则库生成相应的∏_ans(¬Ψ).具体算法如图11所示,其调用的函数RecurAnaly(Unit_y)如图12所示.

5 实 验 5.1 哲学家就餐问题的CSP模型

为对不同进程算子进行实验,分别采用3种方法构造该问题.

· 第1种方法采用递归技术,具体描述如下:

\[\begin{align} & P{{h}_{i}}=i.sit\to i.pick\_fork.i\to i.pick\_fork.i \\ & \oplus 1\to i.down\_fork.i\to i.down\_fork.i\oplus 1 \\ & \to i.up\to P{{h}_{i}} \\ \end{align}\]

(i)

该方法对哲学家Phi的要求比较严格,其行为满足:先坐下来,拿起左边叉子,再拿右边的叉子,接着进餐完毕;然后放下左边叉子,再放右边叉子,最后离开座位.如此反复.

叉子进程:要么被左边的哲学家拿起,然后放下;要么被右边的科学家拿起,然后放下.可描述为

\[\begin{align} & Fork.i=(i.pick.fork.i\to i.down.fork.i\to \\ & Fork.i☐ i⊖1.pick.fork.i\to i⊖1.down.fork.i \\ & \to Fork.i) \\ \end{align}\]

(ii)

· 第2种方法采用一般选择及其嵌套方式进行描述,具体描述如下:

Phi=i.sit→(i.pick_fork.i→i.pick_fork.i⊕1→(i.down_fork.i→i.down_fork.i⊕1→i.up→Phic☐i.down_fork.i ⊕1→i.down_fork.i→i.up→Phic)☐i.pick_fork.i⊕1→i.pick_fork.i→(i.down_fork.i→ i.down_fork.i⊕1→i.up→Phic☐i.down_fork.i⊕1→i.down_fork.i→i.up→Phic))

(iii)

与进程(i)不同,哲学家进程开始时,对于拿起或放下叉子的左、右顺序不作限制,当选定某一方式后,哲学家

按照已经选择的方式进行.每条分支最后调用的Ph_ic与Ph_i被选择的路径有关,表示由Ph_i被选择的路径形成的

自递归进程.例如:

若Ph_i满足选择机制的分支是i.sit→i.pick_fork.i→i.pick_fork.i⊕1→i.down_fork.i→i.down_fork.i⊕1→i.up,

那么Ph_ic=i.sit→i.pick_fork.i→i.pick_fork.i⊕1→i.down_fork.i→i.down_fork.i⊕1→i.up→Ph_ic

该哲学家进程分支的选择由与其交互的其他哲学家进程或者叉子进程提供.

叉子进程的CSP描述与进程(ii)相同.

· 第3种方法采用非确定选择及其嵌套进行描述,具体描述如下:

Phi=i.sit→(i.pick_fork.i→i.pick_fork.i⊕1→(i.down_fork.i→i.down_fork.i⊕1→i.up→Phic)∏(i.down_fork.i ⊕1→i.down_fork.i→i.up→Phic)∏(i.pick_fork.i⊕1→i.pick_fork.i→(i.down_fork.i→ i.down_fork.i⊕1→ i.up→Phic)∏(i.down_fork.i⊕1→i.down_fork.i→i.up→Phic))

(iv)

进程(iii)与进程(ii)的含义基本相同,Ph_ic的定义也与进程(ii)相同;不同点在于:进程(ii)的选择由其他哲学

家或叉子提供,进程(iii)的选择由自身提供.且进程(iii)通过规则x→(P∏Q)=(x→P)∏(x→Q)可转化为如下形式:

Ph_i=(i.sit→i.pick_fork.i→i.pick_fork.i⊕1→i.down_fork.i→i.down_fork.i⊕1→i.up→Ph_ic)∏(i.sit→i.pick_fork.i→

i.pick_fork.i⊕1→i.down_fork.i⊕1→i.down_fork.i→i.up→Ph_ic)∏(i.sit→i.pick_fork.i⊕1→i.pick_fork.i→

(i.down_fork.i→i.down_fork.i⊕1→i.up→Ph_ic)∏(i.sit→i.pick_fork.i⊕1→i.pick_fork.i→i.down_fork.i⊕1→

i.down_fork.i→i.up→Ph_ic).

叉子进程的CSP描述与进程(ii)相同.

哲学家就餐问题形成的并发系统COLLGE可用CSP描述如下:

Ph=Ph1||Ph2||Ph3

(v)

Fork=Fork1||Fork2||Fork3

(vi)

COLLGE3=Ph||Fork (vii)

(vii)

5.2 实验结果

本实验分为两部分:(1) T_ASP的验证能力和验证准确性实验;(2) 一次验证多条性质的实验.实验中,分别采用了DLV,Smodels和Cmodels这3种ASP求解器.实验平台配置如下:Win7,Inter(R) Core(TM) i3-2000 CPU @ 3.10GHz,RAM:4.00GB.

1. T_ASP的验证能力和验证的准确性

为了说明T_ASP系统的验证效果,以哲学家就餐模型为例进行实验,并与文献^[29]中的方法进行比较.实验主要从两方面进行:(1) 系统的验证能力;(2) 验证结果的准确性.简化起见,称文献^[29]中的方法为CS_ASP.

分别设定M₁,M₂,M₃,M₄和M₅对性质P₁验证.其中,M₁=ph₁||ph₂,表示哲学家ph₁和ph₂并发,ph_i(i=1,2)采用形式(i)进行描述;M₂=ph₁||ph₂||ph₃,表示哲学家ph₁,ph₂和ph₃并发,ph_i(i=1,2,3)也采用形式( i)进行描述;M₃=ph₁||ph₂,ph_i(i=1,2)采用形式(iii)进行描述;M₄=ph₁||ph₂,ph_i(i=1,2)采用形式(iv)进行描述;M₅=ph₁||ph₂||ph₃,ph_i(i=1,2,3)采用形式(iii)进行描述.待验证性质为P₁=F1.up∧F2.up,即,哲学家ph₁和ph₂都可以用餐.表2给出了相应的实验结果(CS_ASP的并发步骤限制在25步以内).结果表明:T_ASP调用Cmodels时验证效率最高,Smodels次之,DLV最低;CS_ASP和T_ASP都可以完成对M₁的验证,在同种求解器下验证效率基本相当;CS_ASP不能对M₂,M₃,M₄和M₅进行验证,这是由于CS_ASP中不具备分支进程的转化机制和并发的递归调用机制.

T_ASP不限定验证的步数,而CS_ASP是在有穷步骤内对模型进行验证的.为了比较这两种验证方法的效率和准确性,在M₁上对性质P₁,P₂和P₃进行验证.其中,P₂=G(1.sit→F1.up),即,ph₁必然可以吃到东西;P₃= G(1.up→X2.up),即ph₁起身后离开,接着ph₂起身离开.由表3的实验结果可见:CS_ASP和T_ASP在同种求解器下的验证效率相当,且调用Cmodels和Smodels的验证效率高于DLV.此外,CS_ASP验证结果满足P₂,T_ASP则输出不满足P₂.这是由于CS_ASP的并发步骤数限定较少时产生了误判.验证P₃时,两种方法的验证结果都是不满足,但T_ASP还输出反例集CE.

2. 一次验证多条性质

在哲学家就餐模型上,实现P₃和P₄的同时验证以及P₃和P₄的独立验证.刻画3个哲学家就餐模型M₆,M₇,M₈,其中,M₆=COLLGE₃,且ph_i(i=1,2,3)采用形式(i)进行描述;M₇=COLLGE₃,且ph_i(i=1,2,3)采用形式(ii)进行描述;M₈= COLLGE₃,且ph_i(i=1,2,3)采用形式(iii)进行描述.对COLLGE₃进行验证时,发生死锁的迹已经除去.此外,约定COLLGE₃满足基本的安全性质,如,一个叉子不能同时被两个哲学家拿起.P₃与前文相同,P₄=F1.up∧F2.up∧ F3.up表示3个哲学家都可以吃到饭.

由表4的实验结果可见:大部分情况下,P₃和P₄同时验证消耗的时间要小于独立验证所消耗的时间之和,表明1次验证多条性质可提高性质验证效率.此外,M₆的验证时间要远小于M₇和M₈.这是由于建模方式越严格,模型的验证效率越高.

6 相关工作

CSP的形式化验证包括程序正确性证明和模型检测两种方法:程序正确性证明主要在早期使用,并逐渐演化成为Hoare逻辑的公理语义^[39];模型检测是当前CSP验证的主流方法,如FDR^{[17, 18]},ARC^[19],PAT^[20],SymFDR^[28]都采用模型检测技术对CSP进行验证.FDR是应用最广的CSP验证工具,它通过操作语义将CSP转化为相应的迁移系统,进而显式地导出相应的指称语义模型,并完成性质验证.然而,FDR中性质采用CSP语言进行描述,有利于精炼检测,但其通用性不强.ARC是一种高效的CSP验证工具,它是通过操作语义将进程转化为相应的抽象语义模型——基于OBDD的符号模型.该方式可以有效地缓解状态爆炸问题,但是转化过程比较复杂.此外,ARC也采用CSP语言进行性质规约,不利于性质的描述.与ARC类似,PAT也是将进程转化为基于OBDD的符号模型;不同的是,PAT采用有界模型检测方式,并基于时态逻辑描述性质.PAT的不足之处是,对包含无穷序列的模型无法进行完全正确的判定.SymFDR是在FDR的基础上结合BMC和k-归纳方法构造的CSP检测工具:BMC技术使SymFDR快速找到错误,k-归纳使其具有无界模型检测的能力.但是,SymFDR继承了FDR的语义模型生成方式和性质规约方式.与上述验证工具不同,本文给出的CSP检测工具——T_ASP并非基于操作语义,而是采用一种新的指称语义模型——关键迹模型,作为语义和实现模型.该模型包含数据量较小,一定程度上缓解了状态爆炸问题,且模型生成采用递归计算策略,易于理解,实现简单.与PAT类似,T_ASP也采用基于事件的LTL公式对性质进行规范,通用性好,描述能力强.此外,T_ASP还可以一次验证多条性质,一定程度上提高了验证效率.

与本文工作类似,Heljanko提出了一种基于ASP的有界模型检测方法,其基本思想是:把LTL性质验证归约为回答集求解,利用ASP技术检测Petri网在有限步骤内的并发状况,从而完成系统的有界LTL模型验证^[40].与此类似,文献^[41]提出了一种基于ASP的CTL公式的可满足判定方法,把CTL的可满足性判断问题转化为偏好回答集计算.基于Heljanko的思想,文献^[42]实现了有界抽象状态机(ASM)的LTL验证;文献^{[40, 41]}中的方法可以快速地对性质进行验证,并找出相应的反例,但是无法对系统进行无界模型验证.与上述工作不同,本文给出的T_ASP系统可对具有有穷迹语义的CSP进程进行无界模型检测,且输入为高层语言模型,由系统自动生成语义模型,极大地方便了并发系统的验证.

文献^[29]初步探讨了基于ASP的CSP模型验证方法,实现了CSP模型和时态逻辑公式的ASP描述以及基于ASP求解器的性质验证方法,但其自动化程度不高,且相应的理论支撑不够.文献^[30]中首次提出了基于进程迹的CSP模型验证思想,通过递归计算策略生成进程的迹模型,并通过SAT判定思想对CSP的迹模型进行性质验证.然而,迹模型通常比较庞大,所以验证效率不是很高.本文在文献^[30]的基础上所提出的关键迹模型,只生成并发过程中实际发生的迹,数据量远小于迹模型,从而提高了验证效率.此外,系统地构建了关键迹模型的自动生成机制及基于关键迹模型的自动验证机制,与文献^[30]相比,本系统可完全自动化.

7 总 结

本文主要工作可分为理论和实现两个方面.

· 理论方面,定义了一种CSP指称语义模型——关键迹模型,并给出了该模型的递归计算策略;论证了基于关键迹模型验证的可靠性;依据可满足性判定技术,提出了基于关键迹的性质验证方法;

· 实现方面,利用ASP技术构造了关键迹模型的自动生成方法以及LTL的自动验证方法.

在此基础上实现的T_ASP系统可完成CSP的基本验证,并具有以下特色:(1) 一次提供多条反例,便于系统诊断模块综合分析,错误较多时可减少诊断时间;(2) 采用LTL进行性质规约,通用性好,描述能力强;(3) 可一次验证多条性质;(4) 基于指称语义,相关理论易理解,系统实现简单、便于扩展和修改.

T_ASP初步实现了上述功能,但在验证规模、反例分析以及适用场景方面还存在不足之处.未来研究集中在以下几个方面:

(1) 基于反例的系统调试技术.

反例生成与模型调整在验证过程中相辅相成,反例生成在T_ASP系统中已经完成,但尚不能进行模型调整. T_ASP可利用非实例化ASP程序的调试技术分析已验证性质的支撑原因集合,进而对模型进行调整.目前,已存在多种实例化ASP程序的调试技术,如不一致性分析技术^[43]、Justification技术^[44]、基于ASP的调试技术^[45]、Meta-ASP的调试技术^[46].下一步工作可将实例化程序的调试技术引入非实例化程序^[47],并应用于T_ASP的调试模块.

(2) 基于有界模型检测技术的关键迹模型验证.

有界模型检测技术只检测模型的有限前缀,可以减少内存需求,提高验证效率,但有可能提供错误的反例.下一步的研究中,将把增加完备性阈值^[48]、k-归纳或Craig interpolation策略引入基于ASP的有界模型检测中,从而为性质验证提供可靠反例.

(3) 实现ASP平台下的增量式验证技术.

增量式验证可以提高知识重用,从而提高验证效率.但ASP平台下存在的理论难题是:如何确定新的性质加入后,系统的已验证性质继续可满足.因为只有已验证性质继续保持满足,该验证方法才是有效的.显然,该问题在单调逻辑中不会出现,然而对于非单调逻辑则是可能的.为此,可借助ASP语义研究的有关理论,如Splitting定理^[49],研究满足上述关系的充分或充要条件.

(4) 面向可扩展需求的应用场景研究.

T_ASP系统的优势之一在于其具有良好的可扩展性,可以较方便地把一些新的处理机制接入系统.因此,具有较强扩展需求的应用领域非常适合采用T_ASP系统.例如,轻量级Web组合中的适配问题,除了传统的适配验证之外,可以把基于ASP的适配机制引入T_ASP,达到自动适配的目的.