Accession Number : ADP006477

Title :   Formal Verification of a Redundancy Management Algorithm,

Corporate Author : GEC AVIONICS LTD ROCHESTER (UNITED KINGDOM)

Personal Author(s) : Draper, Jonathan

Report Date : SEP 1991

Pagination or Media Count : 6

Abstract : This paper describes work on mathematical formal verification of a redundancy management algorithm that was carried out in two stages. The first stage used the specification language Z and verified the specifications with hand written rigorous proofs. The second stage used a proof tool to produce formal proofs and specified the system with the language of that proof tool. The system specified was part of a safety critical software section of an avionic system. The paper includes a section that presents the theoretical concepts of formal methods, concentrating on specification and proof. These ideas are illustrated in the paper with extracts from the formal specifications. Some of the benefits and problems of using mathematical proof for verification are described in the illustration of the redundancy management example.

Descriptors :   *ALGORITHMS, *COMPUTER PROGRAM VERIFICATION, AVIONICS, BENEFITS, HANDS, LANGUAGE, MANAGEMENT, PAPER, REDUNDANCY, SAFETY, SPECIFICATIONS, TOOLS, VERIFICATION, WORK, VALIDATION.

Subject Categories : Computer Programming and Software

Distribution Statement : APPROVED FOR PUBLIC RELEASE