May测试语义前同余性的研究

南京航空航天大学计算机科学与技术学院　邓鹏辉　张晋津



May测试语义前同余性的研究

南京航空航天大学计算机科学与技术学院邓鹏辉张晋津

【摘要】在面向服务器的进程代数理论中，为了描述服务器和客户之间的并发行为，Bernardi和Hennessy等人提出了三种must-testing语义，并对它们的前同余性以及公理系统进行了研究。但是关于may-testing语义并未涉及，本文将对可能测试语义的前同余性进行研究。

【关键词】进程代数；并发行为；may-testing语义；前同余性

0　引言

在进程代数理论中，Nicola和Hennessy早期提出三种测试语义(may,must,may&must)用来描述精化关系，基于被测试进程与环境间的相互作用诱导出的计算路径序列，分析其行为[1][2]。近几年，Barbanera, Liguoro, Castagna等人提出面向网络服务器的必须测试理论[3]，Bernardi和Hennessy提出了面向网络服务器的CLT语义以及SVR语义用于描述必然测试(must-testing)语义精化关系[4]。它介绍了两种子行为关系：服务器(server)和客户(client)，它们的语法一致，都可以看成进程，并描述了它们之间的相互作用。而基于网络服务器的may-testing语义在文献[4]中并未涉及。本文基于网络服务器的概念，对may-testing测试语义的前同余性进行研究。

1　预备知识

本节简单介绍may-testing测试语义的语法及其结构化操作语义规则，CLT测试前序的语法以及语义定义，以及饱和集的概念。关于may-testing测试语义的更多详细介绍可以参考文献[2]。本文所使用的符号都是常用符号，其基本含义与Milner在文献[4][5]中使用的意义一致。

定义1[3]May-testing语义的项(进程)由BNF范式定义如下：

表1罗列了 May-testing语义的结构化操作语义规则，表中。

表1　结构操作语义规则

具有如下形式的转换序列称为p||r的一条计算路径p||r=p0||r0→p1||r1→…→pk||rk→…。如果它是无限的或者它的最终状态pn||rn满足pn||rn，则称它是极大的；如果存在满足rk，则称它是成功的。如果存在一条p||r的极大计算路径是客户成功的，则称p可能满足 r，记为p may r。

2　may-testing前序的语法定义

本节给出may-testing语义的两种语义定义，并证明它们是等价的。

定义2 给定进程r1、r2，如果对任意进程p，使得p may r1蕴涵p may r2，则称r1是r2的精化，记为。

定义3 给定进程r1、r2，，如果对s的任意前缀，使得蕴涵，则称r1是r2的精炼，记为。

定理1 对任意客户r1、r2，当且仅当。

3　may-testing前序的前同余性

在前面一节介绍了两种等价的may-testing前序的语法定义，而同余性是组合推理的基础，这节我们将证明该测试前序具有同余性。

情形1 前缀算子a。

情形2 选择算子+。

假设r1+r2并且a.是a.并且是s的前缀使得。从而r1或者r2，不是一般性，假设r1，从而。由r1可知存在s的前缀使得，所以r1+r2。

4　结束语

本文基于网络服务器的概念，提出两种等价的may-testing前序，并证明了该测试前序具有前同余性本文的研究工作只是相关领域的一部分，针对不同问题还有许多值得研究的方向，如：本文只讨论了进程的有限行为，可以在此基础上加入递归算子，用以刻画无限的行为。该语义中含递归算子的最大前同余性，方程唯一解和最大解等等研究领域都未涉及。

参考文献

[1]Nicola D,Hennessy M.Testing equivalences for processes[J]. ELSEVIER,1983,34(1-2):83-133.

[2]Hennessy M.Algebraic Theory ofProcesses[J].MIT Press, 1988,1-272.

[3]Castagna G,Gelbert N,Padovani L.A theory of contracts for web services [J].ACM Trans.,2009,31(5):1-61.

[4]Bernardi G,Hennessy M.Mutually testing processes[J].ACM, 2015,11(2:1):1-23.

[5]Milner R.Communication and Concurrency[J].Prentice Hall, 1989,1-260.

邓鹏辉（1986－），男，江西鹰潭人，南京航空航天大学计算机科学与技术学院研究生，研究领域：进程代数、计算机科学中的逻辑学等。

张晋津（1981－），男，山西曲沃人，讲师，博士，研究领域：形式化方式、计算机科学中的逻辑学等。

作者简介：

基金项目：国家自然科学基金（编号：11426136，60973045）；江苏省高校自然科学基金（编号：13KJB520012）。