WIXLIB

Formal Methods(Status of RTCA/SC-205, Subgroup 6)Kelly HayhurstNASA Langley Research Centerkelly.j.hayhurst@nasa.gov[This is a draft version of the presentation, with basic information on thestatus of the Formal Methods Subgroup of RTCA SC-205/WG-71. Thefinal version, presented at the conference, will contain additionalinformation that you can get by sending Kelly an email request.]

Purpose of this talk Continue familiarization with formal methods– about formal methods, in general– specifically, how they will be discussed in the proposed FormalMethods Supplement to DO-178C Provide current information on activities and statusof SC-205 Subgroup 6 Formal Methods

Why bother with formal methods? Some avionics developers want to use formalmethods in their development processes -- forcertification credit Practically no guidance exists for how to do this– for the developer or for the certifier RTCA/SC-205, Sub-group 6 is working to proposesupplementary guidance on formal methods For that supplement to receive appropriate review, abetter understanding of formal methods is needed

Proposed SG6 mentDO-178CDO-178CDO-278ADO-278AGuidance forusing formalmethods to meet178C and 278Aobjectives The Formal Methods Supplement will not be a "how to" guide for formal methodsSG6 is working on a Discussion Paper that will provideexamples and more "how to" information4

Unofficial goalEnable the routine use of mature formal methodstoday for certification credit and allow for the use ofother formal methods as they mature To do that, we are working to– "De-mystify" formal methods provide sufficient information to allow the benefits and limitations offormal methods to be understood– Provide guidance for using formal methods withconventional methods so that the use of formal methods can be "normal"– Provide sufficient information to allow mature methods to bedistinguished from untrustworthy methods

Defining "formal methods" Mathematically based techniques for thespecification, development and verification ofsoftware and hardware systems – [Ref. Wiki]– that are based on formal logic, discrete mathematics, andcomputer-readable languages Formal methods allow properties of a computersystem to be predicted from a mathematical modelof the system by a process akin to calculation – [Ref.Rushby1]

Two Important Parts Formal Methods usually involves two types of activities:modeling and analysis– where the models and analysis procedures have an underlyingmathematically precise foundation Although modeling and analysis are common activitiesin software engineering, they have particular meaningswhen used in a Formal Methods context– not all models nor all analyses will meet requirements for beingformal "formal models" and "formal analysis" will be used todistinguish those activities when they meet requirementsfor formality

a Formal Model a Formal Analysis a Formal Method

Formal Models In general, a model is an abstract representation of agiven set of aspects of a system that is used foranalysis, simulation and/or code generation. To be formal, a model must have an unambiguous,mathematically defined syntax and semantics.– this makes it possible to use automated means to obtainguarantees that the model has certain specified properties Formal models can be produced by the developmentprocess (e.g.,. requirement or design activities) or byanalysis of the software or system artifact– when the artifact itself exhibits the characteristics of welldefined syntax and semantics

Examples of Formal ModelsThe applicability of Formal Methods to any particular softwaredevelopment activity is bounded by the ability to construct anappropriate formal model. Graphical models where the components of the diagram andthe connections between them have mathematically definedsyntax and semantics– e.g., control diagrams or state machines Textual based models such as Z or a subset of C or Ada thatare selected to have a mathematically defined syntax andsemantics Abstract models formed inside a Formal Methods tool by ananalysis of the software or system artifacts of interest such asthe code

Limitations of Formal Models A single model, or even a combination of models,may not be sufficient to capture all of the aspects ofa system– in many cases, it may not be possible to completely model asystem using a single formal notation – or even multiplenotations Requirements specified in natural language mayinclude system properties that cannot be reasonedabout with a formal method Models can be insufficiently detailed to allowmeaningful analysis of some properties and yetperfectly adequate for others

The Benefits of Formal Models Formal models, by themselves, have importantbenefits, because they are capable of:– unambiguously describing requirements and properties ofsoftware systems– enabling precise communication between engineers The biggest benefit is as the foundation for formalanalysis– that can be applied to provide assurance of properties andcompliance with requirements

Formal Analysis Formal analysis can provide guarantees or proofs ofsoftware system properties and compliance withrequirements. To conduct a formal analysis, a set of softwaresystem properties is necessary– these properties are either created or– they are embedded in specific tools that implement the formalanalysis e.g., Worst Case Execution Timing

What makes analysis formal A method is formal if it has a sound mathematicalbasis, typically given by a formal specificationlanguage– this basis provides a means of precisely defining notions likeconsistency and completeness, and more relevant, specification,implementation and correctness. [Ref. the Encyclopedia of Software Engineering] An analysis method has the soundness property ifand only if its inference rules prove only formulasthat are valid with respect to its semantics [Ref. Wiki]the method never assertsthat a property is truewhen it may not be true

Types of formal analysis Deductive methods, such as theorem proving– involve mathematical arguments, such as mathematicalproofs, for establishing a specified property of a formalmodel Model checking– works by exploring all reachable paths through a formalmodel to determine whether a specified property is satisfied Abstract Interpretation– used for constructing semantics-based analysis algorithmsfor the automatic, static and conservative determination ofdynamic properties of infinite-state programs

Deduction (Proof, Theorem Proving) Mathematical argument forestablishing some propertyof the system descriptionMathematicalModel(s)Property Constructed as a series ofsteps, each of which isjustified from a set of rulesAnalysis Eliminates ambiguity andsubjectivity inherent whendrawing informalconclusions May be manual but usuallyconstructed withautomated assistanceNo prooffoundEither falseOr more work to be doneProof

Model Checking State machine model of asystem is expressed in asuitable language Model checker determines ifMathematicalModelthe given finite state machinemodel satisfies requirementsexpressed as formulas in agiven logicPropertyAnalysis Basic method is to explore allreachable paths in acomputational tree derivedfrom the state machine model Answer: “correct" or acounter-example executionsequence is producedcounterexampleScenario thatviolates propertycorrectno result

Abstract Interpretation A formal method for automaticprogram analysis andverificationAbstractmodel The abstract model ispessimistic in that it considersall possible behavior in allapplicable executionenvironmentsAnalysis The program model isautomatically computed,directly from program text Can be tuned to be precise (nofalse alarm) and does scale up(to millions of lines)Probablynot okNeed to determineif error or false alarmOK

Formal Methods as a VerificationTechnique Formal Methods enable complete exploration of a formalmodel of possible behaviors or properties Subject to the fidelity of the modeling employed(which should be established by additional verification,as per guidance in this document), Formal Methodsprovides assurance that certain kinds of faults are notpresent– at the level of description and stage of the lifecycle consideredby the formal model The FM Supplement will provide guidance for using thisassurance to meet verification objectives of DO-178– either fully, or in conjunction with additional verification,including suitable complementary testing in the target hardware

Now – to Subgroup 6 Chaired by Duncan Brown (Rolls-Royce) and Kelly Hayhurst (NASA) CAST representative: Gary Horan (FAA) Advocates, practitioners and academicsRobert Annis (Smiths)Philippe Baufreton (Hispano-Suiza)Martin Beeby (Seaweed Systems)Guy Berthon (Thales)Matteo Bordin (AdaCore)Darren Cofer (Rockwell Collins)Herve Delseny (Airbus)Vincent Dovydaitis (Foliage)Louis Fabre (Eurocopter)Leonard Fulcher (TTTech)Ibrahim Habli (University of York)Michael Hennell (LDRA)Michael Holloway (NASA)Jeffrey Joyce (Critical Systems Lab)Emmanuel Ledinot (Dassault)Frederic Painchaud (DRDC-RDDC)Cyrille Rosay (EASA)Jamel Rauahi (Centre dEssaisAeronautique de Toulosue)Martin Schwarz (TTTech)Christel Seguin (ONERA)Peter Schmitt (IRA)Jean Souyris (Airbus)Elisabeth Strunk (Aerospace)Nick Tudor (Qinetiq)Rob Weaver (NATS)Mike Whalen (Rockwell Collins)Virginie Wiels (ONERA)Berndt Wloczyk (Airbus)formerly, Peter Amey (Praxis)

Work on the Supplement Section 1 – Introduction– additional background information on formal methods Section 2 – System Aspects & Section 3 – Software Life Cycle– no change Section 4, Software Planning– minor change, to include plans for using formal methods Section 5 – Software Development– some additional information on formal models Section 6 – Verification– this is the primary focus – and still a work in progress Section 7-10, no expected change Section 11 – Life Cycle Data– some additions to describe formal methods data

The Verification Challenge forFormal Methods The focus of DO-178B is verification bytest Some verification objectives imply amethod, i.e. testing Although testing is a powerfultechnique, the “return on investment” ofmodule testing and structural coverageis often questioned, especially withincreasing complexity Formal methods can prove propertiesof modules but cannot literally meetstructural coverage objectives as theobjective implies execution of the codeThis presentschallenges withrespect to the"core" document(178)andwith respect tocoming up with acomparablemeasure ofcoverage for formalmethods

Taking advantage of Airbus Airbus has successfully used some formal methods forcertification credit in their A380 program– worst case execution time computation of programs (Level A) using abstract interpretation (aiT)– stack analyzers for stack consumption computation (Levels A,B, and C) using abstract interpretation– proof of absence of Run Time Errors (Level A) using abstract interpretation (RTE-ENS)– unit-level proof of low level requirements in place of unit testing(Level A) using the deductive method (Caveat) We are leveraging the Airbus experience as much aspossible

General Challenge to doing aSupplement There are many different types of formal methods– trying to write guidance that covers all those methods is noteasy– not always easy to avoid describing "how to" do something Formal methods knowledge tends to be specialized– some formal methodists are model checkers, some are theoremprovers, – that is, there are few generalists that have a "big picture" view ofusing formal methods There is limited experience using formal methodsfor certification credit for many of the objectives– insufficient to establish best practice