Formal Aspects of Computing

, Volume 30, Issue 2, pp 219–237 | Cite as

Formal verification and quantitative metrics of MPSoC data dynamics

Original Article
  • 10 Downloads

Abstract

Multiprocessor system on chip (MPSoC) implements system functions through tasks. It is necessary to estimate system behaviors early in the design process without actual hardware implementation. As there are a huge variety in freedom of choices in the mapping of tasks, existing researches mainly focus on the schedulability analysis and resource constraints, with a lack of concerning on how data in tasks “behaves” in different schedulings. In practical applications, tasks are achieved by sequential executions of code blocks, which change the variables accordingly. Some variables are shared by all the tasks through global memory, such as public data, critical signals and so on. Changes of these data reflect functions of the system which also deserves attention. Data dynamics can illustrate data changes within a task as well as data exchanges between tasks, and thus can depict scheduling with more detail than just telling whether they can be scheduled. This paper proposes a new formal approach by combing hybrid automata and probabilistic timed automata to model MPSoC data dynamics, describing its real-time scheduling characteristics, concurrency, and probability. Furthermore, we also propose a new quantitative metric for measuring data dynamics named “reach-ratio” to compute the probability, weighted over tasks, of starting a task from which a certain area of the state space can be reached, where the tasks must be started within a time-bound that varies from task to task. The reach-ratio metric, as a supplement of traditional properties such as safety, liveness and fairness, reflects the extent of which the system achieves the intended function at a given scheduling strategy. Case study investigations of our new formal approach provide empirical evidence for MPSoC designers to balance controller policy without hardware implementation.

Keywords

Formal verification Data dynamics MPSoC Hybrid automata Probabilistic timed automata Reach-ratio metric 

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. ACH93.
    Alur R, Courcoubetis C, Henzinger TA, Ho PH (1993) Hybrid automata: an algorithmic approach to the specification and verification of hybrid systems. Springer, Berlin, pp 209–229Google Scholar
  2. AHH96.
    Alur R, Henzinger TA, Ho PH (1996) Automatic symbolic verification of embedded systems. IEEE Trans Softw Eng 22(3): 181–201CrossRefGoogle Scholar
  3. ABD00.
    Asarin E, Bournez O, Dang T, Maler O, Pnueli A (2000) Effective synthesis of switching controllers for linear systems. Proc IEEE 88(7): 1011–1025CrossRefGoogle Scholar
  4. BJC14.
    Bak S, Johnson TT, Caccamo M, Sha L (2014) Real-time reachability for verified simplex design. In: Real-time systems symposium (RTSS),2014 IEEE, pp 138–148Google Scholar
  5. BHM08.
    Brekling A, Hansen MR, Madsen J (2008) Models and formal verification of multiprocessor system-on-chips. J Log Algebr Program 77(1): 1–19MathSciNetCrossRefMATHGoogle Scholar
  6. Chu99.
    Chutinan A (1999) Hybrid system verification using discrete model approximations. Ph.D. thesis, Carnegie Mellon UniversityGoogle Scholar
  7. DN00.
    Davoren JM, Nerode A (2000) Logics for hybrid systems. Proc IEEE 88(7): 985–1010CrossRefGoogle Scholar
  8. DT98.
    Daws C, Tripakis S (1998) Model checking of real-time reachability properties using abstractions. In: Tools and algorithms for the construction and analysis of systems. Springer, Berlin, pp 313–329Google Scholar
  9. Fre05.
    Frehse G (2005) PHAVer: algorithmic verification of hybrid systems past HyTech. In: Morari M, Thiele L (eds) Hybrid systems: computation and control, vol 3414, Lecture Notes in Computer Science. Springer, Berlin, pp 258–273Google Scholar
  10. FLD11.
    Frehse G, Le Guernic C, Donzé A, Cotton S, Ray R, Lebeltel O, Ripado R, Girard A, Dang T, Maler O (2011) Spaceex: Scalable verification of hybrid systems. In: Computer aided verification. Springer, Berlin, pp 379–395Google Scholar
  11. Gir05.
    Girard A (2005) Reachability of uncertain linear systems using zonotopes. In: Morari M, Thiele L (eds) Hybrid systems: computation and control, vol 3414, Springer, Berlin, pp 291–305Google Scholar
  12. Guz05.
    Gu Z (2005) Solving real-time scheduling problems with model-checking. In: Yang LT, Zhou X, Zhao W, Wu Z, Zhu Y, Lin M (eds) Embedded software and systems, proceedings, vol 3820. Springer, Berlin, pp 186–197Google Scholar
  13. Hen00.
    Henzinger TA (2000) The theory of hybrid automata. In: Inan MK, Kurshan RP (eds) Verification of digital and hybrid system, vol 170. Springer, Berlin, pp 265–292Google Scholar
  14. HHW98.
    Henzinger TA, Ho PH, Wong-Toi H (1998) Algorithmic analysis of nonlinear hybrid systems. IEEE Trans Autom Control 43(4): 540–554MathSciNetCrossRefMATHGoogle Scholar
  15. Leh90.
    Lehoczky JP. (1990) Fixed priority scheduling of periodic task sets with arbitrary deadlines. In: Real-time systems symposium, Lake Buena Vista, Florida, 1990. IEEE, pp 201–209Google Scholar
  16. KV07.
    Kurzhanskiy AA, Varaiya P (2007) Ellipsoidal techniques for reachability analysis of discrete-time linear systems. IEEE Trans Autom Control 52(1): 26–38MathSciNetCrossRefMATHGoogle Scholar
  17. KNS02.
    Kwiatkowska M, Norman G, Segala R, Sproston J (2002) Automatic verification of real-time systems with discrete probability distributions. Theor Comput Sci 282(1): 101–150MathSciNetCrossRefMATHGoogle Scholar
  18. KNS02+.
    Kwiatkowska M, Norman G, Sproston J (2002) Probabilistic model checking of the IEEE 802.11 wireless local area network protocol. Springer, Berlin, pp 411–423MATHGoogle Scholar
  19. KNP06.
    Kwiatkowska M, Norman G, Parker D, Sproston J (2006) Performance analysis of probabilistic timed automata using digital clocks. Form Methods Syst Des 29(1): 33–78CrossRefMATHGoogle Scholar
  20. KNS07.
    Kwiatkowska M, Norman G, Sproston J, Wang F (2007) Symbolic model checking for probabilistic timed automata. Inf Comput 205(7): 1027–1077MathSciNetCrossRefMATHGoogle Scholar
  21. KNP09.
    Kwiatkowska M, Norman G, Parker D (2009) Stochastic games for verification of probabilistic timed automata. In: Formal modeling and analysis of timed systems. Springer, Berlin, pp 212–227Google Scholar
  22. KNP11.
    Kwiatkowska M, Norman G, Parker D (2011) Prism 4.0: verification of probabilistic real-time systems. Springer, Snowbird, pp 585–591Google Scholar
  23. LG09.
    Le Guernic C, Girard A (2009) Reachability analysis of hybrid systems using support functions. In: Computer aided verification. Springer, Berlin, pp 540–554Google Scholar
  24. LTW14.
    Li T, Tan F, Wang Q, Bu L, Cao Jn, Liu X (2014) From offline toward real time: a hybrid systems model checking and CPS codesign approach for medical device plug-and-play collaborations. IEEE Trans Parallel Distrib Syst 25(3): 642–652CrossRefGoogle Scholar
  25. MDA09.
    Madl G, Dutt N, Abdelwahed S (2009) A conservative approximation method for the verification of preemptive scheduling using timed automata. In: 15th IEEE real-time and embedded technology and applications symposium, pp 255–264Google Scholar
  26. MP12.
    Manna Z, Pnueli A (2012) Temporal verification of reactive systems: safety. Springer Science and Business MediaGoogle Scholar
  27. MKY05.
    Mutsuda Y, Kato T, Yamane S (2005) Specification and verification techniques of embedded systems using probabilistic linear hybrid automata. In: Embedded software and systems. Springer, pp 346–360Google Scholar
  28. MPM05.
    Mysore V, Piazza C, Mishra B (2005) Algorithmic algebraic model checking II: Decidability of semi-algebraic model checking and its applications to systems biology. In: Automated technology for verification and analysis. Springer, pp 217–233Google Scholar
  29. Pla08.
    Platzer A (2008) Differential dynamic logic for hybrid systems. J Autom Reason 41(2): 143–189MathSciNetCrossRefMATHGoogle Scholar
  30. RS07.
    Ratschan S, She Z (2007) Safety verification of hybrid systems by constraint propagation-based abstraction refinement. ACM Trans Embed Comput Syst (TECS) 6(1): 8CrossRefMATHGoogle Scholar
  31. SRS94.
    Sha L, Rajkumar R, Sathaye SS (1994) Generalized rate-monotonic scheduling theory: a framework for developing real-time systems. Proc IEEE 82((1): 68–82Google Scholar
  32. Spr00.
    Sproston J (2000) Decidable model checking of probabilistic hybrid automata. In: Joseph M (ed) Formal techniques in real-time and fault-tolerant systems, proceedings, vol 1926. Springer, Berlin, pp 31–45Google Scholar
  33. SSM04.
    Sankaranarayanan S, Sipma HB, Manna Z (2004) Non-linear loop invariant generation using gröbner bases. ACM SIGPLAN Not 39(1): 318–329CrossRefMATHGoogle Scholar
  34. SSR98.
    Stankovic JA, Spuri M, Ramamritham K, Buttazzo G (1998) Deadline scheduling for real-time systems: EDF and related algorithms, vol 460. Springer Science and Business Media, New YorkCrossRefMATHGoogle Scholar
  35. VGL06.
    Visintini AL, Glover W, Lygeros J, Maciejowski J (2006) Monte carlo optimization for conflict resolution in air traffic control. IEEE Trans Intell Transp Syst 7(4): 470–482CrossRefMATHGoogle Scholar
  36. Wol09.
    Wolf W (2009) Multiprocessor system-on-chip technology. IEEE Signal Process Mag 26(6): 50–54CrossRefGoogle Scholar
  37. YKH10.
    Yang H, Kim S, Ha S (2010) An milp-based performance analysis technique for non-preemptive multitasking MPSoC. IEEE Trans Comput Aided Des Integr Circuits Syst 29(10): 1600–1613CrossRefGoogle Scholar
  38. ZWT14.
    Zhang H, Wu J, Tan H, Yang H (2014) Approximate trace equivalence of real-time linear algebraic transition systems. Comput Model New Technol 18(7):36–40Google Scholar
  39. ZWT16.
    Zhang H, Wu J, Lu J, Tang J (2016) Safety verification of finite real-time nonlinear hybrid systems using enhanced group preserving scheme. Cluster Comput 19(4):2189–2199Google Scholar

Copyright information

© British Computer Society 2017

Authors and Affiliations

  1. 1.Chengdu Institute of Computer ApplicationChinese Academy of SciencesChengduChina
  2. 2.University of Chinese Academy of SciencesBeijingChina
  3. 3.Guizhou Bank Postdoctoral StationGuiyangChina
  4. 4.Guangxi Key Laboratory of Hybrid Computational and IC Design AnalysisGuangxi University for NationalitiesGuangxiChina

Personalised recommendations