Other functions - task order - statement of work (SOW) title: technology infusion study for do-333, the formal methods supplement to do-178C and do-278A 1.0 background: NASA's aviation safety…

Other functions - task order - statement of work (SOW) title: technology infusion study for do-333, the formal methods supplement to do-178C and do-278A 1.0 background: NASA's aviation safety program is conducting research directed at improving the safety of current and future aircraft operating in the national airspace system. The research focus includes the system-wide safety assurance technologies (ssat) project. Under ssat, there is a technical challenge area known as assurance of flight critical systems (afcs). A primary thrust of afcs research is advancing formal methods technology so IT can serve the needs of the avionics community. In january 2012, rtca released several documents, products of rtca special committee SC-205, that are key to the future of certification of avionics software. Foremost among these are do-178C, software considerations in airborne systems and equipment certification, and do-278A, software integrity assurance considerations for communication, navigation, surveillance, and air traffic management (CNA/ATM) systems. As the long-awaited successors to do-178B and do-278, these documents provide updated guidance for developers of airborne and ground-based software. SC-205 also created four supplements to accompany do-178C and do-278A. One of these, formal methods supplement to do-178C and do-278A, has been published as do-333. For the first time, avionics developers will have extensive guidance on applying formal methods technology to produce evidence that certification authorities can accept for certification credit. This will provide a pathway for the gradual introduction of formal methods into the development life cycle and the eventual certification of aircraft and engines whose software airworthiness is assured (in part) by formal methods. While the release of do-333 is an important event, there remain significant challenges to the successful infusion of formal methods into development and certification workflows. At a minimum, the level of formal methods expertise within the aviation workforce needs to be raised. Moreover, there exists a need for case studies to explore more fully the application of formal methods in realistic settings and demonstrate how the results can be mapped to the objectives of do-333. Although do-333 represents a carefully reasoned approach, the wide variety of formal methods tools and techniques poses the challenge of fitting them within a unified framework. The goal of this study task is to produce more detailed guidance and worked examples to help bridge the GAP between the promise of do-333 and the current level of preparedness within industry and government. Bridging this GAP is vital for the successful infusion of formal methods into civil aviation. 2.0 scope and objectives: the scope of this task order is to conduct a study that will summarize the state of the art in formal methods applicable to the aviation domain. The study will include one or more case studies on the use of do-333 and formal methods in realistic applications to avionics software. The objective of this task is to deliver a set of documents that together will constitute a guidebook on formal methods suitable for those undertaking software development using techniques having do-333 relevance. The resulting guidebook should be regarded as a compendium of technical advice and informed recommendations. IT should not be construed as having any official connection to do-333 because IT will not be subjected to the rtca consensus process. Because the documents produced under this task are intended for open, public distribution, the contractor shall ensure that they are free of proprietary, sensitive, or restricted information of all kinds. IT is expected that some software tools to be described will require the purchase of a license from a tool vendor. If there are additional intellectual property issues involved, such as the use of patented algorithms or