Using correctness results to verify behavioral properties of microprocessors

Author

Windley, Phillip J.

Author_Institution

Dept. of Comput. Sci., Idaho Univ., Moscow, ID, USA

fYear

1991

fDate

24-27 Jun 1991

Firstpage

99

Lastpage

106

Abstract

An alternative method is given for verifying behavioral properties of computer systems using a correctness result. It is shown that the correctness result can be useful in establishing these properties by proving two important properties for a microprocessor called AVM-1. The author briefly describes the general techniques used in verifying a microprocessor. An informal description of architecture and organization of AVM-1 is presented next. He discusses parts of the formal specification and verification of AVM-1. It is shown how they can be used to prove two properties regarding the integrity of the supervisory mode in AVM-1

Keywords

computer architecture; formal specification; microprocessor chips; program verification; AVM-1; behavioral properties; computer systems; correctness result; correctness results; formal specification; informal description; integrity; microprocessor; supervisory mode; verification; Aerospace control; Application software; Computer applications; Computer architecture; Computer science; Control systems; Frequency; Hardware; Memory management; Microprocessors;

fLanguage

English

Publisher

ieee

Conference_Titel

Computer Assurance, 1991. COMPASS '91, Systems Integrity, Software Safety and Process Security. Proceedings of the Sixth Annual Conference on

Conference_Location

Gaithersburg, MD

Print_ISBN

0-7803-0126-9

Type

conf

DOI

10.1109/CMPASS.1991.161049

Filename

161049