×

zbMATH — the first resource for mathematics

Robust specification of real time components. (English) Zbl 1348.68143
Fahrenberg, Uli (ed.) et al., Formal modeling and analysis of timed systems. 9th international conference, FORMATS 2011, Aalborg, Denmark, September 21–23, 2011. Proceedings. Berlin: Springer (ISBN 978-3-642-24309-7/pbk). Lecture Notes in Computer Science 6919, 129-144 (2011).
Summary: Specification theories for real-time systems allow to reason about interfaces and their implementation models, using a set of operators that includes satisfaction, refinement, logical and parallel composition. To make such theories applicable throughout the entire design process from an abstract specification to an implementation, we need to be able to reason about possibility to effectively implement the theoretical specifications on physical systems. In the literature, this implementation problem has already been linked to the robustness problem for Timed Automata, where small perturbations in the timings of the models are introduced. We address the problem of robust implementations in timed specification theories. Our contributions include the analysis of robust timed games and the study of robustness with respect to the operators of the theory.
For the entire collection see [Zbl 1223.68006].

MSC:
68Q60 Specification and verification (program logics, model checking, etc.)
68Q45 Formal languages and automata
Software:
ECDAR
PDF BibTeX Cite
Full Text: DOI
References:
[1] de Alfaro, L., Henzinger, T.A.: Interface automata. In: ESEC / SIGSOFT FSE, pp. 109–120 (2001)
[2] de Alfaro, L., Henzinger, T.A.: Interface-based design. In: Engineering Theories of Software Intensive Systems, Marktoberdorf Summer School (2004)
[3] Alur, R., Dill, D.L.: A theory of timed automata. Theor. Comput. Sci. 126(2), 183–235 (1994) · Zbl 0803.68071
[4] Badouel, E., Benveniste, A., Caillaud, B., Henzinger, T., Legay, A., Passerone, R.: Contract theories for embedded systems: A white paper. Research report, IRISA/INRIA Rennes (2009)
[5] Bouyer, P., Markey, N., Reynier, P.A.: Robust model-checking of linear-time properties in timed automata. In: Correa, J.R., Hevia, A., Kiwi, M. (eds.) LATIN 2006. LNCS, vol. 3887, pp. 238–249. Springer, Heidelberg (2006) · Zbl 1145.68464
[6] Bouyer, P., Markey, N., Reynier, P.A.: Robust analysis of timed automata via channel machines. In: Amadio, R.M. (ed.) FOSSACS 2008. LNCS, vol. 4962, pp. 157–171. Springer, Heidelberg (2008) · Zbl 1138.68431
[7] Bulychev, P., Chatain, T., David, A., Larsen, K.G.: Efficient on-the-fly algorithm for checking alternating timed simulation. In: Ouaknine, J., Vaandrager, F.W. (eds.) FORMATS 2009. LNCS, vol. 5813, pp. 73–87. Springer, Heidelberg (2009) · Zbl 1262.68105
[8] Cassez, F., David, A., Fleury, E., Larsen, K.G., Lime, D.: Efficient on-the-fly algorithms for the analysis of timed games. In: Abadi, M., de Alfaro, L. (eds.) CONCUR 2005. LNCS, vol. 3653, pp. 66–80. Springer, Heidelberg (2005) · Zbl 1134.68382
[9] Chatterjee, K., Henzinger, T.A., Prabhu, V.S.: Timed parity games: Complexity and robustness. In: Cassez, F., Jard, C. (eds.) FORMATS 2008. LNCS, vol. 5215, pp. 124–140. Springer, Heidelberg (2008) · Zbl 1171.68527
[10] David, A., Larsen, K.G., Legay, A., Nyman, U., Wąsowski, A.: Timed I/O automata: a complete specification theory for real-time systems. In: HSCC, pp. 91–100. ACM, New York (2010) · Zbl 1361.68143
[11] David, A., Larsen, K.G., Legay, A., Nyman, U., Wąsowski, A.: ECDAR: An environment for compositional design and analysis of real time systems. In: Bouajjani, A., Chin, W.-N. (eds.) ATVA 2010. LNCS, vol. 6252, pp. 365–370. Springer, Heidelberg (2010) · Zbl 05795644
[12] Jaubert, R., Reynier, P.A.: Quantitative robustness analysis of flat timed automata. In: Hofmann, M. (ed.) FOSSACS 2011. LNCS, vol. 6604, pp. 229–244. Springer, Heidelberg (2011) · Zbl 1326.68185
[13] Maler, O., Pnueli, A., Sifakis, J.: On the synthesis of discrete controllers for timed systems (an extended abstract). In: Finkel, A., Jantzen, M. (eds.) STACS 1992. LNCS, vol. 577, pp. 229–242. Springer, Heidelberg (1992) · Zbl 1379.68227
[14] Puri, A.: Dynamical properties of timed automata. In: Ravn, A.P., Rischel, H. (eds.) FTRTFT 1998. LNCS, vol. 1486, pp. 210–227. Springer, Heidelberg (1998)
[15] The COMBEST Consortium: Combest, http://www.combest.eu.com
[16] The SPEEDS Consortium: Speeds, http://www.speeds.eu.com
[17] Wulf, M., Doyen, L., Markey, N., Raskin, J.F.: Robust safety of timed automata. Formal Methods in System Design 33, 45–84 (2008) · Zbl 1165.68392
[18] Wulf, M.D., Doyen, L., Raskin, J.F.: Almost ASAP semantics: from timed models to timed implementations. Formal Aspects of Computing 17(3), 319–341 (2005) · Zbl 1101.68670
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.