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. We propose a hierarchical approach to modelling and formal verification of a complete embedded system at higher levels of abstraction, using Multiway Decision Graphs (MDGs). We demonstrate our approach on the embedded software for a mouse controller application on a commercial microcontroller (PIC 16C71), using the MDG verification tools. We model the system at different levels of the design heirarchy i.e., the microcontroller RT level, the microcontroller Instruction Set Architecture (ISA), the embedded software assembly code level and the embedded software flowchart specification. We conduct verifications using equivalence checking between the RTL harware and the ISA to establish the correctness of the system hardware platform in implementing its intended architecture. We then take the next step 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, we validate our models and verification by conducting property checking. Liveness properties are also checked using the recently 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 both equivalence and property checking. Given the relatively small CPU time and memory consumption achieved in our experiments, the verification approach we adopted was able to verify a whole embedded system automatically..

Download postscript file (PS File)

Send comments and suggestions to: tahar@ece.concordia.ca