Analysis of a Technical Description of the Airbus

AnalysisofaTechnicalDescriptionoftheAirbusA320BrakingSystemPeterB.LadkinCRIN-CNRS&INRIALorraine,B^atimentLORIA,BP239,54506Vanduvre-Les-Nancy,[e-mail]15,1995Abstract.WeanalysethedescriptionoftheoperationoftheAirbusA320brakingsystemscontainedintheFlightCrewOperatingManual.Weusethepredicate-actiondiagramsofLamporttoexpressandtocompletethedescription,andgivereasonswhysuchamorerigorousexpressionispreferable.1.IntroductionOnSeptember14th,1993,anAirbusA320landedatWarsawAirportinPolandinathunder-storm.Itoverrantheendoftherunway,surmountedanearthbank,andcametorestontheotherside.Twopeoplediedandotherswereinjuredinthisaccident[FI.93a,FI.93b,FI.93c,FI.93d,FI.93e].ThispaperanalysesthespecicationoftheA320brakingsystemcontainedintheFlightCrewOperatingManual[FCOM].Airplanesareprocedurally-orientedmachines.Manufacturersdevisewaysinwhichtheyshallbeownaspartofthecerticationprocess,anddescriptionsofthesemethods,aswellasdescriptionsofthesystemdesign,arerequireddocumentationoneveryaircraftthaties[FAR,Part91,SubpartA,Paragraph91.9].Crewsprogressthroughextensivetrainingon‘approvedprocedures’foryingtheaircraft.TheAirbusA320aircraftistherstaircraftincommercialoperationtousedigital‘y-by-wire’control,thatis,innormaloperation,theaircraftprimarycontrolisachievedbyelectronicactivationfromacomputerorseriesofcomputers(the‘ElectricalFlightControlSystem’[DM93])whichintegrateinputsfromsensorsandfrompilot‘requests’andcomputeoutputstothecontrolsurfaceactuators.TheA330,A340andtheforthcomingBoeing7772P.B.Ladkinarealso‘y-by-wire’.Thepilotisonemorecomputeruser,nolongerindirectphysicalcontrolofherairplane.Thesoftware-basedightcontrolsystemisspecied,designedandtestedontheground.Theaircraftisextensivelytestedintheair,althoughnoreasonableamountoftestingalonecanguaranteethereliabilitythatdesignersmustaimfor1,unlessthesystemdesignprocedureisknowninadvancetoguaranteethatlevelofsafety[BF93,LS92,LS93].WeanalysetheFCOMdescriptionofanairplane’ssystemsasahigh-levelspecication.Ahigh-levelspecicationisarigorousspecicationofasystemintermsofstatesandpredicatesthatareconsideredasatomicunitsatthehigh-level,whichmaybeanalysedintomorecomplexactions,ormorecomplexlogicalcombinationsofmore-renedstatepredicates,calleda‘lower-level’.ThemethodologyofspecicationandvericationusinghierarchicaldecompositionwaspioneeredbyDijkstra[Dij68]andextensivelydevelopedbyParnas[Par72,Par74].MilestonesystemstousethisapproachwereSRI’sPSOS[NBF+80]andSIFT[Wen78].See[Neu86]forarecentcontributiontothisarea.Weusestate-of-the-artlogicalmethods,thepredicate-actiondiagramsofLamport[Lam94b],whichdespitehavingalogicallyrigorousmeaningconcerningthestatesandactionsofasys-tem,requirelittlemoreoftheuserthanwhatshemustknowandusealready.WeanalysetheFCOMdescriptioninitially‘byhand’toidentifyinfelicitiesintheEnglish,andpotentialsemanticconfusions.Wethenidentifystatepredicatesandthesystemactionsandwritethedescriptionaspredicate-actiondiagrams.Finallywecriticiseandcompletethepredicate-actiondiagrams.WedonotassumemuchknowledgeoflogicotherthananabilitytoreadandunderstandBooleanlogicinEnglish,andapassingacquaintancewithacoupleoffeaturesoftemporallogic.FormaldetailsofLamport’sTemporalLogicofActions(TLA),onwhichpredicate-actiondiagramsarebased,maybefoundin[Lam94a].Therearenospecicmathematicalvericationstepsrequiredinthedevelopmentofsoft-wareforightcontrolsystems[RTCA92,para12].‘Practicaldemonstration’maybeused,despitefundamentalproblemswithdemonstratingthesesystemstotherequiredlevelofre-liability,aswenoteinSection1.3.Nevertheless,thehierarchicaldesignandspecicationmethodologieshavebeenemployedandtheiradvantagesrecognisedforaquartercentury.See[Rus93]foradetaileddiscussionofsuccessesandfailures,andprospects.WebelievetherearebenetsfromconsideringFCOMdescriptionsashigh-levelspecicationsofcomplexair-craftsystems,subjecttothesamelevelofrigorousanalysisasanyotherspecicationofasafety-criticalsystem.Thiswouldensurethatthespecicationiscorrectatthehigh-level,andthatthelower-levelimplementationsindeeddowhattheOperatingManualsaystheyshoulddo.Thisconfersmorerigoronthesystemdevelopmentprocess,aswellasensuringtheconsiderableadvantagetothecrewthatthedescriptiontheyhaveisrelativelycomplete,correct,andnotopentomisinterpretation.Wesuggestthatightcrew,whoareexpectedtounderstandBooleanlogicanyway[FCOM,1.27.10,P11,below],shouldhaveacomplete,accuratespecicationofsystemoperationatthehighlevelfromwhichtowork.Weshowthatsuchaspecicationmaybeprovidedusingpredicate-actiondiagrams,withlittleifanycomplexityoverandabovetheBooleanlogicex-1Noreliabilitynumberforsoftwarealoneisrequiredin[RTCA92],sinceitisaprocessstandard.Thereisarequirementofafailurerateof109perighthourfortheEFCSasawhole,includingsoftwareAnalysisofaTechnicalDescriptionoftheAirbusA320BrakingSystem3pressedinEnglishthatiscurrentlyused.Thisisinlinewithcurrentindustrythinking,asinthetaskforceconvenedtostudyproblemswithcontrolledightintoterrain{\treatingwhathappensonanaircraftightdeckasthenextstageinaprocessthatbeginswiththe