基于WCET分析技术的模型检验方法研究

传统的模型检验技术能够表示出实时系统的性质和规范，但是实时系统的实时约束大多基于抽象层次的实时模型来描述，无法与具体的程序相关联，难以体现系统的实际运行效果。本文以某航天程序为例，通过TCTL建立系统模型，在此基础上引入WCET技术，将模型的状态和实时约束对应到具体的程序片段上，分析了程序片段的最差情况执行时间并反馈到系统模型中。增强了模型的描述能力，为软件系统的进一步升级和维护提供支持。