nach oben

Erschienen in:

2017 | OriginalPaper | Buchkapitel

On Global Scheduling Independency in Networks of Timed Automata

verfasst von : Sergio Feo-Arenis, Milan Vujinović, Bernd Westphal

Erschienen in: Formal Modeling and Analysis of Timed Systems

Verlag: Springer International Publishing

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config

KI-gestützte Suche

Aus

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.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Vorheriges Kapitel On the Determinization of Timed Systems

Nächstes Kapitel Optimal Reachability in Cost Time Petri Nets

We need at least the values 0, 1, 2 (and the standard interpretation of increment and decrement) in our transformation presented in Sect. 4.

The Uppaal tool considers only one sequence of receiving edges induced by the so-called system declaration.

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.

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}^{+}\).

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)MathSciNetCrossRefMATH

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 CrossRef

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 CrossRef

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)MathSciNetCrossRef

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 CrossRef

10.

Muñiz, M.: Model checking for time division multiple access systems. Ph.D. thesis, Albert-Ludwigs-Universität Freiburg, December 2014

11.

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 CrossRef

12.

Olderog, E.R., Dierks, H.: Real-Time Systems - Formal Specification and Automatic Verification. Cambridge University Press, Cambridge (2008)CrossRefMATH

13.

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)

14.

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 CrossRef

15.

Wulf, M.D., Doyen, L., Raskin, J.F.: Almost ASAP semantics: from timed models to timed implementations. Formal Asp. Comput. 17, 319–341 (2005)CrossRefMATH

Titel: On Global Scheduling Independency in Networks of Timed Automata
verfasst von: Sergio Feo-Arenis
Milan Vujinović
Bernd Westphal
Verlag: Springer International Publishing
Buch: Formal Modeling and Analysis of Timed Systems
Print ISBN: 978-3-319-65764-6

Electronic ISBN: 978-3-319-65765-3

Copyright-Jahr: 2017
DOI: https://doi.org/10.1007/978-3-319-65765-3_3

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"