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

Formal Verification for Reliability and Performance on Core Coordination of MPSoC

为了在早期发现片上多核处理器(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.