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

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