Abstract

Embedded systems are finding widespread application including communication systems, factory automation, graphics and imaging systems, medical equipment and even household appliances. With the increasing emergence of mixed hardware/software systems, it is important to ensure the correctness of such a system formally, particularly for real-time and safety critical applications. In this thesis, a hierarchical approach to modeling and formally verifying a complete embedded is proposed. The approach is demonstrated on the embedded software for a mouse controller application on a commercial microcontroller (PIC 16C71) from Microchip Technologies Inc. The embedded system is modeled at different levels of the design hierarchy i.e., the microcontroller RT level, the microcontroller Instruction Set Architecture (ISA), the embedded software assembly code level and the embedded software flowchart specification. The correctness of the system hardware platform in implementing its intended architecture is established by formally verifying the equivalence between the RTL hardware and the ISA, using the MDG sequential equivalence checking tool. The next step is taken to verify the particular application embedded in the system by checking the equivalence between the assembly code and its intended behavior, specified as a flowchart. Further verification is done on the models through the property checking procedure provided by the MDG tools. Liveness properties are also checked using the newly developed MDG model checking procedure. Inconsistencies in the assembly code with respect to the specification, as published in the application notes of the manufacturer, were uncovered through the verification experiments. Given the relatively small CPU time and memory consumption achieved in the experiments, the verification approach that is adopted was able to verify a whole embedded system in an automated environment