A gentle introduction to formal verification of computer systems

pages

English

Documents

Écrit par
Patrick Cousot

Publié par
pefav

Lire un extrait

Obtenez un accès à la bibliothèque pour le consulter en ligne En savoir plus

Découvre YouScribe en t'inscrivant gratuitement

Je m'inscris

Découvre YouScribe en t'inscrivant gratuitement

Je m'inscris

pages

English

Ebook

Lire un extrait

Obtenez un accès à la bibliothèque pour le consulter en ligne En savoir plus

Publié par

pefav

Nombre de lectures

Langue

English

Poids de l'ouvrage

11 Mo

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

Publié par

pefav

Nombre de lectures

Langue

English

Poids de l'ouvrage

11 Mo

AgentleintroductiontoformalveriﬁcationofcomputersystemsbyabstractinterpretationPatrickCOUSOTa,RadhiaCOUSOTbaÉcolenormalesupérieureandNewYorkUniversitybÉcolenormalesupérieureandCNRSAbstract.Weintroduceandillustratebasicnotionsofabstractinterpretationtheoryanditsapplicationsbyrelyingonthereadersgeneralscientiﬁccultureandbasicknowledgeofcomputerprogramming.Keywords.Abstractinterpretation,Formalmethods,Veriﬁcation,Staticanalysis.1.IntroductionSoftwareisinallmission-criticalandsafety-criticalindustrialinfrastructuressinceitis,inprinciple,thecheapestandmosteffectivewaytocontrolcomplexsystemsinrealtime.However,allcomputerscientistshaveexperiencedcostlybugsinembeddedsoftware.ThefailureoftheAriane5.01maidenﬂight[40](duetoanoverﬂow),thefailureofthePatriotmissile[57]duringtheGulfwar(duetoanaccumulatedroundingerror),thelossofMarsorbiter[1](duetoauniterror),thecrashofthetwin-enginedChinookZD576helicopter[8]1areafewexamplesshowingthatmission-criticalandsafety-criticalsoftwarecanbefarfrombeingsafe.Computerscientistsagreeonthefactthatitispreferabletoverifythatmission-criticalorsafetycriticalsoftware(andnowadayshardware)programsdonotgowrongbeforerunningthem.Asanalternativetotesting,whichhardlyscalesupatreasonablecostsandwithasatisfactorycoverage,automatedformalveriﬁcationhasemerged,thislastdecade,asapromisingusefulcomplement,withinterestingpotentialindustrialap-plications.Formalmethodsdatebacktotheearlydaysofcomputerscience(theFloyd/Naur/Hoareveriﬁcationmethod[33,51,37]appearedinthesixtieswithantecedentsgoingbacktoVonNeumannandTuring[38])andthepowerofpresent-daycomputersmakethemapplicabletolargescaleindustrialprojects.Theideaistomakeautomaticproofsatcompile-timetoverifyprogramruntimeproperties.1“Inthesummerof1993anindependentdefenceITcontractor,EDS-SCICON,wasinstructedtoreviewtheFADEC[FullAuthorityDigitalEngineControl]software;afterexaminingonly18percentofthecodetheyfound486anomaliesandstoppedthereview.”[8]

Beyondthedifﬁcultyofspecifyingwhichruntimepropertiesareofinterest,allfor-malmethodsarefacedwithundecidability(themathematicalimpossibilityforacom-puter,whichisaﬁnitedevice,toproveforsurenon-trivialpropertiesofthe(inﬁniteorextremelylarge)runtimebehaviorsofcomputerprograms)andcomplexity(theimpos-sibilityforcomputerstosolvedecidablequestionswithinareasonableamountoftimeandmemoryforlargeinputdata,suchasprogramexecutionsobservedoververylongperiodsoftime).Besidestestingwhichisnotaformalmethod,threemainapproacheshavebeencon-sideredforformalveriﬁcation,allofthembeingapproximationsoftheprogramseman-tics(formallydeﬁningthepossibleexecutionsinallpossibleenvironments)formalizedbyabstractinterpretationtheory:•Deductivemethodsproduceformalmathematicalcorrectnessproofsusingtheo-remproversorproofassistantsandneedhumaninteractiontoprovideinductivearguments(whichhardlyscalesupforlargeprogramswhicharemodiﬁedoverlongperiodsoftimes)andhelpinproofs(suchasproofhintsorstrategies);•Model-checkingexhaustivelyexploresﬁnitarymodelsofprogramexecutions,whichcanbesubjecttocombinatorialexplosion,requiresthehumanproductionofmodels(ormaynotterminateincaseofautomaticreﬁnementofthemodel).Analternativeistoexplorepartiallythemodelbutthisisthendebugging,notveriﬁcation;•Staticanalysis,whichautomatestheabstractionoftheprogramexecution,alwaysterminatesbutcanbesubjecttofalsealarms(thatiswarningsthatthespeciﬁcationmaynotbesatisﬁedalthoughnoactualexecutionoftheprogramcanviolatethisspeciﬁcation).Inthispaper,weexplaininformallyandintuitivelytheunderlyingideasofabstractinterpretation-basedstaticanalysis,whichconsistsinabstractingtheprogramsemantics(formalizingprogramexecutions)toprovideasoundover-approximationofthepotentialerrorswithrespecttoaspeciﬁcation.Staticanalysisinvolvesabstractionsoftheprogramsemanticsthatmustbecoarseenoughtobeeffectivelycomputableandpreciseenoughtoimplythepropertiesrequiredbythespeciﬁcation.Toshowthatsuchabstractionsdoexistforgivenfamiliesofappli-cationsandspeciﬁcations,wereportontheASTRÉEanalyzer(www.astree.ens.fr/),whichisastaticanalyzerforprovingtheabsenceofruntime-errorsinsynchronous,time-triggered,real-time,safetycritical,embeddedsoftwarewrittenorautomaticallygener-atedintheCprogramminglanguage.Ithasbeensuccessfullyappliedtoprovetheab-senceofruntimeerrorsinthecontrol-commandpartoftheprimaryﬂightcontrolsoft-wareoftheﬂy-by-wiresystemofairplanes.2.Softwarebugs2.1.NumericalsoftwarebugsLetusstartbyconsideringclassicalbugsinnumericalcomputations.

Voir

Univers
Ebooks
Livres audio
Presse
Podcasts
BD
Documents

A gentle introduction to formal verification of computer systems

YouScribe

Le catalogue

Le service

Les conditions