Title :
A formal verification technique for embedded software
Author :
Thiry, Olivier ; Claesen, Luc
Author_Institution :
IMEC, Katholieke Univ., Leuven, Belgium
Abstract :
A method for the verification of embedded software correctness is presented. A formal model for an actual commercial microprocessor is established. This is done by modeling the instruction set and processor architecture. Embedded software takes the form of the assembly program code to be run on the processor. Specifications are given as CTL temporal logic formulae. The method has been implemented in the SMV model checker and is illustrated by a practical embedded system application: a mouse controller. The inconsistency of the specification and the implementation as an assembly language program as it has been published in the applications book of the manufacturer has been uncovered
Keywords :
assembly language; computer architecture; microprocessor chips; microprogramming; program verification; real-time systems; temporal logic; CTL temporal logic formulae; assembly language program; assembly program code; embedded software; embedded software correctness; embedded system application; formal model; formal verification; instruction set; processor architecture; Application software; Assembly; Books; Computer architecture; Embedded software; Embedded system; Formal verification; Logic; Mice; Microprocessors;
Conference_Titel :
Computer Design: VLSI in Computers and Processors, 1996. ICCD '96. Proceedings., 1996 IEEE International Conference on
Conference_Location :
Austin, TX
Print_ISBN :
0-8186-7554-3
DOI :
10.1109/ICCD.1996.563578
