40/2011 : Past time LTL runtime verification for microcontroller binary code

RR Number

40/2011

Conference

16th International Workshop on Formal Methods for Industrial Critical Systems (FMICS 2011), Volume 6959/2011 LNCS

Author(s)

Thomas Reinbacher, Jörg Brauer, Martin Horauer, Andreas Steininger, Stefan Kowalewski

Abstract

This paper presents a method for runtime verification of microcontroller binary code based on past time linear temporal logic (ptLTL). We show how to implement a framework that, owing to a dedicated hardware unit, does not require code instrumentation, thus, allowing the program under scrutiny to remain unchanged. Furthermore, we demonstrate techniques for synthesizing the hardware and software units required to monitor the validity of ptLTL specifications.

Bibtex

@incollection {springerlink:10.1007/978-3-642-24431-5_5,
   author = {Reinbacher, Thomas and Brauer, Jörg and Horauer, Martin and Steininger, Andreas and Kowalewski, Stefan},
   affiliation = {Embedded Computing Systems Group, Vienna University of Technology, Austria},
   title = {Past Time LTL Runtime Verification for Microcontroller Binary Code},
   booktitle = {Formal Methods for Industrial Critical Systems},
   series = {Lecture Notes in Computer Science},
   editor = {Salaün, Gwen and Schätz, Bernhard},
   publisher = {Springer Berlin / Heidelberg},
   isbn = {978-3-642-24430-8},
   keyword = {Computer Science},
   pages = {37-51},
   volume = {6959},
   url = {http://dx.doi.org/10.1007/978-3-642-24431-5_5},
   note = {10.1007/978-3-642-24431-5_5},
   year = {2011}
}

Download

Get tu_rwth_fhtw_fmics11.pdf - Adobe PDF-format, (420.92 KB; posted at January 02 2012)