Safety-critical systems, formal methods and standa

zhaowenhua
1 ℃
2020-01-25

整理文档很辛苦，赏杯茶钱您下走！

还剩 ... 页未读，继续阅读 >>

免费阅读已结束，点击下载阅读编辑剩下 ... 页

阅读已结束，您可以下载文档离线阅读编辑

资源描述

Safety-CriticalSystems,FormalMethodsandStandardsJonathanBowenOxfordUniversityComputingLaboratoryProgrammingResearchGroup11KebleRoad,OxfordOX13QD,UKTel:+44-865-273838(272574direct)Fax:+44-865-273839Email:Jonathan.Bowen@comlab.ox.ac.uk&VictoriaStavridouDepartmentofComputerScienceRoyalHollowayandBedfordNewCollegeUniversityofLondonEghamHill,Egham,SurreyTW200EX,UKTel:+44-784-434455(443429direct)Fax:+44-784-443420Email:victoria@cs.rhbnc.ac.ukRevisedDecember1992.ToappearintheSoftwareEngineeringJournal.Safety-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