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

Formal Verification for Reliability and Performance on Core Coordination of MPSoC

作　　者：张晖[1,2,3] 吴尽昭[4] 谢盈[1,2] 曹俊月 

机构地区：[1]中国科学院成都计算机应用研究所,四川成都610041 [2]中国科学院大学,北京100049 [3]贵州银行博士后科研工作站,贵州贵阳550001 [4]广西民族大学广西混杂计算与集成电路设计分析重点实验室,广西南宁530006

出　　处：《四川大学学报（工程科学版）》2016年第3期107-114,共8页Journal of Sichuan University (Engineering Science Edition)

基　　金：国家自然科学基金资助项目(11371003;11461006);广西科技基金项目(10169-1);广西自然科学基金项目(2012GXNSFGA060003);广西教育厅科研项目(201012MS274)

摘　　要：为了在早期发现片上多核处理器(MPSoC)设计缺陷,提出一种对核协调进行结构建模和性质刻画的形式化方法。在标记变迁系统中引入多项式函数替代动作表达核协调过程中对数据的改变,加入物理元器件发生故障的概率属性,形成用以描述核协调可靠性和性能的混杂马尔科夫决策过程模型。采用随机时序逻辑刻画系统性质,通过模型检测工具验证分析,以银行数据脱敏MPSoC为例,分析系统可靠性和时间延迟与能耗等性能指标。这些验证结果对于早期MPSoC设计人员具有较强的指导作用。In order to discover MPSoC＇ s design defect earlier, a formal method for depicting core coordination was proposed, which ineluded 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 were 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模型检测器 数据脱敏 

分 类 号：TP301[自动化与计算机技术—计算机系统结构]