Runtime verification of microcontroller binary code

Autor:	Andreas Steininger, Stefan Kowalewski, Martin Horauer, Jörg Brauer, Thomas Reinbacher
Rok vydání:	2014
Předmět:	High-level verification Functional verification Linear temporal logic Programming language Computer science Runtime verification Field-programmable gate array computer.software_genre Formal verification computer Software Invariant (computer science) Intelligent verification
Zdroj:	Science of Computer Programming. 80:109-129
ISSN:	0167-6423
DOI:	10.1016/j.scico.2012.10.015
Popis:	Runtime verification bridges the gap between formal verification and testing by providing techniques and tools that connect executions of a software to its specification without trying to prove the absence of errors. This article presents a framework for runtime verification of microcontroller binary code, which provides the above mentioned link in a non-intrusive fashion: the framework neither requires code instrumentation nor does it affect the execution of the analyzed program. This is achieved using a dedicated hardware unit that runs on a field programmable gate array in parallel to the analyzed microcontroller program. Different instances of this framework are discussed, with varying degrees of expressiveness of the supported specification languages and complexity in the hardware design. These instances range from invariant checkers for a restricted class of linear template constraints to a programmable processor that supports past-time linear temporal logic with timing constraints.
Databáze:	OpenAIRE
Externí odkaz:	https://explore.openaire.eu/search/publication?articleId=doi_________::a433e3a6e0554383b10384ea60960efc https://doi.org/10.1016/j.scico.2012.10.015 Zobrazit plný text záznamu Full Text from ScienceDirect