Abstract
| Original language | English |
|---|---|
| Title of host publication | Eighth IEEE International Working Conference on Source Code Analysis and Manipulation (SCAM 2008) |
| Publisher | IEEE Computer Society |
| Pages | 15-24 |
| Number of pages | 10 |
| ISBN (Print) | 978-0-7695-3353-7 |
| DOIs | |
| Publication status | Published - 2008 |
| Externally published | Yes |
| Event | Eighth IEEE International Working Conference on Source Code Analysis and Manipulation - Beijing Friendship Hotel, Beijing, China Duration: 28 Sep 2008 → 29 Sep 2008 Conference number: 8 http://www.ieee-scam.org/2008/ |
Conference
| Conference | Eighth IEEE International Working Conference on Source Code Analysis and Manipulation |
|---|---|
| Abbreviated title | SCAM 2008 |
| Country | China |
| City | Beijing |
| Period | 28/09/08 → 29/09/08 |
| Internet address |
Fingerprint
Cite this
}
Some Assembly Required - Program Analysis of Embedded System Code. / Fehnker, Ansgar; Huuck, Ralf; Rauch, Felix; Seefried, Sean.
Eighth IEEE International Working Conference on Source Code Analysis and Manipulation (SCAM 2008). IEEE Computer Society, 2008. p. 15-24.Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review
TY - GEN
T1 - Some Assembly Required - Program Analysis of Embedded System Code
AU - Fehnker, Ansgar
AU - Huuck, Ralf
AU - Rauch, Felix
AU - Seefried, Sean
PY - 2008
Y1 - 2008
N2 - Programming embedded system software typically involves more than one programming language. Normally, a high-level language such as C/C++ is used for application oriented tasks and a low-level assembly language for direct interaction with the underlying hardware. In most cases those languages are closely interwoven and the assembly is embedded in the C/C++ code. Verification of such programs requires the integrated analysis of both languages at the same time. However, common algorithmic verification tools fail to address this issue. In this work we present a model-checking based static analysis approach which seamlessly integrates the analysis of embedded ARM assembly with C/C++ code analysis. In particular, we show how to automatically check that the ARM code complies to its interface descriptions. Given interface compliance, we then provide an extended analysis framework for checking general properties of ARM code. We implemented this analysis in our source code analysis tool Goanna, and applied to the source code of an L4 micro kernel implementation.
AB - Programming embedded system software typically involves more than one programming language. Normally, a high-level language such as C/C++ is used for application oriented tasks and a low-level assembly language for direct interaction with the underlying hardware. In most cases those languages are closely interwoven and the assembly is embedded in the C/C++ code. Verification of such programs requires the integrated analysis of both languages at the same time. However, common algorithmic verification tools fail to address this issue. In this work we present a model-checking based static analysis approach which seamlessly integrates the analysis of embedded ARM assembly with C/C++ code analysis. In particular, we show how to automatically check that the ARM code complies to its interface descriptions. Given interface compliance, we then provide an extended analysis framework for checking general properties of ARM code. We implemented this analysis in our source code analysis tool Goanna, and applied to the source code of an L4 micro kernel implementation.
U2 - 10.1109/SCAM.2008.15
DO - 10.1109/SCAM.2008.15
M3 - Conference contribution
SN - 978-0-7695-3353-7
SP - 15
EP - 24
BT - Eighth IEEE International Working Conference on Source Code Analysis and Manipulation (SCAM 2008)
PB - IEEE Computer Society
ER -