法律状态公告日
法律状态信息
法律状态
2016-03-02
授权
授权
2013-09-04
实质审查的生效 IPC(主分类):G06F9/45 申请日:20130524
实质审查的生效
2013-08-07
公开
公开
技术领域
本发明属于形式化建模验证技术领域，特别是时间相关系统的建模验证方法，提出了一 种从扩展π演算p-π到MSVL的转换方法，可用于对时间相关移动并发系统进行建模、仿 真和验证。
背景技术
随着移动互联网计算和计算机网络通信技术的发展，以移动性、并发性、时间相关性、 异构性等为主要特征的时间相关移动并发系统已得到广泛应用。由于时间相关移动并发系统 本身的复杂程度高，使得其开发过程不仅难度大，效率低，周期长，且难以避免和发现其中 隐含的缺陷和错误。对于安全攸关的时间相关移动并发系统，其失误和崩溃可能会造成重大 损失，因此时间相关并发系统的正确性、可靠性、安全性等可信性质受到人们的普遍关注。 然而，当前的很多形式化方法，大都只能对普通的并发系统建模和验证，缺乏对时间相关移 动并发系统建模和验证的方法。
如何找到一种能够对时间相关移动并发系统的时间相关行为进行建模的形式化方法并 完成时间相关性质的有效验证成为研究的重点。
p-π是一种扩展的π演算，它不仅继承了π演算能对移动并发系统建模验证的能力，而 且通过加入时间动作前缀，它还能对时间相关的移动并发系统建模。作为一种面向特殊应用 领域的进程代数，p-π提供了丰富的数学方法用于对时间相关系统进行分析验证，但是这些 方法使用起来都比较繁琐且缺乏工具支持，不能实现验证的自动化，影响了对时间相关性质 的有效验证。
框架时序逻辑语言MSVL是一种建模、仿真和验证的时序逻辑编程语言。MSVL是可 执行的，并且有相应的支持工具，已应用于工业中的软件和硬件的建模、仿真和验证。MSVL 基于投影时序逻辑（Projection Temporal Logic，PTL），由于投影时序逻辑提供了丰富的建模、 仿真和验证时间相关并发系统的理论基础，使得从p-π转换为MSVL成为一种可能。而命 题PTL（PPTL）可以表达完全正则性质，也就是说可以表达更多的时序性质，故可方便的 表达时间相关性质，这也极大地便利了对转换得到的时间相关移动并发系统的验证。因此， 为了完成对时间相关移动并发的建模和有效验证，急需一种从扩展π演算p-π到MSVL的 转换方法，以便利用MSVL的现有支持工具完成对时间相关移动并发系统的有效验证。
发明内容
为了克服上述现有技术的不足，本发明的目的在于面向时间相关移动并发系统，提供一 种从扩展π演算p-π到MSVL的转换方法，以实现基于MSVL的对时间相关移动并发系统 的建模、仿真和验证。
为了实现上述发明目的，本发明所采用的技术方案是：
一种扩展π演算p-π到MSVL的转换方法，包括采用p-π对时间相关并发系统建立系统 模型，其特征在于：包括制定名字和原子命题到MSVL的映射规则，制定p-π进程到MSVL 程序的转换规则，通过所述p-π建立的系统模型采用相应的名字和原子命题映射规则将名字 和原子命题映射为MSVL的通道和布尔变量，再将所述的系统模型通过进程转换规则转换 为MSVL程序。
在上述技术方案的基础上，采用p-π对时间相关移动并发系统建模包括采用名字来建模 时间相关移动并发系统进行消息通信的通道，其中所述名字包括自由名和受限名；
采用原子命题来建模时间相关移动并发系统在执行的过程中各个子进程所占有的资源；
采用进程操作符来连接各个子进程，包括前缀操作符“.”，非确定性选择操作符“+”，并 发操作符“|”，匹配操作符“[]”，限名操作符“v”，以及基于进程标识符的进程实例。
在上述技术方案的基础上，所述的名字到MSVL的的映射规则为一个名字转换为一个 相应的MSVL通道变量，所述的原子命题到MSVL的映射规则为一个原子命题转换为一个 相应的MSVL布尔变量。
在上述技术方案的基础上，所述进程的转换规则包括通过制定映射函数Υ： {p-πprocess}——→{MSVLprogram}完成从p-π进程到MSVL程序的转换，该函数 基于p-π进程的结构递归构造而成。
在上述技术方案的基础上，所述进程的转换规则，包括查看系统模型中是否包含进程实 例，如果不包含进程实例，直接通过映射函数Υ将通过p-π建模的系统模型转换为MSVL 程序；如果包含进程实例，则先通过映射函数Υ将通过p-π建模的进程标识符转换为MSVL 程序，再通过映射函数Υ将通过p-π建模的系统模型转换为MSVL程序，并将进程实例通 过替换函数转换为MSVL程序。
在上述技术方案的基础上，所述的进程转换规则的递归构造步骤如下：
（1）p-π的空进程转换成MSVL的空语句，其形式化表述为：
其中0为p-π的空进程，ε为MSVL的空语句；
（2）p-π的输出动作前缀转换成MSVL的发送语句，其形式化表述为：
其中为p-π的输出动作前缀，send(Cx,Cy)为MSVL的发送语句；
（3）p-π的输入动作前缀转换成MSVL的接受语句，其形式化表述为：
其中x(y)为p-π的输入动作前缀，receive(Cx,Cy)为MSVL的接受语句，且y是p-π的受 限名，为存在量词，frame表示Cy在没有被重写时在区间上保持上一个状态的值；
（4）p-π的需要同步的输出输入动作前缀转换成MSVL的等待发送和等待接受语句， 形式化表述为：
其中和await(x(y).P)分别表示二者中涉及的输出输入动作前缀需要等待 与之同步的输入输出动作前缀，wait_send(Cx,Cy)和wait_receive(Cx,Cy)分别为MSVL 中的等待发送语句和等待接受语句，在这里为存在量词，frame表示Cy在没有被重写时 在区间上保持上一个状态的值；
（5）p-π的内部动作前缀转换成MSVL的表示发生内部动作的命题，其形式化表述为：
其中τ为p-π中的内部动作前缀，pI为MSVL中的一个一个特定的命题，pI用于表示当前 状态发生了一个内部动作，τ是瞬时动作，pI设定区间长度为0，即转换为pI^ε；
（6）p-π的性质动作前缀转换成MSVL的布尔变量赋值语句，形式化表述为：
其中}且pi(1≤i≤n)为p-π中原子命题， Ip∈PR，其中PR为系统所涉及的所有资源，pi∈Ip表示系统当前状态占有该资源，转 换为MSVL中的布尔变量，并将其赋值为true；
（7）p-π的时间单元动作前缀转换成MSVL的单位时间语句，其形式化表述为：
其中skip在p-π中表示时间单元动作前缀，而在MSVL中为单位时间语句；
（8）p-π的空动作前缀转换成MSVL的空语句，形式化表述为：
其中ε在p-π中表示空动作前缀，而在MSVL中为空语句；
（9）p-π的非确定性选择进程转换成MSVL的选择语句，形式化表述为：
其中+为p-π中的非确定选择操作符，P1+P2表示P1或P2非确定性的执行，为MSVL中的选择语句，表示Υ(P1)或Υ(P2)选择性地执行；
（10）p-π的并发进程转换成MSVL的并发语句，形式化表述为：
其中|为p-π中的并发操作符，P1|P2表示P1与P2并发执行，Υ(P1)||Υ(P2)为MSVL中的并 发语句；
（11）p-π的匹配进程转换成MSVL的条件语句，形式化表述为：
其中[]为p-π中的匹配操作符，[a1＝a2]P表示若a1＝a2则执行P，否则为空进程， thenΥ(P)elseε为MSVL中的条件语句，当时，执行语句Υ(P)， 否则执行空语句；
（12）p-π的限名进程转换成MSVL的存在量词语句，形式化表述为：
其中ν为p-π中的限名操作符，νaP表示a为受限名，frame表示Ca在没有被重写时在 区间上保持上一个状态的值；
（13）p-π的进程实例转换成MSVL的函数替换语句，形式化表述为：
先将PA转换为Υ(PA)，再通过实参替换形参以完成进程实例的转换,其中和分 别为向量和其中Aa1,...,an为p-π中的进程实例，进程标识符A 的定义为且其中和分别为向量a1,...,an和 x1,...,xn。
与现有技术相比较，本发明由于采用区间动作前缀描述时间相关移动并发系统的时间 相关行为，因而可以很好的对时间相关移动并发系统建模，又因为采用将建立的模型转换为 MSVL语言可以借助MSVL建模、仿真和验证工具完成对时间相关移动并发系统的仿真验 证。这就使得本发明成为一种有效的为时间相关移动并发系统建模、仿真和验证的方法。采 用区间动作前缀，即skip和Ip，为时间相关并发系统的时间相关行为建模，由于区间动作 前缀考虑了时间，可以精确刻画时间相关行为；采用结构化的转换规则完成从p-π到MSVL 的转换，鉴于规则具有高度的结构化对应关系，可以保证转换前后系统的结构等价性。
附图说明
图1是本发明提出的从扩展π演算p-π到MSVL转换流程图。
具体实施方式
下面将结合附图对本发明作进一步的描述。
如图1所示，本发明为一种从扩展π演算p-π到MSVL的转换方法，所述方法包括以下 步骤：
（1）采用p-π建立系统模型，所述p-π是一种面向时间相关移动并发系统的扩展π演 算。令N为名字的可数无穷集，Prop为原子命题的集合，为非负整数的集合。p-π的语法 定义如下：
其中π是动作前缀，它包括接受动作前缀x(y)，发送动作前缀内部动作前缀τ，单 位时间动作前缀skip，性质动作前缀且 和空动作前缀ε。0为空进程；π.P为前缀动作监视进程； P1|P2表示P1和P2不确定地选择执行；P1|P2表示进程P1和P2并发执行；[a1＝a2]P表示 若a1＝a2，则该进程按P执行，否则为空进程；νaP表示将名字a限制在进程P中使用； 对于进程实例A<a1,...,an>，A是进程标识符，和分别表示向量a1,...,an和x1,...,xn。在建模过程中涉及的相关导出进程定义包括：
（2）通过映射函数将采用p-π建立的系统模型转换为相应的MSVL程序。所述的MSVL 程序为一种基于投影时序逻辑的建模、仿真和验证语言。MSVL由表达式和语句构成。表达 式的语法定义如下：
e::＝c|x|&x|*x|○x|Θx|e0ope1(op::＝+|-|×|/)
其中c为常量，x为变量，&x为指向x的指针，*x为取指针变量x的内容。○和Θ为时 序操作符，分别表示下一状态和前一状态。b为布尔表达式。
MSVL语言包括十六条基本语句，具体如下：
其中x为变量，p和q为任意的MSVL程序。终止语句表示当前状态是最后一个状态，框 架语句用于解决时序逻辑语言在执行过程中变量的值的继承问题。其中状态框架语句用于解 决变量当前状态的继承问题而区间框架语句用于解决变量在整个区间的继承问题。合取语句 p∧q表示p和q同时满足，选择语句p∨q表示p或q满足，○p表示在下一状态p满足， □p表示在每个状态p都满足。条件语句if b then p else q表示若b成立则执行p否则执 行q。存在量词语句表示存在一个变量x使得p(x)满足。顺序语句p;q表示p和 q顺序执行。并发语句p||q表示p和q并发执行。While语句while b do p表示若b成立 则执行p直到b成立。同步通信语句await(b)通过b来使通信双方同步。投影语句 (p1,...,pm)prjq表示p1,...,pm与q采用不同的时间粒度并发执行，其中q执行在p1,...,pm的每个区间的端点上，这样p1,...,pm和q就可以自治地设定区间长度。
MSVL中的通道和通信原语的定义如下：
转换的具体步骤如下：
1.将通过p-π建模的系统模型中的名字转换为MSVL中的通道，具体为一个p-π中的 名字对应一个相应的MSVL通道。
2.将通过p-π建模的系统模型中的原子命题转换为MSVL中的布尔变量，具体为一个 p-π中的原子命题对应一个相应的MSVL布尔变量。
3.查看系统模型中是否包含进程实例，不包含进程实例则直接通过映射函数Υ将通过 p-π建模的系统模型转换为MSVL程序。具体映射规则如下：
步骤3.1：p-π的空进程转换成MSVL的空语句，形式化表述为：
其中0为p-π的空进程，ε为MSVL的空语句。
步骤3.2：p-π的输出动作前缀转换成MSVL的发送语句，形式化表述为：
其中为p-π的输出动作前缀，send(Cx,Cy)为MSVL的发送语句。
步骤3.3：p-π的输入动作前缀转换成MSVL的接受语句，形式化表述为：
其中x(y)为p-π的输入动作前缀，receive(Cx,Cy)为MSVL的接受语句，由于y是p-π的 受限名，所以此处要映射为MSVL中的局部变量，即要在Cy前加存在量词，在这里frame 是为了让Cy在没有被重写时在区间上保持上一个状态的值。
步骤3.4：p-π的需要同步的输出输入动作前缀转换成MSVL的等待发送和等待接受语 句，形式化表述为：
其中和await(x(y).P)分别表示二者中涉及的输出输入动作前缀需要等待 与之同步的输入输出动作前缀。wait_send(Cx,Cy)和wait_receive(Cx,Cy)分别为MSVL 中的等待发送语句和等待接受语句。在这里和frame的用法与步骤2.2.3中输入动作前缀 的转换中涉及的用法相同。
步骤3.5：p-π的内部动作前缀转换成MSVL的表示发生内部动作的命题，形式化表述 为：
其中τ为p-π中的内部动作前缀，pI为MSVL中的一个特殊的命题，专门用于表示当前状 态发生了一个内部动作，又因为τ是瞬时动作，所以在转换为MSVL程序时，要为pI设定 区间长度为0，即转换为pI∧ε。
步骤3.6：p-π的性质动作前缀转换成MSVL的布尔变量赋值语句，形式化表述为：
其中
步骤3.7：p-π的时间单元动作前缀转换成MSVL的单位时间语句，形式化表述为：
其中skip在p-π中表示时间单元动作前缀，而在MSVL中为单位时间语句。
步骤3.8：p-π的空动作前缀转换成MSVL的空语句，形式化表述为：
其中ε在p-π中表示空动作前缀，而在MSVL中为空语句。
步骤3.9：p-π的非确定性选择进程转换成MSVL的选择语句，形式化表述为：
其中+为p-π中的非确定选择操作符，P1+P2表示P1或P2非确定性的执行。Υ(P1)∨Υ(P2) 为MSVL中的选择语句，表示Υ(P1)或Υ(P2)选择性地执行。
步骤3.10：p-π的并发进程转换成MSVL的并发语句，形式化表述为：
其中|为p-π中的并发操作符，P1|P2表示P1与P2并发执行。Υ(P1)||Υ(P2)为MSVL中的并 发语句。
步骤3.11：p-π的匹配进程转换成MSVL的条件语句，形式化表述为：
其中[]为p-π中的匹配操作符，[a1＝a2]P表示若a1＝a2则执行P，否则为空进程。 为MSVL中的条件语句，当时，执行语句Υ(P)， 否则执行空语句。
步骤3.12：p-π的限名进程转换成MSVL的存在量词语句，形式化表述为：
其中ν为p-π中的限名操作符，νaP表示a为受限名，即将a的作用范围限制在P中， 进程P不能通过a与其他进程通信，除非P通过一个公开名将a传递给其他进程，让a的 作用范围扩展到P之外。由于a是受限名，故将其转换为MSVL中的局部变量，即在变量 前加存在量词，此处frame的用法与步骤2.2.3中输入动作前缀的转换中的用法相同。
步骤3.13：p-π的进程实例转换成MSVL的函数替换语句，形式化表述为：
其中A<a1,...,an>为p-π中的进程实例，进程标识符A的定义为且 （和分别为向量a1,...,an和x1,...,xn）。此处，应先将PA转换为 Υ(PA)，再通过实参替换形参以完成进程实例的转换（和分别为向量
4.查看系统模型，如果通过p-π建立的系统模型的定义中包含进程实例，则先通过映 射函数Υ将通过p-π建模的进程标识符转换为MSVL程序，再通过映射函数Υ将通过p-π 建模的系统模型转换为MSVL程序，并将进程实例通过替换函数转换为MSVL程序，所述 的映射函数的具体实施步骤如步骤3.1到3.13所示。
对于本领域的技术人员来说，可根据以上描述的技术方案以及构思，做出其它各种相应 的改变以及变形，而所有的这些改变以及变形都应该属于本发明权利要求的保护范围之内。
机译： Gartar演算演算演算演算演算
机译： 从不可扩展的视频转换方法到可扩展的视频，从可扩展的视频转换方法到不可扩展的视频
机译： 用于颜色匹配的颜色转换方法，用于扩展程序模块功能的方法以及使用该方法用于扩展程序模块功能的颜色转换方法
