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