一种基于System C语言的模型检测方法

• 作者: 于琼 吴丽佳 靳庆庚
• 来源期刊: 广西民族大学学报（自然科学版）
• 学科: 工学
• 关键词: System C 时间自动机 模型检测
• 年，卷（期）: 2016,（3）
• 所属期刊栏目: 计算机技术
• 页码范围: 80-85
• 页数: 6页
• 分类号: TP312
• 字数: 4126字
• 语种: 中文

摘要

System C语言在软硬件协同设计过程中被广泛用来建模和仿真.笔者提出了一种验证System C设计的方法,即通过把System C设计映射成为一个具有良好定义语义的UPPAAL时间自动机.System C设计的结构和非正式定义的行为在形成的UPPAAL时间自动机中得到了完整的保留.产生的UPPAAL模型允许使用UPPAAL模型检查器和其配套工具来进行验证.模型检查器用来验证设计的一些重要属性,比如活性,死锁问题和时间约束属性.通过对两个实例的活性、安全性和时间属性的验证采证明该方法的适用性.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	吴丽佳	广西民族大学广西混杂计算与集成电路设计分析重点实验室	2	1	1.0	1.0
2	靳庆庚	广西民族大学广西混杂计算与集成电路设计分析重点实验室	6	3	1.0	1.0
3	于琼	广西民族大学广西混杂计算与集成电路设计分析重点实验室	1	0	0.0	0.0