State-based model checking of event-driven system requirements

Author

Atlee, Joanne M. ; Gannon, John

Author_Institution

Dept. of Comput. Sci., Waterloo Univ., Ont., Canada

Volume

19

Issue

1

fYear

1993

fDate

1/1/1993 12:00:00 AM

Firstpage

24

Lastpage

40

Abstract

It is demonstrated how model checking can be used to verify safety properties for event-driven systems. SCR tabular requirements describe required system behavior in a format that is intuitive, easy to read, and scalable to large systems (e.g. the software requirements for the A-7 military aircraft). Model checking of temporal logics has been established as a sound technique for verifying properties of hardware systems. An automated technique for formalizing the semiformal SCR requirements and for transforming the resultant formal specification onto a finite structure that a model checker can analyze has been developed. This technique was effective in uncovering violations of system invariants in both an automobile cruise control system and a water-level monitoring system

Keywords

formal specification; formal verification; A-7 military aircraft; SCR tabular requirements; automobile cruise control system; event-driven system requirements; formal specification; model checking; software requirements; system invariants; temporal logics; water-level monitoring system; Automatic control; Automobiles; Control systems; Formal specifications; Hardware; Logic; Military aircraft; Safety; Software systems; Thyristors;

fLanguage

English

Journal_Title

Software Engineering, IEEE Transactions on

Publisher

ieee

ISSN

0098-5589

Type

jour

DOI

10.1109/32.210305

Filename

210305