扩展Petri网：实时系统建模与形式化验证新方法

嵌入式实时系统因其对时间约束性、安全性和可靠性的高度需求，面临着传统建模和形式化验证方法在模拟和验证其复杂特性方面的挑战。本文提出了一种创新的方法，即基于扩展Petri网的系统建模与形式化验证。首先，通过扩展有色Petri网的时间属性，构建了实时有色Petri网模型，这种模型能有效地捕捉和评估系统的实时特性，如截止时间和任务调度。 实时有色Petri网模型引入了颜色标签，以区分不同的执行阶段和优先级，这对于处理嵌入式系统中的并发行为和优先级抢占问题尤为关键。这种模型不仅考虑了系统的行为，还考虑了时间因素，使得分析更加精确。 接着，作者将实时有色Petri网模型映射到时间自动机，通过定义相应的语义转换规则，使得模型可以转化为时间自动机的形式。时间自动机是一种强大的工具，它结合了时间逻辑，如时间计算树逻辑（Temporal Computation Tree Logic, TCTL），用于形式化地验证系统的实时性、安全性以及可靠性。 例如，在实际应用中，作者以列车通信网络控制器的双线冗余控制模块为例，展示了如何运用这一方法进行建模和形式化验证。通过这种方法，验证模块能够在满足系统时间约束的同时，确保其在面临各种故障或异常情况下的安全操作，并验证其可靠性，比如在故障切换时的响应时间。 基于扩展Petri网的建模和形式化验证方法为嵌入式实时系统的设计和验证提供了一个强大的框架，它既考虑了系统的动态行为，又考虑了时间约束，从而提高了系统的质量和安全性。通过本文的研究，作者展示了这种方法的有效性和实用性，为嵌入式系统的开发实践提供了新的思考角度和验证手段。