nach oben

Erschienen in:

2015 | OriginalPaper | Buchkapitel

Assuring the Guardians

verfasst von : Jonathan Laurent, Alwyn Goodloe, Lee Pike

Erschienen in: Runtime Verification

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

Ultra-critical systems are growing more complex, and future systems are likely to be autonomous and cannot be assured by traditional means. Runtime Verification (RV) can act as the last line of defense to protect the public safety, but only if the RV system itself is trusted. In this paper, we describe a model-checking framework for runtime monitors. This tool is integrated into the Copilot language and framework aimed at RV of ultra-critical hard real-time systems. In addition to describing its implementation, we illustrate its application on a number of examples ranging from very simple to the Boyer-Moore majority vote algorithm.

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 Verifying Hennessy-Milner Logic with Recursion at Runtime

Nächstes Kapitel A Case Study on Runtime Monitoring of an Autonomous Research Vehicle (ARV) System

https://github.com/Copilot-Language.

Maintaining structure is important for two reasons. First, the model checker can use this structural information to optimize its search; see structural abstraction in [8]. Second, structured transition systems are easier to read, debug, and transform.

Akbarpour, B., Paulson, L.C.: MetiTarski: an automatic theorem prover for real-valued special functions. J. Automat. Reasoning 44(3), 175–205 (2010)MathSciNetCrossRefMATH

Caspi, P., Pialiud, D., Halbwachs, N., Plaice, J.: LUSTRE: a declarative language for programming synchronous systems. In: 14th Symposium on Principles of Programming Languages, pp. 178–188 (1987)

de Moura, L., Rueß, H., Sorea, M.: Bounded model checking and induction: from refutation to verification. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 14–26. Springer, Heidelberg (2003)

Dutertre, B.: Yices 2.2. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 737–744. Springer, Heidelberg (2014)

Eén, N., Sörensson, N.: Temporal induction by incremental SAT solving. Electr. Notes Theor. Comput. Sci. 89(4), 543–560 (2003)CrossRefMATH

Torlak, E., Bodik, R.: A lightweight symbolic virtual machine for solver-aided host languages. In: Proceedings of the 35th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2014, pp. 530–541. ACM (2014)

Gill, A.: Domain-specific languages and code synthesis using Haskell. Commun. ACM 57(6), 42–49 (2014)CrossRef

Hagen, G.: Verifying safety properties of Lustre programs: an SMT-based approach. PhD thesis, University of Iowa (2008)

Hagen, G., Tinelli, C.: Scaling up the formal verification of lustre programs with SMT-based techniques. In: Proceedings of the 8th International Conference on Formal Methods in Computer-Aided Design (FMCAD 2008). IEEE (2008)

10.

Halbwachs, N., Lagnier, F., Raymond, P.: Synchronous observers and the verification of reactive systems. In: Nivat, M., Rattray, C., Rus, T., Scollo, G. (eds.) AMAST 1993. Workshops in Computing, pp. 83–96. Springer, London (1994)

11.

Havelund, K.: Runtime verification of C programs. In: Suzuki, K., Higashino, T., Ulrich, A., Hasegawa, T. (eds.) TestCom/FATES 2008. LNCS, vol. 5047, pp. 7–22. Springer, Heidelberg (2008) CrossRef

12.

Havelund, K., Roşu, G.: Efficient monitoring of safety properties. Int. J. Softw. Tools Technol. Transf. 6(2), 158–173 (2004)CrossRef

13.

Hesselink, W.H.: The Boyer-Moore majority vote algorithm (2005)

14.

Jones, S.P. (ed.): Haskell 98 Language and Libraries: The Revised Report. Cambridge University Press, Cambridge (2002). http://haskell.org/

15.

Mikáć, J., Caspi, P.: Formal system development with Lustre: Framework and example. Technical Report TR-2005-11, Verimag Technical Report (2005)

16.

Moore, S.J., Boyer, R.S.: MJRTY - A Fast Majority Vote Algorithm. Technical Report 1981–32, Institute for Computing Science, University of Texas, February 1981

17.

University of Iowa: Kind Research Group. Kind 2: Multi-engine SMT-based Automatic Model Checker. http://kind2-mc.github.io/kind2/

18.

Pike, L., Goodloe, A., Morisset, R., Niller, S.: Copilot: a hard real-time runtime monitor. 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. 345–359. Springer, Heidelberg (2010) CrossRef

19.

Pike, L., Hickey, P.C., Bielman, J., Elliott, T., DuBuisson, T., Launchbury, J.: Programming languages for high-assurance autonomous vehicles: extended abstract. In: Programming Languages Meets Program Verification, pp. 1–2. ACM (2014)

20.

Pike, L., Niller, S., Wegmann, N.: Runtime verification for ultra-critical systems. In: Khurshid, S., Sen, K. (eds.) RV 2011. LNCS, vol. 7186, pp. 310–324. Springer, Heidelberg (2012) CrossRef

21.

Pike, L., Wegmann, N., Niller, S., Goodloe, A.: Experience report: a do-it-yourself high-assurance compiler. In: Proceedings of the International Conference on Functional Programming (ICFP). ACM, September 2012

22.

Pike, L., Wegmann, N., Niller, S., Goodloe, A.: Copilot: monitoring embedded systems. Innovations Syst. Softw. Eng. 9(4), 235–255 (2013)CrossRef

23.

Uhler, R., Dave, N.: Smten with satisfiability-based search. In: Proceedings of the 2014 ACM International Conference on Object Oriented Programming Systems Languages and Applications, OOPSLA 2014, pp. 157–176. ACM (2014)

24.

Rushby, J.: Runtime certification. In: Leucker, M. (ed.) RV 2008. LNCS, vol. 5289, pp. 21–35. Springer, Heidelberg (2008) CrossRef

25.

Sheeran, M., Singh, S., Stålmarck, G.: Checking safety properties using induction and a SAT-solver. In: Johnson, S.D., Hunt Jr., W.A. (eds.) FMCAD 2000. LNCS, vol. 1954, pp. 108–125. Springer, Heidelberg (2000)

26.

Somenzi, F., Bradley, A.R.: Ic3: where monolithic and incremental meet. In: Proceedings of the International Conference on Formal Methods in Computer-Aided Design, FMCAD 2011, pp. 3–8. FMCAD Inc. (2011)

Titel: Assuring the Guardians
verfasst von: Jonathan Laurent
Alwyn Goodloe
Lee Pike
Verlag: Springer International Publishing
Buch: Runtime Verification
Print ISBN: 978-3-319-23819-7

Electronic ISBN: 978-3-319-23820-3

Copyright-Jahr: 2015
DOI: https://doi.org/10.1007/978-3-319-23820-3_6

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"