Copilot: Monitoring Embedded Systems

• ABSTRACT:
  
  Runtime verification (RV) is a natural fit for ultra-critical systems, where correctness is imperative. In ultra-critical systems, even if the software is fault-free, because of the inherent unreliability of commodity hardware and the adversity of operational environments, processing units (and their hosted software) are replicated, and fault-tolerant algorithms are used to compare the outputs. We investigate both software monitoring in distributed fault-tolerant systems, as well as implementing fault-tolerance mechanisms using RV techniques. We describe the Copilot language and compiler, specifically designed for generating monitors for distributed, hard real-time systems. We also describe two case-studies in which we generated Copilot monitors in avionics systems.

• BIBTEX:
  

  @TechReport{pike-cr-12,
    author =       {Lee Pike},
    title =        {{C}opilot: Monitoring Embedded Systems},
    institution =  {NASA Langley Research Center},
    year =         {2012},
    number =    {NASA/CR-2012-217329},
    month =     {January},
    note =      {Available at \url{http://ntrs.nasa.gov/search.jsp?R=20120001989&hterms=pike+goodloe&qs=Ntx%3Dmode%2520matchallpartial%2520%26Ntk%3DAll%26N%3D0%26Ntt%3Dpike%2520goodloe}}
  }
      

• PAPER DOWNLOAD: copilot-cr.pdf