论文部分内容阅读
Petri网是一种既有直观的图形表示方式，又有严格数学理论基础和多种分析方法的建模工具。使用Petri网的分析方法可以刻画系统的结构，展现系统的运行机制，表示和分析系统的动态行为。带有对象的Petri网(PNO)是将面向对象方法和谓词／变迁网有机结合而定义的一种高级Petri网。因为PNO在初始化和验证具体系统时才构建库所的标识关系，变迁的使能与对象状态相关，并且变迁的实施需要修改托肯和相关对象的属性，因此不便于直接使用常规的分析技术验证PNO模型。 针对PNO模型存在的分析验证问题，本文将时态逻辑引入PNO模型，提出了相应的建模及验证方法。建模方法使用精确标识PNO描述系统体系结构模型，并通过时态逻辑定义模型上的需求和限制。验证方法使用SMV工具验证PNO模型和时态逻辑之间的一致性，该方法包括三个步骤。首先，根据SMV的要求在模型中增加与变迁有关的对象属性，并根据增加的对象属性细化变迁附加条件函数和变迁实施处理函数。其次，使用时态逻辑公式描述系统的属性。最后，通过算法PNO2SMV将PNO模型转换成SMV程序表示的有限变迁系统，以验证有限变迁系统是否满足系统属性对应的逻辑公式，从而确保了系统设计的正确性。 本文将上述建模及验证方法应用在列车运行模型(TOPNO)上，通过在某一列车运行区域和列车运行图实例上的应用表明：使用本文提出的建模及验证方法可以在系统开发过程的更早阶段揭示潜在的问题，确保系统设计的正确性，从而实现系统设计和分析验证之间的高度完整性。