Breadcrumb

 
 

A hierarchical approach to the formal verification of embedded systems using MDGs

Title:

A hierarchical approach to the formal verification of embedded systems using MDGs

Balakrishnan, Subhashini (1999) A hierarchical approach to the formal verification of embedded systems using MDGs. Masters thesis, Concordia University.

[img]
Preview
PDF
2369Kb

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

Divisions:Concordia University > Faculty of Engineering and Computer Science > Electrical and Computer Engineering
Item Type:Thesis (Masters)
Authors:Balakrishnan, Subhashini
Pagination:x, 73 leaves : ill. ; 29 cm.
Institution:Concordia University
Degree Name:Theses (M.A.Sc.)
Program:Electrical and Computer Engineering
Date:1999
Thesis Supervisor(s):Tahar, Sofiene
ID Code:1090
Deposited By:Concordia University Libraries
Deposited On:27 Aug 2009 13:16
Last Modified:08 Dec 2010 10:18
Related URLs:
All items in Spectrum are protected by copyright, with all rights reserved. The use of items is governed by Spectrum's terms of access.

Repository Staff Only: item control page

Document Downloads

More statistics for this item...

Concordia University - Footer