Safety-critical systems, formal methods and standa

Safety-CriticalSystems,FormalMethodsandStandardsJonathanBowenOxfordUniversityComputingLaboratoryProgrammingResearchGroup11KebleRoad,OxfordOX13QD,UKTel:[phone](272574direct)Fax:[phone]Email:[e-mail]&VictoriaStavridouDepartmentofComputerScienceRoyalHollowayandBedfordNewCollegeUniversityofLondonEghamHill,Egham,SurreyTW200EX,UKTel:[phone](443429direct)Fax:[phone]Email:[e-mail]-CriticalSystems,FormalMethodsandStandardsJonathanBowenVictoriaStavridouAbstractStandardsconcernedwiththedevelopmentofsafety-criticalsystems,andthesoftwareinsuchsystemsinparticular,aboundtodayasthesoftwarecrisisincreasinglyaectstheworldofembeddedcomputer-basedsystems.Theuseofformalmethodsisoftenadvocatedasawayofincreasingcondenceinsuchsystems.Thispaperexaminestheindustrialuseofthesetechniques,therecommendationsconcerningformalmethodsinanumberofcurrentanddraftstandards,andcommentsontheapplicabilityandproblemsofusingformalmethodsforthedevelopmentofsafety-criticalsystemsofanindustrialscale.Somepossiblefuturedirectionsaresuggested.1ABriefHistoricalPerspectiveLiveshavedependedonmathematicalcalculationsforcenturies.Inthe19thcentury,thescienticcommunitywasfacingthe‘tablescrisis’[144]duetotheproblemoferrorsinnumericaltablessuchaslogarithmsandnavigationtables,calculatedbyhuman‘computers’.Itwasrumouredthatshipshadbeenwreckedasaresultofsucherrors.CharlesBabbagewassoconcernedthathedecidedtotrytoalleviatethesituationbyattemptingtomechanizetheprocessofgeneratingsuchtablesusing‘dierenceengines’andlatermoreversatileandprogrammable‘analyticalengines’,theforerunnersofmoderncomputers.Thersttrue‘real-time’computertobedevelopedwasontheWhirlwindprojectatMIT[5].Startedin1944,theprojectproducedanembryonic(military)airtraccontrolsystemin1951.Theshortlifetimeofthelargenumberofvacuumtubesusedinthecomputerwasaconsiderableproblem.Initially,themeantimebetweenfailureswasabout20minutes.Fault-tolerancewasachievedbydetectingweaktubesbeforetheyfailedandredirectingsignalstoothercomponents,thusenablingcontinuedoperationevenintheeventofpartialhardwarefailure[149].Atthistime,suchfailureswereadominantfeatureofthesystem.Computer-basedindustrialprocesscontrolfollowedbythelate1950s.Theproblemsofsoft-waredevelopmentandrevisionbecamerecognized,butthesolutionsremainedadhocandunre-liable[134].Eveninthemid1950s,thecostofproducingsoftwarehadalreadyoutstrippedthatofthecomputersthemselves.Thephysicalhardwarebecameincreasinglyreliable.Theproblemoffrequentbreakdowns,bulkinessandhighpowerconsumptionofvacuumtubeswasalleviatedbytheinventionofthetransistor.Despiteconsiderableimprovement,theconnectionsbetweencomponents(e.g.,‘dryjoints’betweensolderedwires)remainedaserioussourceoffailure.Theadventofintegratedcircuitsin1959,whilehelpingwiththisproblem,wasinitiallynotcost-eective.HowevertheUSspaceprogrammedemandedlow-weightandhigh-reliabilitycomponents{almostirrespectiveofcost{forthe(safety-critical)computerrequiredonboardthespacecraft.ThisenabledtheUStogaintheleadinthemicroelectronicsworldatthetime;subsequentlythepriceofintegratedcircuitsdroppedandthenumberoftransistorsperchipincreaseddramaticallyyearbyyear.1Similaradvanceswerenotforthcomingforsoftwarethatalsobecamemorecomplexbutlessreliable.Ascomputersbecamephysicallysmaller,itwasmoreandmorefeasibletoembedthemwithinthesystemsthattheycontrolled.In1971,Intelannouncedtherstcompletemicroprocessoronasinglechip,littlerealisingwhatanenormousimpactsuchanideawouldhaveontheworldofcomputing.Atthebeginningofthe1980s,embeddedsoftwarehadstillnotreallybeenconsideredseriouslybytheoreticalcomputerscienceresearchers(butsee[156]),despitethefactthatitiscapableofinictingphysicaldamage[14].Howeverinthelastdecade,suchsystemshavecomeundermoreandmorescrutinyascomputerspervadeallareasofourlives,especiallyinembeddedapplications.Thesoftwarecurrentlyusedincomputershasitselfbecomesocomplexthatitisnottrust-worthyandhascausedhumaninjuryanddeathasaresult.[108]providesalistofincidentsthatisupdatedannually.Upuntilrelativelyrecentlyithasnotbeenconsideredfeasibletouseformaltechniquestoverifysuchsoftwareinanindustrialsetting[61].Nowthatsomecasestudiesandexamplesofrealuseareavailable,formalmethodsarebecomingmoreacceptableinindustrialcircles.Evenpopulistaccountsofthecomputingindustryarementioningtheproblemsofsoft-wareerrorsinrelationtocriticalsystemsandthepossibilityofapplyingmathematicaltechniquestoreducesucherrorsinawidevarietyofforums[90,106,112,141].Thispaperbrieydiscussessafety-criticalsystems,examinestheuseofformalmethodsasapossibletechniqueforincreasingsafetyandreliability,andsurveyssomestandardsinthisarea.Theobjectiveofthepaperistoprovideinformationonthecurrentsafetyissues,particularlywithregardtosoftware,asreectedbyanumberofcurrentandemergingstandardsandtoexaminewaysinwhichformalmethodstechnologycanandhasbeenusedtoimprovesystemsafety.Itshouldbenotedthatformalmethodsareonlyoneofagamutofimportanttechniques,includingmanyclassicalsafetyan