Members

• Subhashini Balakrishnan
• A. Abbas Mir
• Dr. Sofiène Tahar

Description

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 project, a hierarchical approach to modeling and formal verification of a complete embedded system at higher levels of abstraction, using Multiway Decision Graphs (MDGs), 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 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 both equivalence and property checking. 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 automatically. Recently we also experimented with using this hierarchical approach to apply model checking using CADENCE SMV. The comparison with the MDG verification show the advantage of the data abstraction provided by the MDG tools. Furthermore, MDG supports equivalence checking while SMV does not which is an asset to the hierarchical methodology.

Publications

1. A. A. Mir, S. Balakrishnan, and S. Tahar: Modeling and Verification of an Embedded System using Cadence SMV; Proc. IEEE Canadian Conference on Electrical & Computer Engineering (CCECE'00), Halifax, Nova Scotia, Canada, May 2000.
2. Balakrishnan and S. Tahar: Une approche hiérarchique à la vérification formelle des systèmes embarqué en utilisant MDGs; 68th ACFAS Symposium (ACFAS'00), Montreal, Canada, May 2000.
3. S. Balakrishnan and S. Tahar: A Hierarchical Approach to the Formal Verification of Embedded Systems Using MDGs; Proc. IEEE 9th Great Lakes Symposium on VLSI (GLS-VLSI'99), Ann Arbor, Michigan, USA, March 1999, IEEE Computer Society Press, pp. 284-287.
4. S. Balakrishnan and S. Tahar: Modeling and Formal Verification of a Commercial Microcontroller for Embedded System Applications; Proc. IEEE 10th International Conference on Microelectronics (ICM'98), Monastir, Tunisia, December 1998, pp. 107-110.
5. A. A. Mir, S. Balakrishnan, and S. Tahar: Modeling and Verification of an Embedded System using Cadence SMV ; Technical Report, Concordia University, Department of Electrical and Computer Engineering, September 1999. [12 pages]
S. Balakrishnan and S. Tahar: On the Formal Verification of Embedded Software Using Multiway Decision Graphs;. Technical Report No. 402, Concordia University, Department of Electrical and Computer Engineering, December 1997. [14 pages]
6. Subhashini Balakrishnan: Modeling and Verification of Embedded Systems using MDGs; MaSc Thesis, Concordia University, Department of Electrical and Computer Engineering, November 1999.