Formal Verification for Reliability and Performance on Core Coordination of MPSoC

zhanghui; wujinzhao; xieying; caojunyue

您当前的位置：

首页 >

文章列表页 >

Formal Verification for Reliability and Performance on Core Coordination of MPSoC

更新时间：2023-11-14

- Formal Verification for Reliability and Performance on Core Coordination of MPSoC
- Advanced Engineering Sciences Vol. 48, Issue 3, Pages: 107-114(2016)
- 作者机构：
  
  1. 中国科学院成都计算机应用研究所
  2. 广西民族大学广西混杂计算与集成电路设计分析重点实验室
- 作者简介：
- 基金信息：
- DOI：
  CLC：
- Published：2016，
  
  Published Online：21 March 2016，
扫描看全文
张晖,吴尽昭,谢盈,曹俊月.MPSoC核协调可靠性和性能的形式化验证[J].工程科学与技术,2016,48(3):107-114.

zhanghui, wujinzhao, xieying, et al. Formal Verification for Reliability and Performance on Core Coordination of MPSoC. [J]. Advanced Engineering Sciences 48(3):107-114(2016)
张晖,吴尽昭,谢盈,曹俊月.MPSoC核协调可靠性和性能的形式化验证[J].工程科学与技术,2016,48(3):107-114. DOI：

zhanghui, wujinzhao, xieying, et al. Formal Verification for Reliability and Performance on Core Coordination of MPSoC. [J]. Advanced Engineering Sciences 48(3):107-114(2016) DOI：

摘要

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

Abstract

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.

关键词

片上多核处理器核协调混杂变迁系统混杂马尔科夫决策过程随机时序逻辑PRISM模型检测器数据脱敏

Keywords

multiprocessor system-on-chipcore coordinationhybrid labelled transition systemhybrid markov decision processprobabilistic computation tree logicPRISMdata desensitization

references

更多指标>

Views

1634

下载量

CNKI被引量

Alert me when the article has been cited

提交

Tools

Publicity Resources

No data

Related Author

No data

Related Institution

No data

⁰