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

• 作者: 张曦 董威
• 来源期刊: 中国电子商情·通信市场
• 学科: 工学
• 关键词: 模型检验 实时系统 TLTL WCET
• 年，卷（期）: 2011,（3）
• 所属期刊栏目: 优秀论文
• 页码范围: 115-120
• 分类号: TP316.2
• 字数: 2487字
• 语种: 中文
• DOI: 10.3969/j.issn.1006-6675-B.2011.03.015

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	董威	国防科学技术大学计算机学院	32	402	10.0	19.0
2	张曦	国防科学技术大学计算机学院	2	1	1.0	1.0