Modeling and formal verification of a commercial microcontroller for embedded system applications
S. Balakrishnan, Sofiène Tahar · 2002
Embedded systems are finding widespread application. A formal model for the underlying hardware (RT level) of the microcontroller (PIC 16C71) in commercial use, along with its Instruction Set Architecture (ISA) using Multiway Decision Graphs (MDG) is proposed. Using the MDG verification tools, we verified if the instructions in the instruction set are implemented correctly in the microcontroller hardware. Models for the flowchart specification and the assembly language implementation of an embedded software, used in a mouse controller application are portrayed. Applying the platform of the ISA verification, the correctness of the embedded software has been verified at a higher level of abstraction. Inconsistencies in the assembly code with respect to the specification, as published in the application notes of the manufacturer, were uncovered through our experiments.