Name
Abstract | ||
|---|---|---|
Model checking of binary code is recognized as a promising tool for the verification of embedded software. Our approach, which is implemented in the [MC]SQUARE model checker, uses tailored simulators to build state spaces for model checking. Previously, these simulators have been generated by hand in a time-consuming and error-prone process. This paper proposes a method for synthesizing these simulators from a description of the hardware in an architecture description language in order to tackle these drawbacks. The application of this approach to the Atmel ATmega16 microcontroller is detailed in a case study. |
Year | DOI | Venue |
|---|---|---|
2010 | 10.1109/DDECS.2010.5491761 | Design and Diagnostics of Electronic Circuits and Systems |
Keywords | Field | DocType |
architecture description languages,assembly code,model checking,retargetability,synthesis | Programming language,Model checking,Embedded software,Computer science,Real-time computing,Assembly language,Software,Microcontroller,Application software,Architecture description language,Formal verification,Embedded system | Conference |
ISSN | ISBN | Citations |
2334-3133 | 978-1-4244-6612-2 | 1 |
PageRank | References | Authors |
0.38 | 5 | 4 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Dominique Gückel | 1 | 1 | 0.38 |
| Bastian Schlich | 2 | 214 | 17.98 |
| Jörg Brauer | 3 | 219 | 19.33 |
| Stefan Kowalewski | 4 | 602 | 65.14 |