Formal Methods Tool Qualification - NASA PDF

1m ago
544.11 KB
45 Pages

NASA/CR–2017-219371Formal Methods Tool QualificationLucas G. Wagner, Darren Cofer, and Konrad SlindRockwell Collins, Inc., Cedar Rapids, IowaCesare Tinelli and Alain MebsoutUniversity of Iowa, Iowa City, IowaFebruary 2017

NASA STI Program . . . in ProfileSince its founding, NASA has been dedicated to theadvancement of aeronautics and space science. TheNASA scientific and technical information (STI)program plays a key part in helping NASA maintainthis important role.The NASA STI program operates under the auspicesof the Agency Chief Information Officer. It collects,organizes, provides for archiving, and disseminatesNASA’s STI. The NASA STI program provides accessto the NTRS Registered and its public interface, theNASA Technical Reports Server, thus providing oneof the largest collections of aeronautical and spacescience STI in the world. Results are published in bothnon-NASA channels and by NASA in the NASA STIReport Series, which includes the following reporttypes: TECHNICAL PUBLICATION. Reports ofcompleted research or a major significant phase ofresearch that present the results of NASAPrograms and include extensive data or theoreticalanalysis. Includes compilations of significant scientific and technical dataand information deemed to be of continuingreference value. NASA counter-part of peerreviewed formal professional papers but has lessstringent limitations on manuscript length andextent of graphic presentations.TECHNICAL MEMORANDUM.Scientific and technical findings that arepreliminary or of specialized interest,e.g., quick release reports, workingpapers, and bibliographies that contain minimalannotation. Does not contain extensive analysis.CONTRACTOR REPORT. Scientific andtechnical findings by NASA-sponsoredcontractors and grantees. CONFERENCE PUBLICATION.Collected papers from scientific and technicalconferences, symposia, seminars, or othermeetings sponsored or co-sponsored by NASA. SPECIAL PUBLICATION. Scientific,technical, or historical information from NASAprograms, projects, and missions, oftenconcerned with subjects having substantialpublic interest. TECHNICAL TRANSLATION.English-language translations of foreignscientific and technical material pertinent toNASA’s mission.Specialized services also include organizingand publishing research results, distributingspecialized research announcements and feeds,providing information desk and personal searchsupport, and enabling data exchange services.For more information about the NASA STI program,see the following: Access the NASA STI program home page at E-mail your question to [email protected] Phone the NASA STI Information Desk at757-864-9658 Write to:NASA STI Information DeskMail Stop 148NASA Langley Research CenterHampton, VA 23681-2199

NASA/CR–2017-219371Formal Methods Tool QualificationLucas G. Wagner, Darren Cofer, and Konrad SlindRockwell Collins, Inc., Cedar Rapids, IowaCesare Tinelli and Alain MebsoutUniversity of Iowa, Iowa City, IowaNational Aeronautics andSpace AdministrationLangley Research CenterHampton, Virginia 23681-2199February 2017Prepared for Langley Research Centerunder Contract NNL14AA06C

The use of trademarks or names of manufacturers in this report is for accurate reporting and does notconstitute an official endorsement, either expressed or implied, of such products or manufacturers by theNational Aeronautics and Space Administration.Available from:NASA STI Program / Mail Stop 148NASA Langley Research CenterHampton, VA 23681-2199Fax: 757-864-6500

Table of Contents1Executive Summary . 32Introduction . 434567892.1Intended Reader . 52.2Overview of Project Activities . 5Background . 73.1Aircraft Certification. 73.2DO-178C and Related Documents . 73.3The Role of Tools and Qualification . 103.3.1Determining the Tool Qualification Level . 103.3.2DO-330 and Tool Qualification Objectives . 12Dagstuhl Seminar on Qualification of Formal Methods Tools . 144.1Scope and Purpose. 144.2Seminar Activities. 144.3Conclusions . 15Tool Assurance Study . 165.1Scope and Purpose. 165.2Key Findings . 165.3Conclusions . 18Mitigation Strategies . 196.1Scope and Purpose. 196.2Key Findings . 196.3Conclusions . 20Tool Qualification Plans and Estimates . 217.1Scope and Purpose. 217.2Key Findings . 227.3Conclusions . 22Qualification Package of Kind 2 . 248.1Scope and Purpose. 248.2Key Findings . 258.3Conclusions . 26Development of a Proof-Emitting Version of Kind 2. 271

9.1Background . 279.1.1Verified Tools . 279.1.2Verifying Tools. 289.1.3Previous Work on CVC4 . 289.1.4Production of the PC . 289.1.5Production of the FEC . 299.2Scope and Purpose. 299.3Key Findings . 299.4Conclusions . 3010Qualification of Check-It . 3110.1Scope and Purpose. 3110.2Key Findings . 3210.3Conclusions . 3411Conclusions . 3511.1Key Project Outcomes . 3511.2Future Work . 3612References . 382

1 Executive SummaryFormal methods tools have been shown to be effective at finding defects in safety-critical digital systemsincluding avionics systems. The publication of DO-178C and the accompanying formal methodssupplement DO-333 allows applicants to obtain certification credit for the use of formal methodswithout justification as an alternative method.However, there are still many issues that must be addressed before formal verification tools can beinjected into the design process for digital avionics systems. For example, DO-333 identifies threecategories of formal methods tools: theorem provers, model checkers, and abstract interpretation tools.Most developers of avionics systems are unfamiliar with even the basic notions of formal verification,much less which tools are most appropriate for different problem domains. Different levels of expertiseand skills will have to be mastered to use these tools effectively. DO-333 also requires applicants toprovide evidence of soundness for any formal method to be used; i.e., that it will never provideunwarranted confidence. Constructing a soundness argument is not something most practicingengineers understand. Finally, DO-178C requires that a tool used to meet DO-178C objectives bequalified in accordance with the tool qualification document DO-330. While formal verification toolsonly need to meet the objectives for the lower qualification levels (TQL-4 or TQL-5), it is notunreasonable to expect their qualification to pose unique challenges.In this project we have accomplished the following tasks related to qualification of formal methodstools:1. Investigate the assurances that are necessary and appropriate to justify the application offormal methods tools throughout all phases of design in real safety-critical settings.2. Produce practical examples of how to qualify formal verification tools in each of the threecategories identified in DO-333.3. Explore alternative approaches to the qualification of formal methods tools.We have conducted an extensive study of existing formal methods tools, identifying obstacles to theirqualification and proposing mitigations for those obstacles. We have produced a qualification plan foran open source formal verification tool, the Kind 2 model checker. We have investigated the feasibilityof independently verifying tool outputs through the generation of proof certificates which are thenverified by an independent certificate checking tool that verifies them. Finally, we have investigated thefeasibility of qualifying this proof certificate checker in lieu of qualifying the model checker itself.3

2 IntroductionCivilian aircraft must undergo a rigorous certification process to establish their airworthiness.Airworthiness is a measure of an aircraft’s suitability to operate safely in its intended environment, theNational Airspace System (NAS). Certification encompasses the entire aircraft and all of its components.This includes the engines, the airframe, the landing and taxi systems, and flight deck display systems, toname a few. Guidelines for developing certifiable aircraft are provided in APR4754A: Guidelines forDevelopment of Civil Aircraft and Systems [1]. Similarly, guidance for addressing aspects of safety incivilian aircraft are provided in ARP4761: Guidelines and Methods for Conducting the Safety AssessmentProcess on Civil Airborne Systems and Equipment [2]. Together these documents provide guidance fordeveloping safe and trustworthy civilian aircraft that can fly in the NAS. However, they only address theaircraft and its components at the system level. They do not provide guidance on the hardware andsoftware aspects of an avionics system. Instead, prospective applicants are instructed to consideradditional documents detailing the aspects of software and hardware separately. For hardware, theappropriate document is Design Assurance Guidance for Airborne Electronic Hardware [3], also known asDO-254. For software, the document is Software Considerations in Airborne Systems and EquipmentCertification [4], also known as DO-178C. The document tree for civilian avionics certifications is shownin Figure 1.Figure 1 - Civilian Avionics Certification OverviewDO-178C defines a rigorous software development process that requires the applicant to developrequirements, design and architecture, source code, object code, and test cases and procedures. Theseartifacts must satisfy a set of objectives related to their accuracy, traceability, and verification. Many ofthese objectives have been evaluated through a process of manual review; software stakehold

Formal methods tools have been shown to be effective at finding defects in safety-critical digital systems including avionics systems. The publication of DO-178C and the accompanying formal methods supplement DO-333 allows applicants to obtain certification credit for the use of formal methods without justification as an alternative method.