| 并发系统的安全性与活性的验证方法 |
| |
| 引用本文： | 李杨,程建华,房鼎益,陈晓江,冯健.并发系统的安全性与活性的验证方法[J].计算机工程与应用,2008,44(4):107-110. |
| |
| 作者姓名： | 李杨 程建华 房鼎益 陈晓江 冯健 |
| |
| 作者单位： | 西北大学,信息科学与技术学院,西安,710127 |
| |
| 基金项目： | 陕西省自然科学基金
,
陕西省教育厅产业化重点项目 |
| |
| 摘 要： | 网络环境下的分布式系统是典型的并发系统。安全性和活性是并发系统最为关注和需要保证的两个主要性质。然而在并发系统建模和形式化验证时,面临着描述繁琐、复杂和难以理解的问题,特别是当并发系统的规模(并发进程数目)较大时其性质验证时的效率问题更是严重阻碍了并发系统模型检测与验证技术的应用。将组合可达性分析和标号迁移系统的模块化思想与模型验证技术相结合,提出了一套有效的性质验证方法。论证、分析了三个并发系统安全性和活性验证定理,据此导出了并发系统的安全性与活性验证的有效算法。并通过一个简单实例,对算法有效性进行了初步验证。
|
| 关 键 词： | 并发系统 安全性 活性 组合可达性 标号迁移系统 |
| 文章编号： | 1002-8331（2008）04-0107-04 |
| 收稿时间： | 2007-08-10 |
| 修稿时间： | 2007-11-13 |
Verification of safety and liveness property based on concurrent system |
| |
| 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. |
| |
| Authors: | LI Yang CHENG Jian-hua FANG Ding-yi CHEN Xiao-jiang FENG Jian |
| |
| Affiliation: | 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 |
| |
| Abstract: | |
| |
| Keywords: | concurrent system safety liveness compositional reachability analysis labeled transition system |
| 本文献已被 CNKI 维普 万方数据 等数据库收录！ |
| 点击此处可从《计算机工程与应用》浏览原始摘要信息 |
|
点击此处可从《计算机工程与应用》下载全文 |
|
