中国科学院软件研究所机构知识库
Advanced  
ISCAS OpenIR  > 互联网软件技术实验室  > 期刊论文
题名:
参数化系统安全性的启发式符号验证
其他题名: heuristic symbolic verification of safety properties for parameterized systems
作者: 杨秋松 ; 李明树
关键词: 参数化系统 ; 安全性 ; 向上封闭集合 ; 启发式搜索 ; 符号验证
刊名: 软件学报
发表日期: 2009
卷: 20, 期:6, 页:1444-1456
收录类别: ei
部门归属: 互联网软件技术实验室
摘要: 参数化系统(paramterized system)是指包含特定有限状态进程多个实例的并发系统,其中的参数是指系统内进程实例的数目,即系统的规模.反向可达性分析(backward reachability analysis)已被广泛用于验证参数化系统是否满足以向上封闭(upward-closed)集合表示的安全性(safety property).与有限状态系统验证相类似,参数化系统的验证同样也面临着状态爆炸(state explosion)问题,并且模型检测算法的有效性依赖于如何采用有效的数据结构表示状态集合.针对表示无穷状态的向上封闭集合,研究人员提出了多种基于约束(constraint-based)的符号表示方法.但这些方法依然面临着符号状态爆炸(symbolic state explosion)问题或者其包含判定问题,即判断一个约束条件集合符号化表示的实际状态集合是否为另一约束条件集合所对应的状态集合的子集,是Co-NP完全问题.因此,虽然有限状态验证技术能够验证一些具有一定规模的问题,但现有针对参数化系统的验证方法所能解决的问题的规模较为有限,需要近一步提高模型检测算法的效率.针对参数化系统提出了加快反向可达性分析的多个启发式规则,实验结果表明,这些启发式规则可以使算法的效率提高几个数量级,从而有助于解决现有参数化系统验证方法所存在的问题.
语种: 中文
内容类型: 期刊论文
URI标识: http://ir.iscas.ac.cn/handle/311060/2699
Appears in Collections:互联网软件技术实验室 _期刊论文

Files in This Item:
File Name/ File Size Content Type Version Access License
200920061444.pdf(504KB)----限制开放-- 联系获取全文

Recommended Citation:
杨秋松,李明树. 参数化系统安全性的启发式符号验证[J]. 软件学报,2009-01-01,20(6):1444-1456.
Service
Recommend this item
Sava as my favorate item
Show this item's statistics
Export Endnote File
Google Scholar
Similar articles in Google Scholar
[杨秋松]'s Articles
[李明树]'s Articles
CSDL cross search
Similar articles in CSDL Cross Search
[杨秋松]‘s Articles
[李明树]‘s Articles
Related Copyright Policies
Null
Social Bookmarking
Add to CiteULike Add to Connotea Add to Del.icio.us Add to Digg Add to Reddit
所有评论 (0)
暂无评论
 
评注功能仅针对注册用户开放,请您登录
您对该条目有什么异议,请填写以下表单,管理员会尽快联系您。
内 容:
Email:  *
单位:
验证码:   刷新
您在IR的使用过程中有什么好的想法或者建议可以反馈给我们。
标 题:
 *
内 容:
Email:  *
验证码:   刷新

Items in IR are protected by copyright, with all rights reserved, unless otherwise indicated.

 

 

Valid XHTML 1.0!
Copyright © 2007-2017  中国科学院软件研究所 - Feedback
Powered by CSpace