Skip to main content
Fachgebiete
Automobil + Motoren Bauwesen + Immobilien Business IT + Informatik Elektrotechnik + Elektronik Energie + Nachhaltigkeit Finance + Banking Management + Führung Marketing + Vertrieb Maschinenbau + Werkstoffe Versicherung + Risiko
DE
EN
Bücher
Zeitschriften
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
SLX-Digitalkonferenz: Zukunftswerkstatt 2024

Mehr Umsatz mit Top-Kontakten

Am 7. Mai erfahren Sie, wie Vertriebsteams Leadgenerierung, Leadnurturing und Leadstrategien effizient steuern können.
Erweiterte Suche
Anmelden
nach oben
Erschienen in:
Buchtitelbild

2016 | OriginalPaper | Buchkapitel

Some Thoughts on Runtime Verification

verfasst von : Oded Maler

Erschienen in: Runtime Verification

Verlag: Springer International Publishing

Einloggen

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

search-config
loading …

Abstract

Some reflections on verification and runtime verification in general and of cyber-physical systems in particular.

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
Nächstes Kapitel First International Summer School on Runtime Verification
Fußnoten
1
Speaking about control, “reachability” (and to some extent “controllability”) used not long ago to denote some very precise technical term in the Kalmanistic theory of linear systems before some barbarians came and kidnapped its meaning. As a punishment we have sometime to hear colleagues from others disciplines abuse theoretical computer science sacred terms such as decidability or models of computation.
 
2
The term formal language provides yet another opportunity for terminological confusion. In theoretical computer science a formal language is nothing but a set of sequences, something very semantic in our context.
 
3
I am indebted to a discussion with Yaron Wolfsthal before starting this project, in which he explained to me the workings of the FOCS property checker developed at IBM for discrete/digital systems.
 
4
The advantage of dense time as used in MTL or in timed automata is in not committing to a fixed time step such as the clock tick in digital circuits. Otherwise, the major advantage of timed logics and automata is not in density but in the ability to reason about time arithmetically rather than by counting ticks. More opinions on timed systems can be found in [21].
 
5
No program, no matter how thoroughly verified, will produce the correct result if you hit the computer with a hammer or just unplug it from power.
 
6
This fact renders our early heroic CS efforts to prove decidability results on hybrid systems somewhat misguided, at least from an applicative point of view. In one of the early hybrid systems meetings I organized in Grenoble in the 90s, Paul Caspi presented a cartoon of a dialog between a control engineer, saying: it is trivial and a theoretical computer scientist responding: it is undecidable!. But the noble activity of doing math for its own sake is common in all academic engineering domains, control included.
 
7
Kurt Vonnegut’s quote Tiger got to hunt, bird got to fly; Man got to sit and wonder ‘why, why, why?’ can be rephrased as Governors govern and airplanes fly; It takes a computer scientist to wonder why.
 
8
Are all the things that we want to monitor restricted to prefixes of behaviors that lead to a violation of the specifications? I do not have an answer at this moment and it probably depends also on whether we are in the hard (safety critical) or soft (quality of service) domain. It is also related to whether numerical quantities are involved: the car fuel indicator shows continuously the value of a real-valued variable and, in addition, emits a warning when it crosses a threshold.
 
Literatur
1.
Annapureddy, Y., Liu, C., Fainekos, G.E., Sankaranarayanan, S., S-TaLiRo: a tool for temporal logic falsification for hybrid systems. In: TACAS, pp. 254–257 (2011)
2.
3.
Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skeletons using branching time temporal logic. In: Kozen, D. (ed.) Logic of Programs 1981. LNCS, vol. 131, pp. 52–71. Springer, Heidelberg (1982). doi:10.​1007/​BFb0025774 CrossRef
4.
d’Angelo, B., Sankaranarayanan, S., Sanchez, C., Robinson, W., Finkbeiner, B., Sipma, H.B., Mehrotra, S., Manna, Z., Lola: Runtime monitoring of synchronous systems. In: TIME, pp. 166–174 (2005)
5.
Deshmukh, J., Jin, X., Kapinski, J., Maler, O.: Stochastic local search for falsification of hybrid systems. In: Finkbeiner, B., Pu, G., Zhang, L. (eds.) ATVA 2015. LNCS, vol. 9364, pp. 500–517. Springer, Heidelberg (2015). doi:10.​1007/​978-3-319-24953-7_​35 CrossRef
6.
7.
Donzé, A., Maler, O.: Robust satisfaction of temporal logic over real-valued signals. In: Chatterjee, K., Henzinger, T.A. (eds.) FORMATS 2010. LNCS, vol. 6246, pp. 92–106. Springer, Heidelberg (2010). doi:10.​1007/​978-3-642-15297-9_​9 CrossRef
8.
Donzé, A.: Breach, a toolbox for verification and parameter synthesis of hybrid systems. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 167–170. Springer, Heidelberg (2010). doi:10.​1007/​978-3-642-14295-6_​17 CrossRef
9.
Eisner, C., Fisman, D., Havlicek, J., Lustig, Y., McIsaac, A., Campenhout, D.: Reasoning with temporal logic on truncated paths. In: Hunt, W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 27–39. Springer, Heidelberg (2003). doi:10.​1007/​978-3-540-45069-6_​3 CrossRef
10.
Fainekos, G.E., Pappas, G.J.: Robustness of temporal logic specifications for continuous-time signals. Theoret. Comput. Sci. 410(42), 4262–4291 (2009)MathSciNetCrossRefMATH
11.
Falcone, Y.: You should better enforce than verify. In: Barringer, H., Falcone, Y., Finkbeiner, B., Havelund, K., Lee, I., Pace, G., Roşu, G., Sokolsky, O., Tillmann, N. (eds.) RV 2010. LNCS, vol. 6418, pp. 89–105. Springer, Heidelberg (2010). doi:10.​1007/​978-3-642-16612-9_​9 CrossRef
12.
Ferrère, T., Maler, O., Ničković, D., Ulus, D.: Measuring with timed patterns. In: Kroening, D., Păsăreanu, C.S. (eds.) CAV 2015. LNCS, vol. 9207, pp. 322–337. Springer, Heidelberg (2015). doi:10.​1007/​978-3-319-21668-3_​19 CrossRef
13.
Halpern, J.Y., Vardi, M.Y.: Model checking vs. theorem proving: a manifesto. Artif. Intell. Math. Theory Comput. 212, 151–176 (1991)MathSciNetCrossRefMATH
14.
Harel, D., Pnueli, A.: On the development of reactive systems. In: Apt, K.R. (ed.) Logics and Models of Concurrent Systems, pp. 477–498. Springer, Heidelberg (1985)CrossRef
15.
Jin, X., Donzé, A., Deshmukh, J.V., Seshia, S.A.: Mining requirements from closed-loop control models. In: HSCC (2013)
16.
Kesten, Y., Pnueli, A.: A compositional approach to CTL\(^*\) verification. Theoretical Computer Science 331(2–3), 397–428 (2005)MathSciNetCrossRefMATH
17.
Koymans, R.: Specifying real-time properties with metric temporal logic. Real-Time Syst. 2(4), 255–299 (1990)CrossRef
18.
Maler, O.: Hybrid systems and real-world computations (1992)
19.
20.
Maler, O.: Amir Pnueli and the dawn of hybrid systems. In: HSCC, pp. 293–295. ACM (2010)
21.
Maler, O.: The unmet challenge of timed systems. In: From Programs to Systems (2014)
22.
Maler, O., Nickovic, D.: Monitoring temporal properties of continuous signals. In: Lakhnech, Y., Yovine, S. (eds.) FORMATS/FTRTFT -2004. LNCS, vol. 3253, pp. 152–166. Springer, Heidelberg (2004). doi:10.​1007/​978-3-540-30206-3_​12 CrossRef
23.
Maler, O., Nickovic, D., Pnueli, A.: From MITL to timed automata. In: Asarin, E., Bouyer, P. (eds.) FORMATS 2006. LNCS, vol. 4202, pp. 274–289. Springer, Heidelberg (2006). doi:10.​1007/​11867340_​20 CrossRef
24.
Maler, O., Nickovic, D., Pnueli, A.: On synthesizing controllers from bounded-response properties. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 95–107. Springer, Heidelberg (2007). doi:10.​1007/​978-3-540-73368-3_​12 CrossRef
25.
Maler, O., Nickovic, D., Pnueli, A.: Checking temporal properties of discrete, timed and continuous behaviors. In: Avron, A., Dershowitz, N., Rabinovich, A. (eds.) Pillars of Computer Science. LNCS, pp. 475–505. Springer, Heidelberg (2008)CrossRef
26.
27.
Nickovic, D.: Checking timed, hybrid properties: theory and applications. Ph.D. thesis, Université Joseph Fourier, Grenoble, France (2008)
28.
29.
Queille, J.P., Sifakis, J.: Specification and verification of concurrent systems in CESAR. In: Dezani-Ciancaglini, M., Montanari, U. (eds.) Programming 1982. LNCS, vol. 137, pp. 337–351. Springer, Heidelberg (1982). doi:10.​1007/​3-540-11494-7_​22 CrossRef
30.
Rizk, A., Batt, G., Fages, F., Soliman, S.: A general computational method for robustness analysis with applications to synthetic gene networks. Bioinformatics 25(12), 169–78 (2009)CrossRef
31.
Sankaranarayanan, S., Fainekos, G.E.: Falsification of temporal properties of hybrid systems using the cross-entropy method. In: HSCC (2012)
32.
Shea, R., Wilson, R.A.: The Illuminatus! Trilogy. Dell Publishing, New York (1984)
33.
Sifakis, J.: Rigorous system design. Found. Trends Electron. Des. Autom. 6(4), 293–362 (2012)CrossRef
34.
Sifakis, J.: System design automation: challenges and limitations. Proc. IEEE 103(11), 2093–2103 (2015)CrossRef
35.
Ulus, D., Ferrère, T., Asarin, E., Maler, O.: Timed pattern matching. In: Legay, A., Bozga, M. (eds.) FORMATS 2014. LNCS, vol. 8711, pp. 222–236. Springer, Heidelberg (2014). doi:10.​1007/​978-3-319-10512-3_​16
36.
Ulus, D., Ferrère, T., Asarin, E., Maler, O.: Online timed pattern matching using derivatives. In: Chechik, M., Raskin, J.-F. (eds.) TACAS 2016. LNCS, vol. 9636, pp. 736–751. Springer, Heidelberg (2016). doi:10.​1007/​978-3-662-49674-9_​47 CrossRef
37.
Varaiya, P.: A question about hierarchical systems. In: Djaferis, T.E., Schick, I.C. (eds.) System Theory, pp. 313–324. Springer, Heidelberg (2000)
38.
Moshe, Y.: Vardi and Pierre Wolper. an automata-theoretic approach to automatic program verification. In: LICS (1986)
39.
Wilson, R.A.: Quantum Psychology: How Brain Software Programs You & Your World. New Falcon Publication, New York (1990)
Metadaten
Titel
Some Thoughts on Runtime Verification
verfasst von
Oded Maler
Copyright-Jahr
2016
Buch
Runtime Verification

Print ISBN: 978-3-319-46981-2

Electronic ISBN: 978-3-319-46982-9

Copyright-Jahr: 2016

DOI
https://doi.org/10.1007/978-3-319-46982-9_1