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.
