Cet ouvrage fait partie de la bibliothèque YouScribe
Obtenez un accès à la bibliothèque pour le lire en ligne
En savoir plus

A gentle introduction to formal verification of computer systems

De
29 pages
A gentle introduction to formal verification of computer systems by abstract interpretation Patrick COUSOT a, Radhia COUSOT b a École normale supérieure and New York University b École normale supérieure and CNRS Abstract. We introduce and illustrate basic notions of abstract interpretation theory and its applications by relying on the readers general scientific culture and basic knowledge of computer programming. Keywords. Abstract interpretation, Formal methods, Verification, Static analysis. 1. Introduction Software is in all mission-critical and safety-critical industrial infrastructures since it is, in principle, the cheapest and most effective way to control complex systems in real time. However, all computer scientists have experienced costly bugs in embedded software. The failure of the Ariane 5.01 maiden flight [40] (due to an overflow), the failure of the Patriot missile [57] during the Gulf war (due to an accumulated rounding error), the loss of Mars orbiter [1] (due to a unit error), the crash of the twin-engined Chinook ZD 576 helicopter [8]1 are a few examples showing that mission-critical and safety-critical software can be far from being safe. Computer scientists agree on the fact that it is preferable to verify that mission- critical or safety critical software (and nowadays hardware) programs do not go wrong before running them. As an alternative to testing, which hardly scales up at reasonable costs and with a satisfactory coverage, automated formal verification has emerged, this last decade, as a promising useful complement, with interesting potential industrial ap- plications.

  • runtime properties

  • all mission-critical

  • int fact

  • make automatic proofs

  • program yields

  • static analysis

  • bugs

  • software

  • verify program


Voir plus Voir moins
AgentleintroductiontoformalverificationofcomputersystemsbyabstractinterpretationPatrickCOUSOTa,RadhiaCOUSOTbaÉcolenormalesupérieureandNewYorkUniversitybÉcolenormalesupérieureandCNRSAbstract.Weintroduceandillustratebasicnotionsofabstractinterpretationtheoryanditsapplicationsbyrelyingonthereadersgeneralscientificcultureandbasicknowledgeofcomputerprogramming.Keywords.Abstractinterpretation,Formalmethods,Verification,Staticanalysis.1.IntroductionSoftwareisinallmission-criticalandsafety-criticalindustrialinfrastructuressinceitis,inprinciple,thecheapestandmosteffectivewaytocontrolcomplexsystemsinrealtime.However,allcomputerscientistshaveexperiencedcostlybugsinembeddedsoftware.ThefailureoftheAriane5.01maidenflight[40](duetoanoverflow),thefailureofthePatriotmissile[57]duringtheGulfwar(duetoanaccumulatedroundingerror),thelossofMarsorbiter[1](duetoauniterror),thecrashofthetwin-enginedChinookZD576helicopter[8]1areafewexamplesshowingthatmission-criticalandsafety-criticalsoftwarecanbefarfrombeingsafe.Computerscientistsagreeonthefactthatitispreferabletoverifythatmission-criticalorsafetycriticalsoftware(andnowadayshardware)programsdonotgowrongbeforerunningthem.Asanalternativetotesting,whichhardlyscalesupatreasonablecostsandwithasatisfactorycoverage,automatedformalverificationhasemerged,thislastdecade,asapromisingusefulcomplement,withinterestingpotentialindustrialap-plications.Formalmethodsdatebacktotheearlydaysofcomputerscience(theFloyd/Naur/Hoareverificationmethod[33,51,37]appearedinthesixtieswithantecedentsgoingbacktoVonNeumannandTuring[38])andthepowerofpresent-daycomputersmakethemapplicabletolargescaleindustrialprojects.Theideaistomakeautomaticproofsatcompile-timetoverifyprogramruntimeproperties.1“Inthesummerof1993anindependentdefenceITcontractor,EDS-SCICON,wasinstructedtoreviewtheFADEC[FullAuthorityDigitalEngineControl]software;afterexaminingonly18percentofthecodetheyfound486anomaliesandstoppedthereview.”[8]
Beyondthedifficultyofspecifyingwhichruntimepropertiesareofinterest,allfor-malmethodsarefacedwithundecidability(themathematicalimpossibilityforacom-puter,whichisafinitedevice,toproveforsurenon-trivialpropertiesofthe(infiniteorextremelylarge)runtimebehaviorsofcomputerprograms)andcomplexity(theimpos-sibilityforcomputerstosolvedecidablequestionswithinareasonableamountoftimeandmemoryforlargeinputdata,suchasprogramexecutionsobservedoververylongperiodsoftime).Besidestestingwhichisnotaformalmethod,threemainapproacheshavebeencon-sideredforformalverification,allofthembeingapproximationsoftheprogramseman-tics(formallydefiningthepossibleexecutionsinallpossibleenvironments)formalizedbyabstractinterpretationtheory:Deductivemethodsproduceformalmathematicalcorrectnessproofsusingtheo-remproversorproofassistantsandneedhumaninteractiontoprovideinductivearguments(whichhardlyscalesupforlargeprogramswhicharemodifiedoverlongperiodsoftimes)andhelpinproofs(suchasproofhintsorstrategies);Model-checkingexhaustivelyexploresfinitarymodelsofprogramexecutions,whichcanbesubjecttocombinatorialexplosion,requiresthehumanproductionofmodels(ormaynotterminateincaseofautomaticrefinementofthemodel).Analternativeistoexplorepartiallythemodelbutthisisthendebugging,notverification;Staticanalysis,whichautomatestheabstractionoftheprogramexecution,alwaysterminatesbutcanbesubjecttofalsealarms(thatiswarningsthatthespecificationmaynotbesatisfiedalthoughnoactualexecutionoftheprogramcanviolatethisspecification).Inthispaper,weexplaininformallyandintuitivelytheunderlyingideasofabstractinterpretation-basedstaticanalysis,whichconsistsinabstractingtheprogramsemantics(formalizingprogramexecutions)toprovideasoundover-approximationofthepotentialerrorswithrespecttoaspecification.Staticanalysisinvolvesabstractionsoftheprogramsemanticsthatmustbecoarseenoughtobeeffectivelycomputableandpreciseenoughtoimplythepropertiesrequiredbythespecification.Toshowthatsuchabstractionsdoexistforgivenfamiliesofappli-cationsandspecifications,wereportontheASTRÉEanalyzer(www.astree.ens.fr/),whichisastaticanalyzerforprovingtheabsenceofruntime-errorsinsynchronous,time-triggered,real-time,safetycritical,embeddedsoftwarewrittenorautomaticallygener-atedintheCprogramminglanguage.Ithasbeensuccessfullyappliedtoprovetheab-senceofruntimeerrorsinthecontrol-commandpartoftheprimaryflightcontrolsoft-wareofthefly-by-wiresystemofairplanes.2.Softwarebugs2.1.NumericalsoftwarebugsLetusstartbyconsideringclassicalbugsinnumericalcomputations.
Un pour Un
Permettre à tous d'accéder à la lecture
Pour chaque accès à la bibliothèque, YouScribe donne un accès à une personne dans le besoin