Maintaining abstractions with verification

Author

Hunt, Warren A., Jr. ; Young, William D.

Author_Institution

Comput. Logic Inc., Austin, TX, USA

fYear

1990

fDate

25-28 June 1990

Firstpage

117

Lastpage

125

Abstract

By use of the Boyer-Moore logic a microprocessor, an assembler and a compiler have been formally specified. Each of these provides a more abstract interface than that upon which they are implemented (e.g., the language of the compiler is more abstract than the language of the assembler that is the target of the compiler). In a simple prototype system, it is shown that it is possible to ensure that such abstractions are correctly maintained by verifying the correct implementation of the systems which support them. Because the components of the prototype system were designed as cooperating units, the abstractions supported can be composed to provide an environment for developing software systems for which the predictability of the high-level language programs is just as good as that of the Boolean logic hardware model.<>

Keywords

data structures; formal logic; formal specification; program verification; Boolean logic hardware model; Boyer-Moore logic; abstract interface; abstraction maintenance; assembler; compiler; cooperating units; high-level language programs; microprocessor; predictability; prototype system; software systems; verification; Assembly; Boolean functions; Hardware; High level languages; Logic design; Microprocessors; Predictive models; Prototypes; Software prototyping; Software systems;

fLanguage

English

Publisher

ieee

Conference_Titel

Computer Assurance, 1990. COMPASS '90, Systems Integrity, Software Safety and Process Security., Proceedings of the Fifth Annual Conference on

Conference_Location

Gaithersburg, MD, USA

Type

conf

DOI

10.1109/CMPASS.1990.175408

Filename

175408