对称与动作细化

发布时间：2020-06-06 13:42

【摘要】：一般硬件系统和软件系统都存在大量的相同的或同构的组件,相应地,它们的模型常常在结构上存在对称性,这种对称结构一般具有相同或非常相近的性质。人们为了使问题简化,根据这种情况开发了对称约简算法来简化模型。特别是在形式化验证中,对称约简方法已经成为解决状态爆炸问题的有效方法之一。进程代数已经是刻画并发系统的最普遍、最常用的描述语言,而事件结构也是刻画真并发系统的强有力的建模工具,它们常常展示出对称性。然而,当前大多数研究都集中在基于变迁系统模型的对称约简,从未涉及这两种建模工具的对称性方面的研究。在本文中,我们对进程代数语言和事件结构模型的对称约简进行了深入研究。这些工作力图从结构上建立对建模语言和模型进行约简的基本理论,目的是希望从结构上建立起类似于行为等价的由细到粗的约简体系,为开发复杂系统而建立的不同层次静态约简模型服务。另一方面,自顶向下逐步细化的层次化设计方法是人们广泛接受的设计计算机硬件系统和软件系统的最主要方法之一。动作细化是系统层次化刻画方法的核心操作,这一理论的研究一般在进程代数和事件结构模型中进行的,已经取得了丰硕的成果。在此基础上,我们研究了对称约简对动作细化的影响,同时研究了交织等价和步进等价在动作细化下的保持问题。 本文针对进程代数语言提出了进程的对称性概念,给出了对称约简算法,并证明了约简后的进程与原进程是交织迹和交织互模拟等价的,同时提供了两个有意义的实例来说明对称性的定义并验证了约简算法的正确性。 接下来,针对事件结构模型我们提出了基于置换群的对称性概念。在事件结构中,引入了事件结构的商结构模型,证明了商结构与原事件结构是迹、互模拟和偏序多集迹等价的,建立了针对事件结构的对称约简算法,得出了对称约简不影响等价在动作细化下的保持。在研究了事件结构的对称性之后,进一步从理论上比较对称约简与自互模拟约简的区别和联系。 交织等价(即交织迹等价和交织互模拟等价)与步进等价(即步进迹等价和步进互模拟等价)在动作细化下是不保持的。一些工作研究了交织互模拟等价在严格限制动作细化的情况下才能保持,但在这种限制下交织迹等价仍然不保持,没有工作进一步讨
【学位授予单位】：中国科学院研究生院（成都计算机应用研究所）
【学位级别】：博士
【学位授予年份】：2006
【分类号】：TP303

【共引文献】

相关期刊论文 前10条

1 杨昕梅;孙秀莉;李绍荣;;基于动作细化的握手扩展[J];电子科技大学学报;2011年03期

2 王焕宝;张佑生;;图元的子句时新性[J];东南大学学报(自然科学版);2008年S1期

3 韩婷婷;陈韬略;颜峰;吕建;;一个基于偏序事件结构的Web服务模型及其形式化组装[J];计算机科学;2005年05期

4 张辉;于建江;汤克明;;用于整合SOA与EDA的智能化事件驱动模型[J];计算机应用研究;2009年09期

5 蒋昌俊;Petri网理论与方法研究综述[J];控制与决策;1997年06期

6 赵锡英;;交互式马尔可夫链代数的事件结构模型[J];兰州交通大学学报;2008年03期

7 张晓东,柴跃廷,任守榘;一种形式化的构件模型框架[J];清华大学学报(自然科学版);2000年03期

8 叶新铭,郝松侠;IPv6邻居发现协议的形式化验证[J];软件学报;2005年06期

9 闫炜;吴尽昭;高新岩;;用基于流事件结构的偏序时序逻辑刻画并发系统多诱因特征[J];四川大学学报(工程科学版);2008年01期

10 徐克鹏;左春;;基于BPM的仓储物流管理系统的设计与实现[J];计算机系统应用;2010年05期

相关博士学位论文 前9条

1 杨琛;打结不变的命题投影时序逻辑与模型检测[D];西安电子科技大学;2010年

2 刘志锋;模型检测中关键技术的研究及其应用[D];南京大学;2011年

3 张波;基于XML的分布式软件体系结构研究[D];中国科学院软件研究所;2001年

4 任洪敏;基于π演算的软件体系结构形式化研究[D];复旦大学;2003年

5 陈冬火;超协调时序逻辑及其模型检测方法[D];中国科学院研究生院（成都计算机应用研究所）;2006年

6 孙秀莉;基于动作细化的异步电路自动综合[D];中国科学院研究生院（成都计算机应用研究所）;2005年

7 王海霞;运算电路的形式化验证方法研究[D];中国科学院研究生院（计算技术研究所）;2004年

8 蒋昌俊;并发系统综合的PN行为理论及其应用[D];中国科学院研究生院（计算技术研究所）;1998年

9 郑光;并发系统的动作细化理论[D];兰州大学;2008年

相关硕士学位论文 前10条

1 张静;基于SOA的电信综合定单处理子系统的设计[D];河北科技大学;2011年

2 王蜜;支持服务协同的PaaS平台中服务动态演化方法研究[D];山东大学;2011年

3 许式阳;基于SOA的企业信息系统的研究与应用[D];杭州电子科技大学;2010年

4 李军;软构件工程学习环境开发及应用[D];大连理工大学;2001年

5 赵云峰;低压电力线信道建模及其仿真系统的研究[D];河海大学;2003年

6 龙军;关于密码协议形式化验证方法的研究[D];国防科学技术大学;2003年

7 曾琼;概率进程代数的度量指称语义[D];中国科学院研究生院（成都计算机应用研究所）;2006年

8 郭晋伟;SOA架构的管理信息系统设计与实现[D];中国科学院研究生院（沈阳计算技术研究所）;2006年

9 张之s，

本文编号：2699761