Abstract
Networks of timed automata are a widely used formalism to model timed systems. Models are often concise and convenient since timed automata abstract from many details of actual implementations. One such abstraction is that the semantics of networks of timed automata introduces an implicit global scheduler which blocks edges which are sending on a channel until a matching receiving edge is enabled. When models are used a priori, that is, to develop, e.g., a communication protocol which is supposed to have a (non-shared memory) distributed implementation, a corresponding global scheduler is not desired.
To facilitate distributed implementations of timed automata models, we introduce a new class of networks of timed automata whose behaviour does not depend on the blocking of sending edges. We show that the membership problem for this new class of networks of timed automata is decidable and evaluate our new decision procedure.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Notes
- 1.
We need at least the values 0, 1, 2 (and the standard interpretation of increment and decrement) in our transformation presented in Sect. 4.
- 2.
The Uppaal tool considers only one sequence of receiving edges induced by the so-called system declaration.
- 3.
We consider committed locations (although any model with committed locations does depend on a global scheduler) since we will use committed locations in our source-to-source transformation based decision procedure in Sect. 4.
- 4.
We write \(\mathcal {N}_{ loc } ' \models \mathsf {E}\lozenge \,{} ( enabled \ge 1 \wedge deadlock ){}\) if and only if \(\mathcal {T}(\mathcal {N}_{ loc } )\) has a reachable configuration \(c\) with \(c\models ( enabled \ge 1 \wedge deadlock )\); \(c\models deadlock \) if and only if, for all configurations \(c', c''\) and \(t \in \mathrm {I\!R}_{0}^{+}\), \(c\xrightarrow {t}_{} c' \xrightarrow {\lambda }_{} c''\) implies \(\lambda \in \mathrm {I\!R}_{0}^{+}\).
References
Abdellatif, T., Combaz, J., Sifakis, J.: Model-based implementation of real-time applications. In: EMSOFT, pp. 229–238. ACM (2010)
Alur, R., Dill, D.: A theory of timed automata. TCS 126(2), 183–235 (1994)
Amnell, T., Fersman, E., Pettersson, P., Sun, H., Wang, Y.: Code synthesis for timed automata. Nordic J. Comput. (NJC) 9, 1–32 (2002). http://www2.imm.dtu.dk/pubdb/p.php?1957
Behrmann, G., David, A., Larsen, K.G.: A tutorial on Uppaal. In: Bernardo, M., Corradini, F. (eds.) SFM-RT 2004. LNCS, vol. 3185, pp. 200–236. Springer, Heidelberg (2004). doi:10.1007/978-3-540-30080-9_7
Fehnker, A., Glabbeek, R., Höfner, P., McIver, A., Portmann, M., Tan, W.L.: Automated analysis of AODV using UPPAAL. In: Flanagan, C., König, B. (eds.) TACAS 2012. LNCS, vol. 7214, pp. 173–187. Springer, Heidelberg (2012). doi:10.1007/978-3-642-28756-5_13
Feo-Arenis, S., Westphal, B., Dietsch, D., Muñiz, M., Andisha, A.S., Podelski, A.: Ready for testing: ensuring conformance to industrial standards t formal verification. Formal Asp. Comput. 28(3), 499–527 (2016)
Hendriks, M.: Translating Uppaal to not quite C (2001). http://repository.ubn.ru.nl/bitstream/handle/2066/19058/19058.pdf?sequence=1
Kristensen, J., Mejlholm, A., Pedersen, S.: Automatic translation from Uppaal to C (2005). http://mejlholm.org/uni/pdfs/dat4.pdf
Muñiz, M., Westphal, B., Podelski, A.: Timed automata with disjoint activity. In: Jurdziński, M., Ničković, D. (eds.) FORMATS 2012. LNCS, vol. 7595, pp. 188–203. Springer, Heidelberg (2012). doi:10.1007/978-3-642-33365-1_14
Muñiz, M.: Model checking for time division multiple access systems. Ph.D. thesis, Albert-Ludwigs-Universität Freiburg, December 2014
Muñiz, M., Westphal, B., Podelski, A.: Detecting Quasi-equal clocks in timed automata. In: Braberman, V., Fribourg, L. (eds.) FORMATS 2013. LNCS, vol. 8053, pp. 198–212. Springer, Heidelberg (2013). doi:10.1007/978-3-642-40229-6_14
Olderog, E.R., Dierks, H.: Real-Time Systems - Formal Specification and Automatic Verification. Cambridge University Press, Cambridge (2008)
Senthooran, I., Watanabe, T.: On generating soft real-time programs for non-real-time environments. In: Nishizaki, S., Numao, M., Caro, J., Suarez, M.T. (eds.) Theory and Practice of Computation, pp. 1–12. Springer, Tokyo (2013)
Wibling, O., Parrow, J., Pears, A.: Ad hoc routing protocol verification through broadcast abstraction. In: Wang, F. (ed.) FORTE 2005. LNCS, vol. 3731, pp. 128–142. Springer, Heidelberg (2005). doi:10.1007/11562436_11
Wulf, M.D., Doyen, L., Raskin, J.F.: Almost ASAP semantics: from timed models to timed implementations. Formal Asp. Comput. 17, 319–341 (2005)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2017 Springer International Publishing AG
About this paper
Cite this paper
Feo-Arenis, S., Vujinović, M., Westphal, B. (2017). On Global Scheduling Independency in Networks of Timed Automata. In: Abate, A., Geeraerts, G. (eds) Formal Modeling and Analysis of Timed Systems. FORMATS 2017. Lecture Notes in Computer Science(), vol 10419. Springer, Cham. https://doi.org/10.1007/978-3-319-65765-3_3
Download citation
DOI: https://doi.org/10.1007/978-3-319-65765-3_3
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-65764-6
Online ISBN: 978-3-319-65765-3
eBook Packages: Computer ScienceComputer Science (R0)