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.