Skip to main content
SpringerLink
Log in
Book cover

Runtime Verification pp 87–101Cite as

Assuring the Guardians

  • Conference paper
  • First Online:

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 9333))

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.

This is a preview of subscription content, log in via an institution.

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

Notes

  1. 1.

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

  2. 2.

    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.

References

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

    Article  MathSciNet  MATH  Google Scholar 

  2. 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)

    Google Scholar 

  3. 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)

    Google Scholar 

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

    Google Scholar 

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

    Article  MATH  Google Scholar 

  6. 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)

    Google Scholar 

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

    Article  Google Scholar 

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

    Google Scholar 

  9. 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)

    Google Scholar 

  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)

    Google Scholar 

  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)

    Chapter  Google Scholar 

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

    Article  Google Scholar 

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

    Google Scholar 

  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)

    Google Scholar 

  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

    Google Scholar 

  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)

    Chapter  Google Scholar 

  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)

    Google Scholar 

  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)

    Chapter  Google Scholar 

  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

    Google Scholar 

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

    Article  Google Scholar 

  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)

    Google Scholar 

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

    Chapter  Google Scholar 

  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)

    Google Scholar 

  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)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. École Normale Supérieure, Paris, France

    Jonathan Laurent

  2. NASA Langley Research Center, Hampton, VA, USA

    Alwyn Goodloe

  3. Galois, Inc., Portland, OR, USA

    Lee Pike

Authors
  1. Jonathan Laurent
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Alwyn Goodloe
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Lee Pike
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Alwyn Goodloe .

Editor information

Editors and Affiliations

  1. TU Wien, Vienna, Austria

    Ezio Bartocci

  2. Max Planck Institute for Software Systems, Kaiserslautern, Germany

    Rupak Majumdar

Rights and permissions

Reprints and permissions

Copyright information

© 2015 Springer International Publishing Switzerland

About this paper

Cite this paper

Laurent, J., Goodloe, A., Pike, L. (2015). Assuring the Guardians. In: Bartocci, E., Majumdar, R. (eds) Runtime Verification. Lecture Notes in Computer Science(), vol 9333. Springer, Cham. https://doi.org/10.1007/978-3-319-23820-3_6

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-23820-3_6

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-23819-7

  • Online ISBN: 978-3-319-23820-3

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation