MPSoC核协调可靠性和性能的形式化验证
为了在早期发现片上多核处理器(MPSoC)设计缺陷,提出一种对核协调进行结构建模和性质刻画的形式化方法.在标记变迁系统中引入多项式函数替代动作表达核协调过程中对数据的改变,加入物理元器件发生故障的概率属性,形成用以描述核协调可靠性和性能的混杂马尔科夫决策过程模型.采用随机时序逻辑刻画系统性质,通过模型检测工具验证分析,以银行数据脱敏MPSoC为例,分析系统可靠性和时间延迟与能耗等性能指标.这些验证结果对于早期MPSoC设计人员具有较强的指导作用.
片上多核处理器、核协调、混杂变迁系统、混杂马尔科夫决策过程、随机时序逻辑、PRISM模型检测器、数据脱敏
48
TP301(计算技术、计算机技术)
国家自然科学基金资助项目11371003,11461006;广西科技基金项目10169-1;广西自然科学基金项目2012GXNSFGA060003;广西教育厅科研项目201012MS274
2016-06-27（万方平台首次上网日期，不代表论文的发表时间）
共8页
107-114
