×

zbMATH — the first resource for mathematics

Parametric deadlock-freeness checking timed automata. (English) Zbl 06667723
Sampaio, Augusto (ed.) et al., Theoretical aspects of computing – ICTAC 2016. 13th international colloquium, Taipei, Taiwan, ROC, October 24–31, 2016. Proceedings. Cham: Springer (ISBN 978-3-319-46749-8/pbk; 978-3-319-46750-4/ebook). Lecture Notes in Computer Science 9965, 469-478 (2016).
Summary: Distributed real-time systems are notoriously difficult to design, and must be verified, e.g., using model checking. In particular, deadlocks must be avoided as they either yield a system subject to potential blocking, or denote an ill-formed model. Timed automata are a powerful formalism to model and verify distributed systems with timing constraints. In this work, we investigate synthesis of timing constants in timed automata for which the model is guaranteed to be deadlock-free.
For the entire collection see [Zbl 1347.68012].
MSC:
68Qxx Theory of computing
Software:
IMITATOR; PAT; PPL; Uppaal
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Alur, R., Dill, D.L.: A theory of timed automata. Theor. Comput. Sci. 126(2), 183–235 (1994) · Zbl 0803.68071 · doi:10.1016/0304-3975(94)90010-8
[2] Alur, R., Henzinger, T.A., Vardi, M.Y.: Parametric real-time reasoning. In: STOC, pp. 592–601 (1993) · Zbl 1310.68139 · doi:10.1145/167088.167242
[3] André, É., Fribourg, L., Kühne, U., Soulat, R.: IMITATOR 2.5: a tool for analyzing robustness in scheduling problems. In: Giannakopoulou, D., Méry, D. (eds.) FM 2012. LNCS, vol. 7436, pp. 33–36. Springer, Heidelberg (2012). doi: 10.1007/978-3-642-32759-9_6 · Zbl 06103215 · doi:10.1007/978-3-642-32759-9_6
[4] André, É., Lime, D.: Liveness in L/U-parametric timed automata (2016, submitted). https://hal.archives-ouvertes.fr/hal-01304232
[5] Bagnara, R., Hill, P.M., Zaffanella, E.: 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 (2008) · Zbl 05312355 · doi:10.1016/j.scico.2007.08.001
[6] Beneš, N., Bezděk, P., Larsen, K.G., Srba, J.: Language emptiness of continuous-time parametric timed automata. In: Halldórsson, M.M., Iwama, K., Kobayashi, N., Speckmann, B. (eds.) ICALP 2015. LNCS, vol. 9135, pp. 69–81. Springer, Heidelberg (2015). doi: 10.1007/978-3-662-47666-6_6 · Zbl 1440.68150 · doi:10.1007/978-3-662-47666-6_6
[7] Clarisó, R., Cortadella, J.: Verification of concurrent systems with parametric delays using octahedra. In: ACSD, pp. 122–131. IEEE Computer Society (2005) · Zbl 1138.68465 · doi:10.1109/ACSD.2005.34
[8] Hune, T., Romijn, J., Stoelinga, M., Vaandrager, F.W.: Linear parametric model checking of timed automata. JLAP 52–53, 183–220 (2002) · Zbl 1008.68069
[9] Jovanović, A., Lime, D., Roux, O.H.: Integer parameter synthesis for timed automata. IEEE Trans. Softw. Eng. 41(5), 445–461 (2015) · Zbl 1381.68121 · doi:10.1109/TSE.2014.2357445
[10] Larsen, K.G., Pettersson, P., Yi, W.: UPPAAL in a nutshell. Int. J. Softw. Tools Technol. Transf. 1(1–2), 134–152 (1997) · Zbl 1060.68577 · doi:10.1007/s100090050010
[11] Markey, N.: Robustness in real-time systems. In: SIES, pp. 28–34. IEEE Computer Society Press (2011) · doi:10.1109/SIES.2011.5953652
[12] Sun, J., Liu, Y., Dong, J.S., Pang, J.: PAT: towards flexible verification under fairness. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 709–714. Springer, Heidelberg (2009). doi: 10.1007/978-3-642-02658-4_59 · Zbl 05571940 · doi:10.1007/978-3-642-02658-4_59
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.