Title :
Using correctness results to verify behavioral properties of microprocessors
Author :
Windley, Phillip J.
Author_Institution :
Dept. of Comput. Sci., Idaho Univ., Moscow, ID, USA
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;
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
DOI :
10.1109/CMPASS.1991.161049
