Machine Code Verification Using The Bogor Framework

Verification and validation of embedded systems software is tedious and time consuming. Software model checking uses a tool-based approach automating this process. In order to more accurately model software it is necessary to provide hardware support that enables the execution of software as it should run on native hardware. Hardware support often requires the creation of model checking tools specific to the instruction set architecture. The creation of software model checking tools is non-trivial. We present a strategy for using an "off-the-shelf" model checking tool, Bogor, to provide support for multiple instruction set architectures. Our strategy supports key hardware features such as instruction execution, exceptional control flow, and interrupt servicing as extensions to Bogor. These extensions work within the tool framework using existing interfaces and require significantly less code than creating an entire model checking tool.

Name thesis:degree_name

MS

Grantor dc:publisher

Brigham Young University - Provo

Author dc:creator

• Edelman, Joseph R.

• Bogor
• model checking
• language extension
• embedded systems verification
• Computer Sciences

Language dc:language

English

Repository record dc:identifier

https://scholarsarchive.byu.edu/etd/1386

OAI identifier oai:identifier

oai:scholarsarchive.byu.edu:etd-2385