×

Parameter synthesis for hierarchical concurrent real-time systems. (English) Zbl 1314.68081

Summary: Modeling and verifying complex real-time systems, involving timing delays, are notoriously difficult problems. Checking the correctness of a system for one particular value for each delay does not give any information for other values. It is thus interesting to reason parametrically, by considering that the delays are parameters (unknown constants) and synthesizing a constraint guaranteeing a correct behavior. We present here Parametric Stateful Timed Communicating Sequential Processes, a language capable of specifying and verifying parametric hierarchical real-time systems with complex data structures. Although we prove that the synthesis is undecidable in general, we present several semi-algorithms for efficient parameter synthesis, which behave well in practice. This work has been implemented in a real-time model checker, PSyHCoS, and validated on a set of case studies.

MSC:

68M20 Performance evaluation, queueing, and scheduling in the context of computer systems
68Q60 Specification and verification (program logics, model checking, etc.)
PDFBibTeX XMLCite
Full Text: DOI Link

References:

[1] Aceto, L.; Bouyer, P.; Burgueño, A.; Larsen, KG; Arvind, V. (ed.); Ramanujam, R. (ed.), The power of reachability testing for timed automata, No. 1530, 245-256 (1998), Berlin
[2] Aceto, L.; Burgueño, A.; Larsen, KG; Steffen, B. (ed.), Model checking via reachability testing for timed automata, No. 1384, 263-280 (1998), Berlin
[3] Adbeddaïm Y, Maler O (2002) Preemptive job-shop scheduling using stopwatch automata. In: Katoen JP, Stevens P (eds) TACAS, lecture notes in computer science, vol 2280. Springer, Berlin, pp 113-126 · Zbl 1043.68510
[4] Adbeddaïm Y, Asarin E, Maler O (2006) Scheduling with timed automata. Theor Comput Sci 354(2):272-300 · Zbl 1088.68023
[5] Akshay S, Hélouët L, Jard C, Reynier PA (2012) Robustness of time Petri nets under guard enlargement. RP, lecture notes in computer science, vol 7550. Springer, Berlin, pp 92-106 · Zbl 1355.68187
[6] Alur R, Dill DL (1994) A theory of timed automata. Theor Comput Sci 126(2):183-235 · Zbl 0803.68071 · doi:10.1016/0304-3975(94)90010-8
[7] Alur, R.; Madhusudan, P.; Bernardo, M. (ed.); Corradini, F. (ed.), Decision problems for timed automata: a survey, No. 3185, 1-24 (2004), Berlin · Zbl 1105.68057
[8] Alur R, Henzinger TA, Vardi MY (1993) Parametric real-time reasoning. In: Kosaraju SR, Johnson DS, Aggarwal A (eds) Proceedings of the twenty-fifth annual ACM symposium on theory of computing, 16-18 May 1993, San Diego, CA. ACM · Zbl 1310.68139
[9] André É (2010) An inverse method for the synthesis of timing parameters in concurrent systems. Ph.d. thesis, Laboratoire Spécification et Vérification, ENS Cachan, France · JFM 12.0076.03
[10] André, É.; Liu, Y. (ed.); Martin, A. (ed.), Observer patterns for real-time systems, 125-134 (2013), Washington, DC
[11] André É, Soulat R (2013) The inverse method. FOCUS series in computer engineering and information technology. ISTE Ltd and John Wiley & Sons Inc · Zbl 1217.68140
[12] André É, Chatain T, Encrenaz E, Fribourg L (2009) An inverse method for parametric timed automata. Int J Found Comput Sci 20(5):819-836 · Zbl 1187.68286 · doi:10.1142/S0129054109006905
[13] André, É.; Fribourg, L.; Kučera, A. (ed.); Potapov, I. (ed.), Behavioral cartography of timed automata, No. 6227, 76-90 (2010), Berlin · Zbl 1287.68089
[14] André É, Fribourg L, Kühne U, Soulat R (2012a) IMITATOR 2.5: a tool for analyzing robustness in scheduling problems. In: FM, lecture notes in computer science, vol 7436. Springer, Berlin, pp 33-36
[15] André, É.; Liu, Y.; Sun, J.; Dong, JS; Perseil, I. (ed.); Pouzet, M. (ed.); Breitman, K. (ed.), Parameter synthesis for hierarchical concurrent real-time systems, 253-262 (2012), Washington, DC
[16] André, É.; Fribourg, L.; Soulat, R.; Hung, DV (ed.); Ogawa, M. (ed.), Merge and conquer: state merging in parametric timed automata, No. 8172, 381-396 (2013), Berlin · Zbl 1410.68194
[17] André, É.; Liu, Y.; Sun, J.; Dong, JS; Lin, SW; Sharygina, N. (ed.); Veith, H. (ed.), PSyHCoS: parameter synthesis for hierarchical concurrent real-time systems, No. 8044, 984-989 (2013), Berlin
[18] André, É.; Petrucci, L.; Pellegrino, G.; Braberman, V. (ed.); Fribourg, L. (ed.), Precise robustness analysis of time Petri nets with inhibitor arcs, No. 8053, 1-15 (2013), Berlin · Zbl 1390.68455
[19] Annichini, A.; Bouajjani, A.; Sighireanu, M., TReX: a tool for reachability analysis of complex systems, No. 2102, 368-372 (2001), Berlin · Zbl 0991.68645
[20] Asarin, E.; Maler, O.; Pnueli, A., On discretization of delays in timed automata and digital circuits, No. 1466, 470-484 (1998), Berlin · Zbl 0933.94045
[21] Bagnara R, Hill PM, Zaffanella E (2008) The Parma Polyhedra Library: toward a complete set of numerical abstractions for the analysis and verification of hardware and software systems. Sci Comput Program 72(1-2):3-21 · doi:10.1016/j.scico.2007.08.001
[22] Baier C, Katoen JP (2008) Principles of model checking. MIT Press, Cambridge, MA · Zbl 1179.68076
[23] Behrmann, G.; Larsen, KG; Rasmussen, JI, Beyond liveness: efficient parameter synthesis for time bounded liveness, No. 3829, 81-94 (2005), Berlin · Zbl 1175.68255
[24] Bengtsson, J.; Yi, W., Timed automata: semantics, algorithms and tools, No. 3098, 87-124 (2004), Berlin · Zbl 1088.68119 · doi:10.1007/978-3-540-27755-2_3
[25] Bérard, B.; Gastin, P.; Petit, A., On the power of non-observable actions in timed automata, No. 1046, 257-268 (1996), Berlin · Zbl 1379.68216
[26] Bérard B, Petit A, Diekert V, Gastin P (1998) Characterization of the expressive power of silent transitions in timed automata. Fundam Inform 36:145-182 · Zbl 0930.68077
[27] Bouyer, P.; Larsen, KG; Markey, N.; Sankur, O.; Thrane, CR; Katoen, JP (ed.); König, B. (ed.), Timed automata can always be made implementable, No. 6901, 76-91 (2011), Berlin · Zbl 1343.68134
[28] Bouyer, P.; Markey, N.; Sankur, O.; Czumaj, A. (ed.); Mehlhorn, K. (ed.); Pitts, AM (ed.); Wattenhofer, R. (ed.), Robust reachability in timed automata: a game-based approach, No. 7392, 128-140 (2012), Berlin · Zbl 1367.68161
[29] Bouyer, P.; Markey, N.; Sankur, O.; Abdulla, PA (ed.); Potapov, I. (ed.), Robustness in timed automata, No. 8169, 1-18 (2013), Berlin · Zbl 1407.68282
[30] Bozzelli L, La Torre S (2009) Decision problems for lower/upper bound parametric timed automata. Form Methods Syst Des 35(2):121-151 · Zbl 1186.68245 · doi:10.1007/s10703-009-0074-0
[31] Chaki, S.; Clarke, EM; Ouaknine, J.; Sharygina, N.; Sinha, N., State/event-based software model checking, No. 2999, 128-147 (2004), Berlin · Zbl 1196.68129
[32] Chevallier R, Encrenaz-Tiphène E, Fribourg L, Xu W (2009) Timed verification of the generic architecture of a memory circuit using parametric timed automata. Form Methods Syst Des 34(1):59-81 · Zbl 1165.68401 · doi:10.1007/s10703-008-0061-x
[33] Clarisó R, Cortadella J (2007) The octahedron abstract domain. Sci Comput Program 64(1):115-139 · Zbl 1171.68540 · doi:10.1016/j.scico.2006.03.009
[34] Clarke, EM; Grumberg, O.; Jha, S.; Lu, Y.; Veith, H., Counterexample-guided abstraction refinement, 154-169 (2000), Berlin · Zbl 0974.68517
[35] Collomb-Annichini A, Sighireanu M (2001) Parameterized reachability analysis of the IEEE 1394 root contention protocol using TReX. In: RT-TOOLS
[36] D’Argenio, PR; Katoen, JP; Ruys, TC; Tretmans, J., The bounded retransmission protocol must be on time!, No. 1217, 416-431 (1997), Berlin
[37] Davies J (1993) Specification and proof in real-time CSP. Cambridge University Press, Cambridge · Zbl 0820.68075 · doi:10.1017/CBO9780511569760
[38] Dong JS, Hao P, Qin S, Sun J, Yi W (2008) Timed automata patterns. IEEE Trans Softw Eng 34(6):844-859 · doi:10.1109/TSE.2008.52
[39] Encrenaz, E.; Fribourg, L., Time separation of events: an inverse method, No. 209, 135-148 (2008), Palaiseau · Zbl 1279.68256
[40] Fidge CJ, Hayes IJ, Watson G (1999) The deadline command. IEE Proc Softw 146(2):104-111 · doi:10.1049/ip-sen:19990407
[41] Fribourg, L.; Lesens, D.; Moro, P.; Soulat, R., Robustness analysis for scheduling problems using the inverse method, 73-80 (2012), Washington, DC
[42] Henzinger, TA; Wong-Toi, H., Using HyTech to synthesize control parameters for a steam boiler, No. 1165, 265-282 (1995), Berlin · doi:10.1007/BFb0027241
[43] Henzinger TA, Nicollin X, Sifakis J, Yovine S (1994) Symbolic model checking for real-time systems. Inf Comput 111(2):193-244 · Zbl 0806.68080 · doi:10.1006/inco.1994.1045
[44] Henzinger TA, Ho PH, Wong-Toi H (1997) HyTech: a model checker for hybrid systems. Softw Tools Technol Transf 1:460-463 · Zbl 1060.68603
[45] Hoare C (1985) Communicating sequential processes. Prentice-Hall, International series in computer science · Zbl 0637.68007
[46] Hoenicke, J.; Olderog, ER, Combining specification techniques for processes, data and time, No. 2335, 245-266 (2002), Berlin · Zbl 1057.68626
[47] Hune T, Romijn J, Stoelinga M, Vaandrager FW (2002) Linear parametric model checking of timed automata. J Log Algebr Program 52-53:183-220 · Zbl 1008.68069 · doi:10.1016/S1567-8326(02)00037-1
[48] Jaubert, R.; Reynier, PA; Hofmann, M. (ed.), Quantitative robustness analysis of flat timed automata, No. 6604, 229-244 (2011), Berlin · Zbl 1326.68185
[49] Jovanovic, A.; Lime, D.; Roux, OH; Piterman, N. (ed.); Smolka, SA (ed.), Integer parameter synthesis for timed automata, No. 7795, 401-415 (2013), Berlin · Zbl 1381.68121
[50] Khatib, L.; Muscettola, N.; Havelund, K., Mapping temporal planning constraints into timed automata, 21-27 (2001), Washington, DC
[51] Knapik M, Penczek W (2012) Bounded model checking for parametric timed automata. Trans Petri Nets Other Models Concurr 5:141-159 · Zbl 1350.68183 · doi:10.1007/978-3-642-29072-5_6
[52] Kwak, HH; Lee, I.; Philippou, A.; Choi, JY; Sokolsky, O., Symbolic schedulability analysis of real-time systems, 409-418 (1998), Washington, DC
[53] Kwak HH, Lee I, Sokolsky O (1999) Parametric approach to the specification and analysis of real-time system designs based on ACSR-VP. Electron Notes Theor Comput Sci 25:38-49 · doi:10.1016/S1571-0661(04)00130-6
[54] Larsen KG, Pettersson P, Yi W (1997) UPPAAL in a nutshell. Int J Softw Tools Technol Transf 1(1-2):134-152 · Zbl 1060.68577 · doi:10.1007/s100090050010
[55] Lime, D.; Roux, OH; Seidner, C.; Traonouez, LM; Kowalewski, S. (ed.); Philippou, A. (ed.), Romeo: a parametric model-checker for Petri nets with stopwatches, No. 5505, 54-57 (2009), Berlin
[56] Mahony, BP; Dong, JS, Overview of the semantics of TCOZ, 66-85 (1999), Berlin · Zbl 0963.68118 · doi:10.1007/978-1-4471-0851-1_5
[57] Markey, N., Robustness in real-time systems, 28-34 (2011), Washington, DC
[58] Minsky ML (1967) Computation: finite and infinite machines. Prentice-Hall Inc, Upper Saddle River, NJ · Zbl 0195.02402
[59] Ouaknine, J.; Worrell, J., Revisiting digitization, robustness, and decidability for timed automata, 198-207 (2003), Washington, DC
[60] Ouaknine J, Worrell J (2003b) Timed CSP = closed timed \[\epsilon\] ϵ-automata. Nord J Comput 10(2):99-133 · Zbl 1096.68665
[61] Pnueli, A., The temporal logic of programs, 46-57 (1977), Washington, DC
[62] Qin, S.; Dong, JS; Chin, WN, A semantic foundation for TCOZ in unifying theories of programming, No. 2805, 321-340 (2003), Berlin
[63] Roscoe AW (2001) Compiling shared variable programs into CSP. In: PROGRESS workshop
[64] Sankur, O.; Sharygina, N. (ed.); Veith, H. (ed.), Shrinktech: a tool for the robustness analysis of timed automata, No. 8044, 1006-1012 (2013), Berlin
[65] Schneider S (2000) Concurrent and real-time systems. Wiley, Hoboken, NJ
[66] Schrijver A (1986) Theory of linear and integer programming. Wiley, Hoboken, NJ · Zbl 0665.90063
[67] Sun, J.; Liu, Y.; Dong, JS; Chen, C.; Chin, WN (ed.); Qin, S. (ed.), Integrating specification and programs for system modeling and verification, 127-135 (2009), Washington, DC
[68] Sun, J.; Liu, Y.; Dong, JS; Pang, J., PAT: towards flexible verification under fairness, No. 5643, 709-714 (2009), Berlin
[69] Sun J, Liu Y, Dong JS, Liu Y, Shi L, André É (2013) Modeling and verifying hierarchical real-time systems using stateful timed CSP. ACM Trans Softw Eng Methodol 22(1):3.1-3.29. doi:10.1145/2430536.2430537 · doi:10.1145/2430536.2430537
[70] Traonouez LM, Lime D, Roux OH (2009) Parametric model-checking of stopwatch Petri nets. J Univers Comput Sci 15(17):3273-3304 · Zbl 1217.68140
[71] Traonouez LM (2012) A parametric counterexample refinement approach for robust timed specifications. FIT, electronic proceedings in theoretical computer science 87:17-33 · doi:10.4204/EPTCS.87.3
[72] Yi, W.; Pettersson, P.; Daniels, M., Automatic verification of real-time communicating systems by constraint-solving, No. 6, 243-258 (1995), London
[73] Yoneda, T.; Kitai, T.; Myers, CJ, Automatic derivation of timing constraints by failure analysis, No. 2404, 195-208 (2002), Berlin · Zbl 1010.68711
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. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.