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

摘要：针对工作流网建模过程中节点精化方法只能扩展单节点的局限性,提出一种基于Petri网合成规则的工作流网精化方法.在活的和有界的自由选择网合成规则上添加限制,使其适用于自由选择工作流网的精化,定义可分离工作流网及其保持可分离性的合成规则,证明在自由选择或可分离工作流网上应用合成规则所生成工作流网的合理性.使这两类工作流网的精化能够一次涉及多个节点,为其建模提供维度不同且粒度更细的参考原则.