基于CTL和Petri网的约束一致性验证方法研究

• 作者: 张斌 罗贵明
• 来源期刊: 计算机工程与应用
• 学科: 工学
• 关键词: CTL Petri Net 约束 一致性
• 年，卷（期）: 2006,（23）
• 所属期刊栏目: 学术探讨
• 页码范围: 52-57
• 页数: 6页
• 分类号: TP311
• 字数: 6905字
• 语种: 中文
• DOI: 10.3321/j.issn:1002-8331.2006.23.015

摘要

通过分支时序逻辑(CTL)公式表示系统约束,利用Petri网的可达性分析技术来验证约束一致性是一种重要的、切实可行的约束一致性验证方法.文章描述了一种由CTL公式向Petri网映射的算法,将表示系统约束和组件约束的CTL公式分别映射为Petri网,然后利用Petri网的组合、可达性分析等技术从语义上来验证系统约束与组件约束的一致性.最后,通过对算法的实现开发了一个工具包,并通过一个实例验证了算法正确性和约束一致性验证方法的可行性.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	张斌	清华大学软件学院	56	870	15.0	28.0
2	罗贵明	清华大学软件学院	19	125	6.0	10.0