Title

Formal specification and verification of microprocessor interrupts

Date of Award

1993

Degree Type

Dissertation

Degree Name

Doctor of Philosophy (PhD)

Department

Electrical Engineering and Computer Science

Advisor(s)

Chin, Shiu-Kai

Keywords

information security

Subject Categories

Databases and Information Systems

Abstract

Information security is important in academia, industry and government. The use of formal methods in the design and development of computer hardware and software systems greatly increases the confidence in the security of the information on these systems. Interrupt features are included in most microprocessors and are essential for input/output capabilities. This work uses formal methods to develop and verify correctness properties for well behaved microprocessor interrupts. Several microprocessor architectures are studied to identify common interrupt properties. The well behaved interrupt is then defined and further developed using an abstract state machine and the verification proofs were conducted with the Clio verification system. The abstract concept of program execution where no interrupts occur is compared to program execution in the presence of interrupts and proven to produce the same results. The formal definition and verification of microprocessor interrupts in this work provides a guideline for the formal specification and verification of any computer system with interrupt capabilities and the correctness properties will contribute to the complete formal verification of computer systems.

Access

Surface provides description only. Full text is available to ProQuest subscribers. Ask your Librarian for assistance.

http://libezproxy.syr.edu/login?url=http://proquest.umi.com/pqdweb?did=744939011&sid=1&Fmt=2&clientId=3739&RQT=309&VName=PQD

Link to Full Text

Share

COinS