Computing Reviews
Today's Issue Hot Topics Search Browse Recommended My Account Log In
Review Help
Search
Formal verification and quantitative metrics of MPSoC data dynamics
Zhang H., Wu J. Formal Aspects of Computing30 (2):219-237,2018.Type:Article
Date Reviewed: Jun 7 2018

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.

Reviewer:  George Hacken Review #: CR146071 (1808-0426)
1) Pnueli, A. The temporal logic of programs. In Proceedings of the 18th Annual Symposium on Foundations of Computer Science (Washington, DC), IEEE, 1977, 46–57 .
Bookmark and Share
  Featured Reviewer  
 
Verification (B.1.4 ... )
 
Would you recommend this review?
yes
no
Other reviews under "Verification": Date
Modelling and verification of weighted spiking neural systems
Aman B., Ciobanu G. Theoretical Computer Science 623(C): 92-102, 2016. Type: Article
Jul 13 2016

E-Mail This Printer-Friendly
Send Your Comments
Contact Us
Reproduction in whole or in part without permission is prohibited.   Copyright 1999-2024 ThinkLoud®
Terms of Use
| Privacy Policy