| 基于CTL和Petri网的约束一致性验证方法研究 | |
| 张斌 ; 罗贵明 ; Zhang Bin ; Luo Guiming | |
| 2010-06-09 ; 2010-06-09 | |
| 关键词 | CTL Petri Net 约束 一致性 CTL, Petri Net, onstraint, consistency TP301 |
| 其他题名 | Research on Constraint Consistency Based on CTL and Petri Net |
| 中文摘要 | 通过分支时序逻辑(CTL)公式表示系统约束,利用Petri网的可达性分析技术来验证约束一致性是一种重要的、切实可行的约束一致性验证方法。文章描述了一种由CTL公式向Petri网映射的算法,将表示系统约束和组件约束的CTL公式分别映射为Petir网,然后利用Petri网的组合、可达性分析等技术从语义上来验证系统约束与组件约束的一致性。最后,通过对算法的实现开发了一个工具包,并通过一个实例验证了算法正确性和约束一致性验证方法的可行性。; It's an important and practical constraint consistency verification method to express system constraintion byCTL and to verify consistency of constraint by reachability analysis technique of petri- net.In this paper, we describe analgorithm about mapping a CTL formula to petri- net.The CTL formula which indicates system constraint and componentconstraint will be mapped to petri- net.And consistency of system constraint and component constraint will be verified insemantic by techniques of combination of petri- net and reachability analysis.At last, a toolkit will be realized for thisalgorithm.Further more, he correctness of algorithm and the feasibility of method of constraint consistency verificationwill also be verified by a sample with the toolkit.; 国家自然科学基金资助项目(编号:NSFC:60474026); 清华大学基础基金资助项目 |
| 语种 | 中文 ; 中文 |
| 内容类型 | 期刊论文 |
| 源URL | [http://hdl.handle.net/123456789/56491]  |
| 专题 | 清华大学 |
| 推荐引用方式 GB/T 7714 | 张斌,罗贵明,Zhang Bin,等. 基于CTL和Petri网的约束一致性验证方法研究[J],2010, 2010. |
| APA | 张斌,罗贵明,Zhang Bin,&Luo Guiming.(2010).基于CTL和Petri网的约束一致性验证方法研究.. |
| MLA | 张斌,et al."基于CTL和Petri网的约束一致性验证方法研究".(2010). |
| 个性服务 |
| 查看访问统计 |
| 相关权益政策 |
| 暂无数据 |
| 收藏/分享 |
除非特别说明，本系统中所有内容都受版权保护，并保留所有权利。
修改评论