WIXLIB

permits discussion of formal methods according tothe major life cycle processes called out in DO178B/ED-12B,especiallydevelopmentandverification processes. Development processes areapplicable to formal models, and verificationprocesses are applicable to formal analyses.In general, a model is an abstract representation of agiven set of aspects of the software that is used foranalysis, simulation and/or code generation. In acertification context, to be formal, a model must havean unambiguous, mathematically defined syntax andsemantics. This makes it possible to use automatedmeans to obtain guarantees that the model hascertain specified properties.Although there are important benefits in creatingformal models of life cycle artifacts, the mostpowerful benefits of formal methods are in the formalanalysis of those models. Formal analysis canprovide guarantees or proofs of software propertiesand compliance with requirements. Proof, orguarantee, implies that all execution cases are takeninto account. For the purpose of the FMTS, ananalysis method can only be regarded as formalanalysis if its determination of a property is sound.Sound analysis means that the method neverasserts a property to be true when it may not betrue.There are many different kinds of formal analysis,but they can typically be classified in threecategories: (1) deductive methods, such as theoremproving, (2) model checking, and (3) ematicalarguments, such as mathematical proofs, forestablishing a specified property of a formal model.A correct proof of a property provides rigorousevidence of that property for the formal model.These proofs are typically constructed using anautomated or interactive theorem proving system.Even with such assistance, constructing proofs canbe difficult, or impossible in some cases. However,once a proof is completed, automatic checking of thecorrectness of that proof is usually trivial.Model checking explores all possible behaviors of aformal model to determine whether a specifiedproperty is satisfied. In cases where the property isnot satisfied, a counter-example is generatedautomatically illustrating where and how the propertyfails to hold. In some cases, a model checker maynot be able to determine if the given property holds;for example, in cases where the complexity of themodel exceeds the capacity of the model checker.used for constructing semantics-based analysisalgorithms to determine dynamic properties ofinfinite-state programs. With abstract interpretation,a formal model is generated, usually within a toolthat is specific to the particular property underanalysis. It can be viewed as a partial execution of acomputer program which determines specific effectsof the program (e.g., control structure, flow ofinformation, stack size, number of clock cycles)without actually performing all the calculations.4. Development using formal methodsThe development artifacts shown in Figure 1 can bespecified using a formal model. This is no different,in effect, from using any other language to specify adevelopment artifact, except that using a formalnotation allows some of the verification objectives tobe satisfied by the use of formal analysis.Formalizing requirements or design may increasethe effort required to specify them, compared withusing more conventional languages, but may resultin additional errors being found and removed earlierduring this process due to the additional scrutinyinherent in applying a formal notation.It is worth noting that not all of the requirements forany given development artifact need to be definedformally when using a formal method. For thoserequirements which are not formally defined, DO178/ED-12 guidance should be used.From the perspective of meeting the DO-178B/ED12B objectives for development, no special guidanceis needed when using formal methods. If theapplicant does not plan to use formal analysis in theverification, then there is no need to comply with theFMTS.In cases where formal analysis is planned, thedevelopment activities should ensure that there issufficient definition in the formal model to verifyproperties about the artifacts being analyzed. Thesoftware architecture can be analyzed independentlyof low level requirements. In the same way low levelrequirements can be analyzed independently of highlevel and architectural requirements. Some methodscreate a formal model at the source code level,embedding information flow from the design into thecode, which is then checked by formal analysis. Itmay even be possible to apply formal methods toanalyze properties of object code. In this case,object code is a formal model whose semantics aretreated the same by the formal analysis as they areby the target hardware.Abstract Interpretation is a theory for formallyconstructing conservative representations (i.e.enforcing soundness) of the semantics ofprogramming languages. In practice, this method isERTS 2010 – 19-21 May 2010 – ToulousePage 3/7

5. Verification using formal methodsWith formal analysis, the correctness of life cycledata with respect to a formal model or property cangenerally be proved or disproved; therefore, formalanalysis is able to replace the conventional methodsof review, analysis, and test, as specified in DO178B/ED-12B, for some verification objectives. Theguidance proposed for the FMTS details thepotential use of formal methods at eachdevelopment level and gives the conditions for theuse of a given formal analysis for a given verificationobjective.Meeting the DO-178B/ED-12B objectives forverification of verification process results is morecomplicated when formal analysis is used. In caseswhere testing alone is used, verification ofverification is accomplished by a coverage analysisto guarantee that software has been tested enough.However, test coverage metrics, such as decisioncoverage or modified condition/decision coverage,are not meaningful for analyzing the sufficiency of aformal analysis. For the FMTS, an alternativeapproach to coverage is proposed when formalanalyses are used to replace some testing.d. Compatibility with the target computer: Formalanalysis can be used to detect potential conflictsbetween a formal description of the targetcomputer and the life cycle data item.e. Verifiability:Being able to express arequirement in the formal notation defined in thesoftware verification plan is evidence ofverifiability in the same way as being able todefine a test case. In some cases, formalanalysis is better able to verify a requirementthen testing.For example, requirementsinvolving “always/never” cannot in general beverified by a finite set of test cases, but may beverified by formal analysis.f.5.1 Reviews and analysesFor requirements (HLR and LLR), architecture andsource code, the use of formal methods is aparticular case of analysis. Thus the “only” guidanceneeded for formal analysis in these cases is thecriteria and conditions for the use of formal methodsfor each development process; the objectives havenot been modified. That is, formal analysis can beused to satisfy the objectives for software reviewsand analysis, as shown in Figure 2, as follows:a. Compliance: If the life cycle data items thatcomprise the inputs and outputs of a softwaredevelopment process are formally modeled, thenformal analysis can be used to verifycompliance. Compliance can be demonstratedby showing that the output satisfies the input.Formal methods cannot show that a derivedrequirement is correctly defined and has areason for existing; this must be achieved byreview.b. Accuracy: Formal notations are precise andunambiguous, and can be used to demonstrateaccuracy of the representation of a life cycledata item.c.Consistency: Life cycle data items that areformally expressed can be checked forconsistency (the absence of conflicts). If a set offormal statements is found to be logicallyinconsistent then the inconsistencies must beaddressed before any subsequent analysis isconducted.ERTS 2010 – 19-21 May 2010 – ToulouseConformance to standards: Life cycle dataitems that are formally expressed must becompliant with any standards defining theformalism. Invalid results will be obtained if illformed requirements are allowed. Since formalnotations have a well-defined syntax, automatedsyntax checkers are appropriate for verifying thatthe formally stated requirements are well-formedwith respect to syntax. In addition, an automatedchecker may enforce other restrictions on thenotation (e.g., complexity of notationalconstructs and other design constructs thatwould not comply with the system safetyobjectives). Automated checking will need to besupplemented by review for those standards notamenable to automated checking.g. Traceability: Traceability ensures that all inputrequirements have been developed into lowerlevel requirements or source code. Traceabilityfrom the inputs of a process to its outputs can bedemonstrated by verifying with a formal analysisthat the outputs of the process fully satisfy itsinputs.Traceability from the outputs of aprocess to its inputs can be demonstrated byverifying with a formal analysis that each outputdata item is necessary to satisfy some input dataitem.h. Algorithm aspects: If life cycle data items areformally modeled, then algorithmic aspects canbe checked using formal analysis.i.Requirement formalization correctness: If arequirement has been translated to a formalnotation as the basis for using a formal analysis,then review or analysis should be used todemonstrate that the formal statement is aconservative representation of the informalrequirement. It is important to note that thepreciseness of formal notations is only anadvantage when they maintain fidelity to theintent of the informal requirement. If thesemantic gap between an informal statement ofthe requirement and its embodiment in a formalPage 4/7

notation is too large, then establishing that theformal statement is conservative may be difficult.SystemRequirements5.2 TestUsing formal analysis to meet the verificationobjectives for executable object code is the biggestchallenge for providing guidance because test is theonly means envisaged in DO-178B/ED-12B formeeting those requirements. Replacing all testing atthis level by formal analysis is not possible at thistime; but formal methods can replace test for someproperties, such as worst case execution time orstack usage. Formal methods can also be used toverify the compliance of the executable object codewith respect to high level or low level requirements.However, testing will always remain mandatory andwill be the primary means for verification of theexecutable object ause formal methods cannot replace all testing,verification objectives for executable object code arethe same when using formal methods as for test inDO-178B/ED-12B. However, an additional objective,as follows, is needed when formal analysis is usedto verify properties of the executable object code: ComplianceRobustnessComplianceRobustness5.3 Verification of verificationCoverage analysis in DO-178B/ED-12B is defined intwo steps:-requirements-basedensure that testrequirement;coverage analysis, tocases exist for each-structural coverage analysis, to ensure that thecode structure has been sufficiently exercised bytest cases.ERTS 2010 – 19-21 May 2010 – ToulouseComplianceRobustnessSourceCodeAnalysis of property preservation betweensource code and object code. For the formalanalysis of source code to be used asverification evidence for the target system,verification should be performed to establishproperty preservation between source andobject code. By verifying the correctness of thetranslation of source to object code, formalanalysis performed at the source code levelagainst high or low level requirements can beused to infer correctness of the object codeagainst high or low level requirements. This issimilar to the way that coverage metrics gainedfrom source code can be used to establish theadequacy of tests to verify the target system.This allows for alternative verification paths for theexecutable object code, as shown in Figure 3. Forexample, compliance of object code to LLR can bedemonstrated using formal analysis on source codeand analysis of property preservation betweensource code and object erty PreservationExecutableObject CodeDevelopment activityReview/Analysis activityTest activityFormal AnalysisNote: Requirements include Derived RequirementsFig 3. Alternative verification pathsRequirements-based coverage analysis can be donedirectly when using formal methods by showing thatformal analysis cases exist for each requirement.Structural coverage however is a notion stronglyconnected with test and execution of code. To beable to define an alternative to structural coverageanalysis, the objectives of structural coverageanalysis have to be examined. These objectives, asgiven in DO-178B/ED-12B, are to detect:-shortcomings in requirements-based cases orprocedures,-inadequacies in software requirements,Page 5/7

-dead or deactivated code.When a code structure is not covered by some testcases, then either some test cases are missing for agiven requirement, a requirement is missing, or thecode structure is dead or deactivated.When using formal methods, verification isexhaustive, so a requirement that has been verifiedformally has been completely covered. However,there is no guarantee that a requirement has notbeen forgotten. Thus, it is necessary to have ameans to ensure the completeness of the set ofrequirements. Similarly, it is necessary to have ameans to ensure that there is no unidentified dead ordeactivated code.Consequently, the solution proposed to providecoverage when using formal analysis at theexecutable object code level is meet the followingset of fours objectives:Complete Coverage of Each RequirementThe most thorough verification would be where allpossible paths through the code with all possibledata values are considered. Formal methods ensurethis but sometimes the formal analysis requiresassumptions to be made about the software system.All such assumptions should be verified.Completeness of the Set of RequirementsWhere requirements are formally modeled, it shouldbe demonstrated that the set of requirements iscomplete with respect to the intended functions. Thatis: For all input conditions the required output hasbeen specified. For all outputs the required input conditions havebeen specified.If the set of requirements is found to be incompletethen additional requirements (generally not derivedrequirements) should be added. If a demonstrationof completeness cannot be achieved, then structuralcoverage analysis must be used.Detection of Unintended Dataflow RelationshipsVerifying that the information flow in the source codecomplies with the requirements ensures that thereare no unintended dependencies between the inputsand outputs of the code. If unintended dependenciesexist then these must be resolved either by addingthe missing requirements (generally not derivedrequirements) or removing the erroneous code.Detection of Dead Code and Deactivated CodeGuidance for dead and deactivated code is notdifferent when using formal analysis from using test.In both cases, dead and deactivated code should beERTS 2010 – 19-21 May 2010 – Toulouseidentified by review or analysis and dealt with as perthe guidance in DO-178B/ED-12B.6. Specific objectivesPrevious sections have addressed how formalmethods can satisfy the objectives currently definedin DO-178B/ED-12B. The proposed guidance for theFMTS also includes some additional objectivesconcerning the formal methods that are used.When formal analysis is used to meet the verificationobjectives of DO-178/ED-12, the formal methodshould be correctly defined and justified as follows:a. All notations used for formal analysis should beverified to have precise, unambiguous,mathematically defined syntax and semantics;i.e., they are formal notations.b. The soundness of each formal analysis methodshould be justified. A sound method neverasserts that a property is true when it may not betrue.c.All assumptions related to each formal analysisshould be described and justified (e.g., thoseassociated with the target computer; those aboutthe data range limits; etc.).The first objective requires demonstration that themethod used is formal. The second one restricts theuse of formal methods to sound methods. (Not allformal methods are sound.) The last one focuses onassumptions because assumptions are often usedby formal analyses and it is important for thecorrection of the analysis that they are all justified.7. Benefits of using formal methodsFormal methods were developed as a branch ofcomputer science in order to reason morescientifically about software. Initially the advantagesof formal methods were in analyzing the behavior ofsource code to understand where this was incorrect.Since those early applications of this approach in the1970’s, the problem of error prone source code hasreduced and instead most of the errors in softwaredevelopment are now generally accepted as beingattributable to requirement errors.It has become apparent that creating formalrepresentations or models of requirements can helpto address this problem in the same way as it didwith source code. In that respect, formal methodshave the potential for both increasing safety anddecreasing the cost of certifying flight-criticalsystems. Specific benefits include improvingrequirements, reducing error introduction, improvingerror detection, and reducing cost. Secondly, theformality of the description allows us to carry outPage 6/7

rigorous analyses. Such analyses can verify usefulproperties such as consistency, deadlock-freedom,satisfaction of high level requirements, orcorrectness of a proposed design.7.1 Improve RequirementsExperience shows that the act of capturingrequirements using formal notations is of benefit: itforces the writer to ask questions that wouldotherwise be postponed until coding. Using a formalnotation to capture requirements provides a simplevalidation check, as it forces a level of explicitnessfar beyond that needed for informal representations.Requirements expressed in a formal notation canalso be analyzed early to detect inconsistency andincompleteness and therefore remove errors thatwould normally not be found until later in thedevelopment process.7.2 Reduce Error IntroductionWriting high or low level requirements formallyimproves the quality of the development artifacts.Formalized requirements prevent misunderstandingsthat lead to error introduction. As developmentproceeds, compliance can be continually checkedusing a formal analysis to ensure that errors havenot been introduced.A further advantage of using formal methods at therequirements level is the ability to derive or refinefrom these requirements the code itself, thusensuring that no errors are introduced at this stage.Alternatively their use at the requirements levelallows formal analysis to establish correctnessbetween requirements and code.7.3 Improve Error DetectionFormal analysis can provide exhaustive verificationat whatever levels it is applied: high levelrequirements, low level requirements, source codeor executable. Exhaustive verification means that allof the structure is verified over all possible inputsand states. This can detect errors that would bedifficult or impossible to find using only a test basedapproach.7.4 Reduce CostIn general, software errors are less expensive tocorrect the earlier in the development lifecycle theyare detected. The effort required to generate formalmodels is generally more than offset by the earlyERTS 2010 – 19-21 May 2010 – Toulouseidentification of errors.That is, when formalmethods are used early in the lifecycle, they canreduce the overall cost of the project. Whenrequirements have been formalized the costs ofdownstream activities are reduced. Formal notationsalso reduce cost by enabling the automation ofverification activities.8. ConclusionA primary motivation for developing guidance forusing formal methods in a certification context wasto better enable the routine use of mature formalmethods. That guidance, as proposed to date in aFMTS to DO-178/ED-12, allows adoption of formalmethods into an established set of processes fordevelopment and verification of an avionics systemto be an evolutionary refinement rather than anabrupt change of methodology. Formal methodsmight be used in a very selective manner to partiallyaddress a small set of objectives, or might be theprimary source of evidence for the satisfaction ofmany of the objectives concerned with developmentand verification.This paper has presented a synthesis of the effort ofthe Formal Methods Sub-group of RTCA SC205/EUROCAE WG-71 in developing guidance forusing formal methods in these ways in a certificationcontext with DO-178/ED-12.Ongoing work in the formal methods sub-groupconcerns a discussion paper that is intended to giveseveral examples of the use of formal methods.9. AcknowledgementThis paper presents the work of RTCA SC-205/EUROCAE WG-71 sub-group 6, we thank allmembers of SG6.10. References[1] RTCA/DO-178B, EUROCAE/ED-12B: SoftwareConsiderations in Airborne Systems and EquipmentCertification, December 1, 1992.[2] Advisory Circular # 20-115B. U. S. Department ofTransportation, Federal Aviation Administration,issued January 11, 1993.Page 7/7

For the past four years, RTCA and EUROCAE have sponsored a joint special committee/working group (SC-205/WG-71) to update DO-178B/ED-12B to take into account and facilitate the appropriate use of new software engineering techniques that have emerged since 1992. The committee is updating the core document DO-178B/ED-12B, and four new