×

Formal verification and quantitative metrics of MPSoC data dynamics. (English) Zbl 1382.68145

Summary: 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.

MSC:

68Q60 Specification and verification (program logics, model checking, etc.)
68Q45 Formal languages and automata
PDF BibTeX XML Cite
Full Text: DOI

References:

[1] 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-229
[2] Alur, R; Henzinger, TA; Ho, PH, Automatic symbolic verification of embedded systems, IEEE Trans Softw Eng, 22, 181-201, (1996)
[3] Asarin, E; Bournez, O; Dang, T; Maler, O; Pnueli, A, Effective synthesis of switching controllers for linear systems, Proc IEEE, 88, 1011-1025, (2000)
[4] 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-148
[5] Brekling, A; Hansen, MR; Madsen, J, Models and formal verification of multiprocessor system-on-chips, J Log Algebr Program, 77, 1-19, (2008) · Zbl 1151.68339
[6] Chutinan A (1999) Hybrid system verification using discrete model approximations. Ph.D. thesis, Carnegie Mellon University · Zbl 0954.93020
[7] Davoren, JM; Nerode, A, Logics for hybrid systems, Proc IEEE, 88, 985-1010, (2000)
[8] 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-329
[9] 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-273 · Zbl 1078.93533
[10] 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-395
[11] 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-305 · Zbl 1078.93005
[12] 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-197
[13] 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-292 · Zbl 0959.68073
[14] Henzinger, TA; Ho, PH; Wong-Toi, H, Algorithmic analysis of nonlinear hybrid systems, IEEE Trans Autom Control, 43, 540-554, (1998) · Zbl 0918.93019
[15] 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-209
[16] Kurzhanskiy, AA; Varaiya, P, Ellipsoidal techniques for reachability analysis of discrete-time linear systems, IEEE Trans Autom Control, 52, 26-38, (2007) · Zbl 1366.93039
[17] Kwiatkowska, M; Norman, G; Segala, R; Sproston, J, Automatic verification of real-time systems with discrete probability distributions, Theor Comput Sci, 282, 101-150, (2002) · Zbl 1050.68094
[18] Kwiatkowska M, Norman G, Sproston J (2002) Probabilistic model checking of the IEEE 802.11 wireless local area network protocol. Springer, Berlin, pp 411-423 · Zbl 1065.68583
[19] Kwiatkowska, M; Norman, G; Parker, D; Sproston, J, Performance analysis of probabilistic timed automata using digital clocks, Form Methods Syst Des, 29, 33-78, (2006) · Zbl 1105.68063
[20] Kwiatkowska, M; Norman, G; Sproston, J; Wang, F, Symbolic model checking for probabilistic timed automata, Inf Comput, 205, 1027-1077, (2007) · Zbl 1122.68075
[21] 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-227 · Zbl 1262.68125
[22] Kwiatkowska M, Norman G, Parker D (2011) Prism 4.0: verification of probabilistic real-time systems. Springer, Snowbird, pp 585-591
[23] Le Guernic C, Girard A (2009) Reachability analysis of hybrid systems using support functions. In: Computer aided verification. Springer, Berlin, pp 540-554 · Zbl 1242.93059
[24] Li, T; Tan, F; Wang, Q; Bu, L; Cao, Jn; Liu, X, 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, 642-652, (2014)
[25] 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-264
[26] Manna Z, Pnueli A (2012) Temporal verification of reactive systems: safety. Springer Science and Business Media · Zbl 1288.68169
[27] 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-360
[28] 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-233 · Zbl 1170.68523
[29] Platzer, A, Differential dynamic logic for hybrid systems, J Autom Reason, 41, 143-189, (2008) · Zbl 1181.03035
[30] Ratschan, S; She, Z, Safety verification of hybrid systems by constraint propagation-based abstraction refinement, ACM Trans Embed Comput Syst (TECS), 6, 8, (2007) · Zbl 1078.93508
[31] Sha, L; Rajkumar, R; Sathaye, SS, Generalized rate-monotonic scheduling theory: a framework for developing real-time systems, Proc IEEE, 82, 68-82, (1994)
[32] 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-45 · Zbl 0986.68058
[33] Sankaranarayanan, S; Sipma, HB; Manna, Z, Non-linear loop invariant generation using Gröbner bases, ACM SIGPLAN Not, 39, 318-329, (2004) · Zbl 1325.68071
[34] 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 York · Zbl 0931.68136
[35] Visintini, AL; Glover, W; Lygeros, J; Maciejowski, J, Monte Carlo optimization for conflict resolution in air traffic control, IEEE Trans Intell Transp Syst, 7, 470-482, (2006) · Zbl 1115.90062
[36] Wolf, W, Multiprocessor system-on-chip technology, IEEE Signal Process Mag, 26, 50-54, (2009)
[37] Yang, H; Kim, S; Ha, S, An milp-based performance analysis technique for non-preemptive multitasking mpsoc, IEEE Trans Comput Aided Des Integr Circuits Syst, 29, 1600-1613, (2010)
[38] 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-40
[39] 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-2199
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.