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

摘要：

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

关键词： 模型检验 实时系统模型 实时约束 WCET分析 计算机系统

作者: 张曦 董威

作者单位: 国防科学技术大学计算机学院 湖南 长沙 410073

会议类型: 国内会议

会议名称: 2011(第四届)全国网络与信息安全学术会议

会议地点: 北京

会议语种:中文

页码: 115-120

在线出版日期: 2011-07-01（万方平台首次上网日期，不代表论文的发表时间）