论文部分内容阅读
扩展了基本Petri网,提出了更加适合模型检测的MCPN方法,并将MCPN模型转换成模型检测工具SPIN的输入语言———PROMELA。使用SPIN完成对系统模型的检测,以提高软件设计的可靠性。在转换过程中,考虑了对当前情态下处于激活状态的多个变迁的同时激发;并提出了一种处理Petri网公平性问题的解决方案。