﻿ 适用于演化过程建模的通信膜演算
«上一篇
 文章快速检索 高级检索

 哈尔滨工程大学学报  2018, Vol. 39 Issue (4): 751-759  DOI: 10.11990/jheu.201610100 0

### 引用本文

REN Junqi, LIU Lei, ZHANG Peng. Communication membrane calculus:a formal method for modeling the process of evolution[J]. Journal of Harbin Engineering University, 2018, 39(4), 751-759. DOI: 10.11990/jheu.201610100.

### 文章历史

Communication membrane calculus:a formal method for modeling the process of evolution
REN Junqi, LIU Lei, ZHANG Peng
College of Computer Science and Technology, Jilin University, Changchun 130012, China
Abstract: In this study, we propose a calculus approach named communication membrane calculus which can be used to model the evolution process of a system as an extension of membrane computing.This calculus approach improves communication ability between membranes based on the formal method of membrane computing, to make the modeled system capable of changing with the evolution requires.The calculus approach can eliminate the common defects in membrane computing, which is not applicable to the formal method of modeling of system evolution.The theory of automate was used to analyze the characters of the calculus approach and its scope of application in modeling evolution process.In addition, the calculus approach, based on intermembrane communication, was combined with the formal modeling method to model the evolution of a software product line.The modeling results reveal that the calculus approach is applicable to the formal model of an evolution process.
Key words: formal methods    membrane computing    communication mechanism    description ability    formal modeling    automaton    evolution process    system evolution    software product lines

1998年, 罗马尼亚籍国际信息科学院院士Gheorghe Pǎun提出了MC的定义。此后, Pǎun等[3]对MC中的通信机制进一步探讨, 提出了分布式P系统, 使MC初步具有了膜间对象传递的功能。Qi等[4]提出了细胞膜演算的概念, 并将该演算应用于网格事物的形式化建模中。Krishna等[5]提出了移动膜的概念, 移动膜融合了进程演算等演算方法, 拥有更多的反应规则类型以及通信机制。Aman等[6]提出了扩展移动膜的概念, 对表层膜的定义进行了深入的探讨, 打破了MC定义中表层膜不能传递对象的规定。同时, MC类形式化方法已经成功应用于图形学、密码学、系统生物学[7-9]等。

1 通信膜演算

CMC模型包含三个主要元素:膜结构、对象、反应规则。CMC的演算过程可以概括为:它开始于通信膜系统的某个初始格局(初始的膜结构和每个区域内的初始对象), 演算随着格局的转移进行下去, 直至在某个膜内出现演算结果时停止。

CMC的具体定义如下:

Π=(V, μ, O1, …, On, (R1, ρ1), …, (Rn, ρn))

CMC系统利用反应规则的演算过程就是这个系统的格局依照已有的转换规则由初始格局转换为终止格局的过程。

2 规则的操作语义

CMC有九种反应规则, 为了方便叙述, 先给出几个字符的解释。N为膜的名字集合, V*为对象集合, Rm为膜m内的反应规则集合, ρm为膜m内的规则优先级集合:

1)[mu:C]m→[mv:C]m, 其中mN, u:C, v:CV*, 记为:u:Cv:C

2)[k]k[mu:C]m→[kv:C]k[m]m、[k[mu:C]m]k→[k[m]mv:C]k或[m[k]ku:C]m→[m[kv:C]k]m, 其中k, mN, u:C, v:CV*, 记为:u:Cv:Cin_k

3)[k[mu:O]m]k→[k]k, 其中k, mN, u:OV*, 记为:u:Oσ

4)[ku:O]k→[k[m]m]k, 其中k, mN, u:OV*, 记为:u:O→[mμ, O1, …, On, (R1, ρ1), …, (Rn, ρn)]m

5)[mu:O]m[k]k→[k[m]m]k, 其中k, mN, u:OV*, 记为:u:Oλk

6)[k[mu:O]m]k→[k]k[m]m, 其中k, mN, u:OV*, 记为:u:Oηk

7)[mu:R]m→[m(ri, ρi), (ri, ρi)]m, 其中mN, u:RV*, (ri, ρi)∈(Rm, ρm), 记为:u:R→(ri, ρi)copy

8)[k]k[mu:R]m→[k(ri, ρi)]k[m]m、[k[mu:R]m]k→[k[m]m(ri, ρi)]k或[m[k]ku:R]m→[m[k(ri, ρi)]k]m, 其中k, mN, u:RV*, (ri, ρi)∈(Rm, ρm), 记为:u:R→(ri, ρi)in_k

9)[mu:R]m→[m(Rm, ρm)/(ri, ρi)]m, 其中mN, u:RV*, (ri, ρi)∈(Rm, ρm), 记为:u:R→(ri, ρi)delete

CMC默认所有的膜均具有传递功能。从规则复制、传递以及删除的操作语义可以看出, 复制、传递以及删除的都是存在于规则集合中的反应规则。

3 非确定自动机C-NA

C-NA中的状态s用三元组(τ, O, ψ)表示。其中, τ表示该状态所有带有名字的膜以及膜间关系, 可以用一对带下角标的中括号表示膜, 下角标为膜的名字, 膜间关系用中括号的并列和嵌套表示, 并且τ≠∅;O为该状态包含的对象多重集的集合, O可为空; ψ表示该状态中每一个对象多重集所在的膜的名字的集合。

1) 引入n个对象π1, π2, …, πn,

2) 反应规则ri的“→”前的对象多重集Oi作为拆分后第一条规则的“→”前的对象多重集, 第一条规则的→后为引入的n个对象, 第一条规则为:Oiπ1, π2, …, πn;

3) ri中“→”后每一种结果相应变为一条新的反应规则“→”后的结果, 新的反应规则“→”前的对象在π1, π2, …πn中选取一个, 且保证每个πi都能触发一条反应规则。

1) 将ΠS的初始格局抽象为初始状态集S0, 另s0=S0;

2) 将ΠS的终止格局抽象为终止状态集SZ, 另Z=SZ;

3) 将ΠS中除了终止格局每一次演化得到的格局均抽象成一个状态集Si, 另S=S0∪…∪Si∪ …∪SZ;

4) 将ΠS中所有复合规则进行拆分, 与不需拆分的反应规则合并得到反应规则集合的并集RS=R1R2∪…∪Rn, 另Σ=RS;

5) 将ΠS中任意格局使用一条反应规则转换为另外一个格局这个过程, 映射为状态si使用一个字符ri转换另外一个状态si+1的过程, 即将格局转换过程映射si×risi+1, 另f={s0×r0s1, …, si×risi+1, …, sZ-1×rZ-1sZ};

6) 输出(S, Σ, f, s0, Z)。

4 CMC的性质分析

4.1 可达状态分析

4.2 转换步数分析

4.3 NIA说明

C-NA是由一个CMC系统映射而成的。在CMC系统中, 存在格局不断变化无法生成终止格局的情况, 这时的CMC系统就映射为了一个NIA。由于系统格局不断变化且不终止, 导致了自动机中状态集为无限集合。

CMC系统映射成的C-NA时, 存在使C-NA是一个NIA的情况, 如:

1) 系统中存在一条对象变化规则, 该规则“→”后的对象多重集是“→”前对象多重集的n(n>1)倍;

2) 系统中存在一条膜创建规则, 且该规则创建的膜中出现膜创建规则的循环, 或创建的膜包含触发该规则的对象多重集并且能将此对象多重集传递到该规则所在的膜中。

5 软件产品线演化过程建模及分析

5.1 MobileMedia形式化建模

M-M是一款能够生成移动端媒体播放器的具有代表性的软件产品线。目前, M-M已有6个版本[10-13], 因此本文以M-M的演化为例, 对其进行建模。同时, 特征模型是目前使用较多的一种刻画软件产品线结构以及功能的方式, 特征模型以树的形式给出功能之间的关联关系[14]

M-M的现有特征较多, 所以本文选取了M-M的特征模型中的4个具有代表性特征(MobilePhoto(MP)、PhotoManagement(PM)、SMSTransfer(ST)和Favourite(F))进行建模。这4个特征能够体现M-M的层析结构以及特征之间的关系。其中, MP和PM为强制特征, ST和F为选择特征。利用M-M生成软件时, 生成的软件必须具有强制特征, 同时需要根据用户需求, 在选择特征中进行特征挑选。利用CMC对这个特征模型进行建模, 模型1:M-M的建模。模型如下所示:

ΠMM=(V, μ, OMM, OMP, OPM, OST, OF, (RMM, ρMM), (RMP, ρMP)(RPM, ρPM), (RST, ρST), (RF, ρF));

V={OStartO, OMMtoMPO, OMMtoPMO, OStart2O,

OfinishOOMMtoSTO, OMMtoFO, OMPfinishO,

OPMfinishO, Υ}; μ=[MM[MP]MP[PM]PM[ST]ST[F]F]MM;

OMM=OStartO, OMP, OPM, OF=∅;

RMM={OStartOOMMtoMPOin_MPOMMtoPMOin_PMOStart2O,

OStart2OOMMtoSTOin_ST, OStart2OOMMtoFOin_F,

OMPfinishOOPMfinishOOfinishOΥ}, RMP={OMMtoMPOOMPfinishOin_MM}, RPM={OMMtoPMOOPMfinishOin_MM},

RST={OMMtoSTOOfinishOin_MM}, RF={OMMtoFOOfinishOin_MM}; ρ=∅。

5.2 MobileMedia演化过程建模

Neves等通过分析M-M不同版本间的区别, 总结出添加特征、将特征类型进行转换等8种不同类型的演化场景[15-16]。特征类型转换这种演化场景, 是软件产品线最常见的一种演化。本节以将一个强制特征转化为一个选择特征这种演化场景为例, 说明CMC对演化过程建模的适用性。

ΠEMM=(V, μ, OMM, OR, OMP, OMP, OPM, OST, OF, (RMM, ρMM), (RR, ρR), (RMP, ρMP), (RPM, ρPM), (RST, ρST), (RF, ρF));

V={OStart1O, OMPtoAPO, OStart2O, OMtoAR, OMPtoAP1O, Υ, OMO, OAO, OMtoA1R, OChMPtoAPO, OChAO,OAPO}μ = [MM[R]R[MP]MP[PM]PM [ST]ST[F]F]MM;

OMM=OStartO, OR=∅, OMP=∅, OPM=∅, OST=∅, OF=∅;

RMM={OStartOOMMtoMPOin_MPOMMtoPMOin_PM OStart2O, OStart2OOMMtoSTOin_ST, OStart2OOMMtoFOin_F, OMPfinishOOPMfinishOOfinishOΥ},

RR={OMPM-APMOOMPM-APM1ROMPM-APM2RODelete1Rin_MMODelete2Rin_MMODeleteRin_PM, OMPM-APM1R→(ODelete1R→(OStartOOMMtoMPOin_MP OMMtoPMOin_PMOStart2O, ∅)delete, ∅)copy(ODelete2R→(OMPfinishOOPMfinishOOfinishOΥ, ∅)delete, ∅)copy (ODeleteR→(OMMtoPMOOPMfinishOin_MM, ∅)delete, ∅)copy(OStartOOMMtoMPOin_MPOStart2O)copy (OStart2OOMMtoPMOin_PM)copy(OMPfinishOOfinishOΥ)copy (OMMtoPMOOPMfinishOin_MM)copy, OMPM-APM2R→(ODelete1R→(OStartOOMMtoMPOin_MPOMMtoPMOin_PMOStart2O, ∅)delete, ∅)in_MM(ODelete2R→(OMPfinishOOPMfinishOOfinishOΥ, ∅)delete, ∅)in_MM(ODeleteR→(OMMtoPMOOPMfinishOin_MM, ∅)delete, ∅)in_PM(OStartOOMMtoMPOin_MPOStart2O)in_MM(OStart2OOMMtoPMOin_PM)in_MM (OMPfinishOOfinishOΥ)in_MM(OMMtoPMOOfinishOin_MM)in_PM},

RMP={OMMtoMPOOMPfinishOin_MM}, RPM={OMMtoPMOOPMfinishOin_MM}, RST={OMMtoSTOOfinishOin_MM}, RF={OMMtoFOOfinishOin_MM};ρ=∅。

5.3 实例分析与结论

6 结论

1) 对MC类形式化方法进行了扩展, 提出了一种新的膜演算:通信膜演算。CMC在原有的MC类形式化方法定义的基础上增加了规则的传递、复制和删除, 使得反应规则也具有了动态变化的能力, 这使得CMC比已有的MC类形式化方法具有更多的通信机制与变化机制。

2) 利用CMC可以对系统演化过程进行建模, 本文利用MobileMedia演的实例说明了CMC对演化过程建模的适用性。但是, 本文只是在理论上验证了CMC可以应用于系统的演化过程建模, 同时并没有完成CMC工具的实现。

 [1] PǍUN G. Computing with membranes[J]. Journal of computer and system sciences, 2000, 61(1): 108-143. DOI:10.1006/jcss.1999.1693 (0) [2] PǍUN G. 膜计算导论[M]. 潘林强, 曾湘祥, 宋弢, 等译. 武汉: 华中科技大学出版社, 2012: 383-390. PǍUN G. Membrane computing an introduction[M]. PAN Linqiang, ZENG Xiangxiang, SONG Tao, et al, trans. Wuhan: Huazhong University of Science & Technology Press, 2012: 383-390. (0) [3] QI Zhengwei, LI Minglu, FU Cheng, et al. Membrane calculus:a formal method for grid transactions[J]. Concurrency and computation:practice and experience, 2006, 18(14): 1799-1809. DOI:10.1002/(ISSN)1532-0634 (0) [4] KRISHNA S N, PǍUN G. P systems with mobile membranes[J]. Natural computing, 2005, 4(3): 255-274. DOI:10.1007/s11047-005-3771-7 (0) [5] AMAN B, CIOBANU G. Describing the immune system using enhanced mobile membranes[J]. Electronic notes in theoretical computer science, 2008, 194(3): 5-18. DOI:10.1016/j.entcs.2007.12.003 (0) [6] CIOBANU G, PǍUN G, PÉREZ-JIMÉNEZ M J. Applications of membrane computing[M]. Berlin, Heidelberg: Springer, 2006. (0) [7] 戚正伟, 尤晋元. 基于细胞膜演算的Web服务事务处理形式化描述与验证[J]. 计算机学报, 2006, 29(7): 1137-1144. QI Zhengwei, YOU Jinyuan. The formal specification and verification of transaction processing in Web services by membrane calculus[J]. Chinese journal of computers, 2006, 29(7): 1137-1144. (0) [8] PǍUN G. A quick introduction to membrane computing[J]. The journal of logic and algebraic programming, 2010, 79(6): 291-294. DOI:10.1016/j.jlap.2010.04.002 (0) [9] KRISHNA S N, CIOBANU G. On the computational power of enhanced mobile membranes[C]//Proceedings of the 4th Conference on Computability in Europe. Athens, Greece, 2008: 326-335. (0) [10] GAIA F N, FERREIRA G C S, FIGUEIREDO E, et al. A quantitative and qualitative assessment of aspectual feature modules for evolving software product lines[J]. Science of computer programming, 2014, 96: 230-253. DOI:10.1016/j.scico.2014.03.006 (0) [11] BEOHAR H, VARSHOSAZ M, MOUSAVI M R. Basic behavioral models for software product lines:expressiveness and testing pre-orders[J]. Science of computer programming, 2016, 123: 42-60. DOI:10.1016/j.scico.2015.06.005 (0) [12] RINCÓN L, GIRALDO G, MAZO R, et al. Method to identify corrections of defects on product line models[J]. Electronic notes in theoretical computer science, 2015, 314: 61-81. DOI:10.1016/j.entcs.2015.05.005 (0) [13] WHITE J, GALINDO J A, SAXENA T, et al. Evolving feature model configurations in software product lines[J]. Journal of systems and software, 2014, 87: 119-136. DOI:10.1016/j.jss.2013.10.010 (0) [14] BORBA P, TEIXEIRA L, GHEYI R. A theory of software product line refinement[J]. Theoretical computer science, 2012, 455: 2-30. DOI:10.1016/j.tcs.2012.01.031 (0) [15] NEVES L, TEIXEIRA L, SENA D, et al. Investigating the safe evolution of software product lines[C]//Proceedings of the 10th ACM International Conference on Generative Programming and Component Engineering. Portland, Oregon, USA, 2011: 33-42. (0) [16] NEVES L, BORBA P, ALVES V, et al. Safe evolution templates for software product lines[J]. Journal of systems and software, 2015, 106: 42-58. DOI:10.1016/j.jss.2015.04.024 (0)