Assuring the Guardians

• 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.

• BIBTEX:
  

  @InProceedings{pike-rv-15,
    author =    {Jonathan Laurent and Alwyn Goodloe and Lee Pike},
    title =     {Assuring the Guardians},
    booktitle = {Proceedings of the 5th Intl. Conference on Runtime Verification},
    publisher = {Springer},
    series  =   {LNCS},
    year =      {2015},
    month =     {September},
    note =      {Preprint available at \url{https://leepike.github.io/pub_pages/rv2015.html}},
  }
  

• PAPER DOWNLOAD: pike-rv2015.pdf

• Copilot Compiler and Language: http://leepike.github.com/Copilot/.