论文部分内容阅读
为了确保软件分析与设计阶段UML2.0序列图模型的可靠性,采用命题投影时序逻辑（propositional projection temporal logic,简称PPTL）模型检测方法对该模型进行分析和验证.提出了事件确定有限自动机（event deterministic finite automata,简称ETDFA）,并使用该自动机为序列图建立形式化模型,通过给出的基于ETDFA的PPTL模型检测算法得到验证结果.该方法可以在基于Spin的PPTL模型检测器的支持下实现.实例结果表明,该方法可以验证