A formal verification technique for embedded software

Author

Thiry, Olivier ; Claesen, Luc

Author_Institution

IMEC, Katholieke Univ., Leuven, Belgium

fYear

1996

fDate

7-9 Oct 1996

Firstpage

352

Lastpage

357

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;

fLanguage

English

Publisher

ieee

Conference_Titel

Computer Design: VLSI in Computers and Processors, 1996. ICCD '96. Proceedings., 1996 IEEE International Conference on

Conference_Location

Austin, TX

ISSN

1063-6404

Print_ISBN

0-8186-7554-3

Type

conf

DOI

10.1109/ICCD.1996.563578

Filename

563578