并发系统的安全性与活性的验证方法

计算机工程与应用 ›› 2008, Vol. 44 ›› Issue (4): 107-110.

并发系统的安全性与活性的验证方法

李杨¹,程建华²,房鼎益¹,陈晓江¹,冯健¹

1.西北大学信息科学与技术学院，西安 710127
2.九江学院信息科学与技术学院，江西九江 332005

收稿日期:2007-08-10 修回日期:2007-11-13 出版日期:2008-02-01 发布日期:2008-02-01
通讯作者: 李杨

Verification of safety and liveness property based on concurrent system

LI Yang¹,CHENG Jian-hua²,FANG Ding-yi¹,CHEN Xiao-jiang¹,FENG Jian¹

1.College of Information Science and Technology,Northwest University，Xi’an 710127，China
2.College of Information Science and Technology,Jiujiang University，Jiujiang，Jiangxi 332005，China

Received:2007-08-10 Revised:2007-11-13 Online:2008-02-01 Published:2008-02-01
Contact: LI Yang

摘要/Abstract

摘要： 网络环境下的分布式系统是典型的并发系统。安全性和活性是并发系统最为关注和需要保证的两个主要性质。然而在并发系统建模和形式化验证时，面临着描述繁琐、复杂和难以理解的问题，特别是当并发系统的规模（并发进程数目）较大时其性质验证时的效率问题更是严重阻碍了并发系统模型检测与验证技术的应用。将组合可达性分析和标号迁移系统的模块化思想与模型验证技术相结合，提出了一套有效的性质验证方法。论证、分析了三个并发系统安全性和活性验证定理，据此导出了并发系统的安全性与活性验证的有效算法。并通过一个简单实例，对算法有效性进行了初步验证。

关键词: 并发系统, 安全性, 活性, 组合可达性, 标号迁移系统

Abstract: Distributed system is one type of typical concurrent systems.In concurrent system，safety and liveness are the two main characteristics which should be most concerned and ensured in its application.However，we have to face the problems，in concurrent system modeling and formal verification，such as tedious description，complex and difficult understanding，and it is more serious because of the low efficiency in model checking when it is much large（with a great number of the processes）.Combining the features of good modularity in Compositional Reachability Analysis（CRA） and high efficiency in Labeled Transition System（LTS），an efficient model verification method is proposed.Three theorems for safety and liveness verification of concurrent systems are proved，and the relevant effective verification algorithms are derived.The feasibility of the algorithms is indicated through a simplified example.

Key words: concurrent system, safety, liveness, compositional reachability analysis, labeled transition system

李杨¹,程建华²,房鼎益¹,陈晓江¹,冯健¹. 并发系统的安全性与活性的验证方法[J]. 计算机工程与应用, 2008, 44(4): 107-110.

LI Yang¹,CHENG Jian-hua²,FANG Ding-yi¹,CHEN Xiao-jiang¹,FENG Jian¹. Verification of safety and liveness property based on concurrent system[J]. Computer Engineering and Applications, 2008, 44(4): 107-110.

[1]	谭莉娟，郑巍，刘友林，樊鑫，杨丰玉. 面向适航标准的机载软件测试验证方法综述[J]. 计算机工程与应用, 2021, 57(15): 9-22.
[2]	程亚歌，胡明生，公备，王利朋，徐二锋. 具有强前向安全性的动态门限签名方案[J]. 计算机工程与应用, 2020, 56(5): 125-134.
[3]	王旭，甘国华，吴凌云. 区块链性能的量化分析研究[J]. 计算机工程与应用, 2020, 56(3): 55-60.
[4]	胡慧，徐正全. 基于边缘和局部熵融合的视觉安全性评估方法[J]. 计算机工程与应用, 2020, 56(12): 215-222.
[5]	肖帅，王绪安，潘峰. 无模逆运算的椭圆曲线数字签名算法[J]. 计算机工程与应用, 2020, 56(11): 118-123.
[6]	张玉鹏1，温蜜2. 针对Modbus协议的双重认证算法设计[J]. 计算机工程与应用, 2018, 54(20): 93-98.
[7]	刘年生. MIMO格密码的设计与实现[J]. 计算机工程与应用, 2018, 54(12): 10-13.
[8]	郭伟1，常金勇1，2，高磊1. 基于DCR假设的KDM-CCA安全性[J]. 计算机工程与应用, 2017, 53(12): 116-120.
[9]	恩德1，陈亚柯1，毛哲龙2. 基于FastICA的低信噪比下L-PLC语音的间断传输[J]. 计算机工程与应用, 2016, 52(9): 108-111.
[10]	田启东1，刘顺桂1，江辉2，彭建春2. 融合拓扑和安全及稳定的电力网脆弱性评估[J]. 计算机工程与应用, 2016, 52(6): 223-226.
[11]	司明. 基于FES和FTA的锅炉安全隐患预警及评价系统[J]. 计算机工程与应用, 2016, 52(23): 244-248.
[12]	王路1，蒋霞2，杜玉越1. 逻辑Petri网的S-组合及活性分析[J]. 计算机工程与应用, 2016, 52(18): 31-35.
[13]	刘健1，王玲1，吴桐1，2. 基于级联混沌系统改进的图像加密算法[J]. 计算机工程与应用, 2015, 51(12): 68-73.
[14]	王建晔1，任平安1，吴振强1，李艳平2. 基于编码混淆的匿名通信机制[J]. 计算机工程与应用, 2014, 50(23): 108-113.
[15]	曾萍，张历，胡荣磊，杨亚涛，刘培鹤. WSN中基于ECC的轻量级认证密钥协商协议[J]. 计算机工程与应用, 2014, 50(2): 65-69.