Formal requirements analysis of an avionics control system

Author

Dutertre, Bruno ; Stavridou, Victoria

Author_Institution

Dept. of Comput. Sci., Queen Mary & Westfield Coll., London, UK

Volume

23

Issue

5

fYear

1997

fDate

5/1/1997 12:00:00 AM

Firstpage

267

Lastpage

278

Abstract

The authors report on a formal requirements analysis experiment involving an avionics control system. They describe a method for specifying and verifying real-time systems with PVS. The experiment involves the formalization of the functional and safety requirements of the avionics system as well as its multilevel verification. First level verification demonstrates the consistency of the specifications whilst the second level shows that certain system safety properties are satisfied by the specification. They critically analyze methodological issues of large scale verification and propose some practical ways of structuring verification activities for optimizing the benefits

Keywords

aircraft control; formal specification; formal verification; military aircraft; military avionics; military computing; real-time systems; safety-critical software; PVS; avionics control system; fighter aircraft; formal requirements analysis; formalized functional requirements; formalized safety requirements; large scale verification; multilevel verification; real-time system specification; real-time system verification; system safety properties; verification activity structuring; Aerospace control; Aerospace electronics; Aircraft; Collaborative work; Control systems; Formal verification; Large-scale systems; Optimization methods; Real time systems; Software safety;

fLanguage

English

Journal_Title

Software Engineering, IEEE Transactions on

Publisher

ieee

ISSN

0098-5589

Type

jour

DOI

10.1109/32.588520

Filename

588520