2011年中国民航大学学报：飞行程序发布订阅Petri网建模与有效性验证

本文主要探讨了飞行程序发布订阅服务在未来的航行情报管理系统中的重要性，以及如何通过UML（统一建模语言）来构建这一服务的概念模型。作者王洁宁和姜高扬针对中国民航大学空中交通管理研究基地的研究，提出了一个详细的系统需求分析框架，着重描绘了发布与订阅过程的逻辑流程。 在概念模型的建立过程中，他们利用UML提供的工具和方法，将系统的交互行为抽象成易于理解的图形表示，使得需求和操作过程清晰可见。这不仅有助于设计人员理解和沟通，也为后续的系统开发提供了明确的指导方向。 接下来，他们将这个概念模型转化为Petri网模型，Petri网是一种强大的数学工具，用于描述系统中事件的发生顺序和资源的分配情况。通过Petri网，可以更精确地模拟发布订阅服务中的并发和消息传递行为。 在模型验证阶段，作者运用了可达树分析和P不变量分析方法。可达树分析用来确定每个状态是否可以通过一系列的转换到达，从而评估模型的完整性。而P不变量分析则有助于检查模型是否满足守衡性，即输入资源的数量始终等于输出资源的数量，保证了系统的稳定性。 通过对所建Petri网模型的有界性、守衡性和活性的分析，作者证明了所构建的概念模型在理论上的正确性和有效性。有界性意味着模型的状态数量是有限的，避免了无限循环；守衡性确保了系统的资源平衡；活性则验证了模型具有响应外部事件的能力，即能够产生预期的行为。 这篇论文提供了一个实际且严谨的方法来处理航行情报管理中的发布订阅服务，展示了Petri网在航空交通管理领域的应用潜力，对于提升航行情报系统的效率和可靠性具有重要意义。