MPSoC核协调可靠性和性能的形式化验证

• 作者: 吴尽昭 张晖 曹俊月 谢盈
• 来源期刊: 四川大学学报（工程科学版）
• 学科: 工学
• 关键词: 片上多核处理器 核协调 混杂变迁系统 混杂马尔科夫决策过程 随机时序逻辑 PRISM模型检测器 数据脱敏
• 年，卷（期）: 2016,（3）
• 所属期刊栏目: 信息工程
• 页码范围: 107-114
• 页数: 8页
• 分类号: TP301
• 字数: 6417字
• 语种: 中文
• DOI: 10.15961/j.jsuese.2016.03.014

摘要

为了在早期发现片上多核处理器(MPSoC)设计缺陷,提出一种对核协调进行结构建模和性质刻画的形式化方法.在标记变迁系统中引入多项式函数替代动作表达核协调过程中对数据的改变,加入物理元器件发生故障的概率属性,形成用以描述核协调可靠性和性能的混杂马尔科夫决策过程模型.采用随机时序逻辑刻画系统性质,通过模型检测工具验证分析,以银行数据脱敏MPSoC为例,分析系统可靠性和时间延迟与能耗等性能指标.这些验证结果对于早期MPSoC设计人员具有较强的指导作用.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	谢盈	中国科学院成都计算机应用研究所	4	1	1.0	1.0
5	吴尽昭	广西民族大学广西混杂计算与集成电路设计分析重点实验室	23	39	4.0	5.0
6	张晖	中国科学院成都计算机应用研究所	12	54	5.0	7.0
15	曹俊月	中国科学院成都计算机应用研究所	1	1	1.0	1.0