Formal Methods Tool Qualification - NASA
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 athttp://www.sti.nasa.gov E-mail your question to help@sti.nasa.gov 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 stakeholders4
visually inspect the artifacts to establish that the requisite DO-178C objectives were met. Increasingsoftware complexity has led to the use of software tools to assist in satisfying these objectives.However, when using a tool to satisfy objectives, it must be established that the tool itself istrustworthy. This can be established by manually reviewing the tool’s output, which might be feasiblefor a test case generation tool. If the output of the tool is not independently verified, then the tool mustbe qualified. Qualification is the process by which a software tool is deemed trustworthy. Guidance forqualifying tools is provided in DO-330: Software Tool Qualification Considerations [5]. In a processsimilar to DO-178C, this document outlines a set of activities for establishing that a software tool can betrusted to carry out its mission in the software development process.As software complexity has grown, the avionics community has also turned to emergent technologies tomitigate the high cost of modern software development. In fact, the release of DO-178C also providedguidance on the use of these emergent technologies in DO-178C. This guidance comes in the form oftechnology supplements. These supplements interpret the guidance in DO-178C through the lens of theprospective technology. These supplements address model based development, object orientedtechnology, and formal methods. This project focuses on the use of formal methods tools. Guidance fortheir usage is provided in DO-333: Formal Methods Supplement to DO-178C and DO-278A [6].Prior NASA-sponsored work entitled Formal Methods Case Studies for DO-333 [7] described in detailhow one might use formal methods tools to satisfy DO-178C objectives. The focus of the current projectis to extend that work by thoroughly exploring the issues surrounding the qualification of formalmethods tools. It seeks to interpret the guidance of DO-333 and DO-330 and provide critical feedback tothe avionics community on how to qualify formal methods tools.2.1 Intended ReaderThis report is intended for1. software developers and prospective certification applicants who may wish to qualify formalmethods tools in a DO-178C software development process,2. formal methods tool developers who wish build robust formal methods tools to be used in theavionics industry, and3. practicing certification experts who will be expected to evaluate formal methods basedcertifications.It is hoped that the concepts and experiences documented in this report will provide insight into the DO330 and DO-333 guidance.It is recommended that the reader has a general familiarity with the DO-178C software developmentprocess, including the required artifacts to be developed. It is also recommended that the reader isfamiliar with at least one of the following classes of formal methods tools: model checking, theoremproving, or abstract interpretation.2.2 Overview of Project ActivitiesThe purpose of this project is to thoroughly investigate the qualification of formal methods tools. Thefirst activity focused on organizing an event to engage the certification and formal methodscommunities to discuss qualification of formal methods tools. This event, a Dagstuhl Seminar, focusedon providing a broad overview of the certification processes to the formal methods community. Further,5
participants provided experience reports on past formal methods qualifications within variousindustries, such as rail, nuclear, and automotive industries. Lastly, the entire group discussed nonstandard approaches to qualification, including the use of qualified tools to check the results ofunqualified tools.Next, the project addressed the general issue of trust in formal methods tools. The Tool Assurance Studyprovides a broad overview of potential trust issues in formal methods tools. It identifies issues withformal methods tools in general and then identifies issues in trust specific to each class of formalmethods tool. This document will be useful to prospective users of formal methods tools to helpunderstand the roles of the tool developer and tool user in obtaining trustworthy results from a formalmethods tool.The remainder of work on the project focuses on the interpretation of the DO-330 qualificationguidance as it applies to formal methods tools. First, the Mitigation Strategies activity performed areview of the tool qualification objectives anticipated for formal methods tools. This is covered in detailin Section 3.3.1, but broadly stated, it is anticipated that formal methods tools are much more likely tobe used for verification rather than software development. As such, the requirements for theirqualification are lower than they would be for tools used to produce airborne software. The MitigationStrategies task performs an overview of each qualification objective and highlights concerns regardingunique challenges to meeting that objective for a formal methods tool. Additionally, for someobjectives, the authors provid
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.
2016 nasa 0 29 nasa-std-8739.4 rev a cha workmanship standard for crimping, interconnecting cables, harnesses, and wiring 2016 nasa 0 30 nasa-hdbk-4008 w/chg 1 programmable logic devices (pld) handbook 2016 nasa 0 31 nasa-std-6016 rev a standard materials and processes requirements for spacecraft 2016 nasa 0 32
e Adobe Illustrator CHEAT SHEET. Direct Selection Tool (A) Lasso Tool (Q) Type Tool (T) Rectangle Tool (M) Pencil Tool (N) Eraser Tool (Shi E) Scale Tool (S) Free Transform Tool (E) Perspective Grid Tool (Shi P) Gradient Tool (G) Blend Tool (W) Column Graph Tool (J) Slice Tool (Shi K) Zoom Tool (Z) Stroke Color
6 Track 'n Trade High Finance Chapter 4: Charting Tools 65 Introduction 67 Crosshair Tool 67 Line Tool 69 Multi-Line Tool 7 Arc Tool 7 Day Offset Tool 77 Tool 80 Head & Shoulders Tool 8 Dart/Blip Tool 86 Wedge and Triangle Tool 90 Trend Fan Tool 9 Trend Channel Tool 96 Horizontal Channel Tool 98 N% Tool 00
5.D Qualification of water supplies 5.D.1 Introduction 5.D.2 Risk analysis 5.D.3 Design qualification 5.D.4 Installation qualification 5.D.5 Operational qualification (OQ) 5.D.6 Transfer to the user 5.D.7 Process validation/performance qualification (PQ) 5.D.8 Qualification report 5.E Operation of water supplies
An equipment qualification is handled in different phases of the equipment lifecycle, start-ing with design qualification, installation qualification, and then operational qualification and performance qualification. Every step in the equipment qualification formally comprises a plan, the execution and a report.
exempting qualification. B Structure of the qualification The structure of the qualification and syllabus subjects is shown on the following diagram. C Progression through the qualification Subjects within each learning pillar of the qualification are designed to be sequential, from operational to strategic level, encouraging
Jan 10, 2012 · The NASA STI program provides access to the NASA Aeronautics and Space Database and its public interface, the NASA Technical Report Server, thus providing one of the largest collections of aeronautical and space science STI in the world. Results are published in both non-NASA channels and by NASA in the NASA
Solutions: AMC Prep for ACHS: Counting and Probability ACHS Math Competition Team 5 Jan 2009. Problem 1 What is the probability that a randomly drawn positive factor of 60 is less than 7? Problem 1 What is the probability that a randomly drawn positive factor of 60 is less than 7? The factors of 60 are 1,2,3,4,5,6,10,12,15,20,30, and 60. Six of the twelve factors are less than 7, so the .
