Formal Design and Safety Analysis of AIR6110 Wheel Brake System

SAE Aerospace Information Report 6110, “Contiguous Aircraft/System Development Process Example,” follows the development of a complex wheel brake system (WBS) using processes in the industry standards Arp4754A, “Guidelines for Development of Civil Aircraft and Systems,” and Arp4761, “Guidelines and Methods for Conducting the Safety Assessment Process on Civil Airborne Systems and Equipment.” Air6110 employs informal methods to examine several WBS architectures which meet the same requirements with different degrees of reliability. In this case study, we analyze the Air6110 with formal methods. First, WBS architectures in Air6110 formerly using informal steps are recreated in a formal manner. Second, methods to automatically analyze and compare the behaviors of various architectures with additional, complementary information not included in the Air6110 are presented. Third, we provide an assessment of distinct formal methods ranging from contract-based design, to model checking, to model based safety analysis