Formal specification and verification of graphical user interfaces

Author

Fisher, Gene L. ; Frincke, Deborah A.

Author_Institution

Div. of Comput. Sci., California Univ., Davis, CA, USA

Volume

ii

fYear

1991

fDate

8-11 Jan 1991

Firstpage

114

Abstract

A technique for the fully formal specification and verification of graphical user interfaces is described. The technique is based on the algebraic specification of abstract datatypes. Both application program and user interface are defined in the same form, using equational axioms to specify formal semantics. The relationship between an application and its interface is defined using display axioms that specify the connection between abstract application operations and the corresponding operations of the interface. Using these display axioms, one can formally verify that an interface is correct with respect to the underlying application. In addition, the display axioms can be treated as a form of executable specification, used at runtime to maintain correspondence between the application program and its interface

Keywords

formal specification; graphical user interfaces; program verification; abstract datatypes; algebraic specification; application program; equational axioms; formal semantics; formal specification; graphical user interfaces; software verification; Application software; Computer displays; Computer science; Concrete; Equations; Formal specifications; Graphical user interfaces; Runtime; Specification languages; User interfaces;

fLanguage

English

Publisher

ieee

Conference_Titel

System Sciences, 1991. Proceedings of the Twenty-Fourth Annual Hawaii International Conference on

Conference_Location

Kauai, HI

Type

conf

DOI

10.1109/HICSS.1991.183970

Filename

183970