MPSoC stands for “multiprocessor system-on-a-chip.” This paper treats verification via simulation of the design and expected behavior of such multiprocessor, multitasking systems.

The proposed approach combines hybrid automata with probabilistic timed automata in modeling elements of scheduling, concurrency, and probability of task execution. The (new) reach-ratio metric supplements safety, liveness, and fairness properties of concurrent systems, and is, in essence, the probability “of starting a task from which a certain area of the state space can be reached.” Probabilistic timed automata model tasks retry upon their failure to obtain critical resources for further execution. An application’s task interdependencies and the scheduling arbiter’s policy (rate monotonic, fixed priority, or earliest deadline first) figure in to the best- and worst-case timings of a model’s set of tasks.

Section 3 motivates the paper’s probabilistic hybrid automaton’s specific definition, following an illustrative analysis of a scheduler that has probability 0.95 for successful acquisition of resources. The formal discipline of temporal logic is among those cited [1], but is erroneously attributed to the year 2012 (its Turing-Award-winning work was published in the late 1970s). The diamond and box temporal logic operators are used in section 5 to compute the reach set and the reach ratio. The formal model-checking algorithm for a (state space) trajectory’s reach set is listed in section 5, and is followed by pseudocode for the reach ratio.

The paper’s diverse array of techniques and semi-formal proofs works well in illustrating the state of the art of its subject. The authors’ reach ratio seems promising in the modeling and quantification of MPSoC data dynamics.