###
DOI:
工程科学与技术:2016,48(3):107-114
←前一篇   |   后一篇→
本文二维码信息
码上扫一扫!
MPSoC核协调可靠性和性能的形式化验证
(1.中国科学院成都计算机应用研究所;2.广西民族大学 广西混杂计算与集成电路设计分析重点实验室)
Formal Verification for Reliability and Performance on Core Coordination of MPSoC
(1.Chengdu Institute of Computer Application, Chinese Academy of Sciences;2.Guangxi Key Laboratory of Hybrid Computational and IC Design Analysis, Guangxi Uni-versity for Nationalities)
摘要
图/表
参考文献
相似文献
本文已被:浏览 1127次   下载 365
投稿时间:2015-12-14    修订日期:2016-03-21
中文摘要: 为了在早期发现片上多核处理器(MPSoC)设计缺陷,本文提出了一种对核协调进行结构建模和性质刻画的形式化方法。在标记变迁系统中引入多项式函数替代动作表达核协调过程中对数据的改变,加入物理元器件发生故障的概率属性,形成用以描述核协调可靠性和性能的混杂马尔科夫决策过程模型。采用随机时序逻辑刻画系统性质,通过模型检测工具验证分析,以银行数据脱敏MPSoC为例,分析系统可靠性和时间延迟与能耗等性能指标。这些验证结果对于早期MPSoC设计人员具有较强的指导作用。
Abstract:In order to discover MPSoC's design defect earlier, a formal method for depicting core coordination was proposed, including structural model and logical characterization. The main idea was to adopt polynomial functions to replace actions on labelled transition system to describe data changes among different states. Combining with the malfunctioning probability of physical components, a hybrid Markov decision process model was formulated to describe the reliability and performance of the core coordination. Then system properties was depicted by the probabilistic computation tree logic and verified by model checker. Finally, an experiment using data desensitization MPSoC in banks was carried out and a result including the system reliability and time latency as well as power consumption was analyzed. The study is valuable for early MPSoC designers.
文章编号:201501347     中图分类号:    文献标志码:
基金项目:国家自然科学基金项目(11371003,11461006);广西科技基金项目(10169-1);广西自然科学基金(2012GXNSFGA060003);广西教育厅科研项目(201012MS274)
作者简介:
引用文本:
张晖,吴尽昭,谢盈,曹俊月.MPSoC核协调可靠性和性能的形式化验证[J].工程科学与技术,2016,48(3):107-114.
zhanghui,wujinzhao,xieying,caojunyue.Formal Verification for Reliability and Performance on Core Coordination of MPSoC[J].Advanced Engineering Sciences,2016,48(3):107-114.