NASA Logo

NTRS

NTRS - NASA Technical Reports Server

Back to Results
Formal Methods Case Studies for DO-333RTCA DO-333, Formal Methods Supplement to DO-178C and DO-278A provides guidance for software developers wishing to use formal methods in the certification of airborne systems and air traffic management systems. The supplement identifies the modifications and additions to DO-178C and DO-278A objectives, activities, and software life cycle data that should be addressed when formal methods are used as part of the software development process. This report presents three case studies describing the use of different classes of formal methods to satisfy certification objectives for a common avionics example - a dual-channel Flight Guidance System. The three case studies illustrate the use of theorem proving, model checking, and abstract interpretation. The material presented is not intended to represent a complete certification effort. Rather, the purpose is to illustrate how formal methods can be used in a realistic avionics software development project, with a focus on the evidence produced that could be used to satisfy the verification objectives found in Section 6 of DO-178C.
Document ID
20140004055
Acquisition Source
Langley Research Center
Document Type
Contractor Report (CR)
Authors
Cofer, Darren
(Rockwell Collins, Inc. Cedar Rapids, IA, United States)
Miller, Steven P.
(Rockwell Collins, Inc. Cedar Rapids, IA, United States)
Date Acquired
April 29, 2014
Publication Date
April 1, 2014
Subject Category
Numerical Analysis
Report/Patent Number
NF1676L-18435
NASA/CR-2014-218244
Funding Number(s)
TASK: NNL12AB85T
WBS: WBS 534723.02.02.07.40
CONTRACT_GRANT: NNL06AA04B
Distribution Limits
Public
Copyright
Public Use Permitted.
No Preview Available