Design and Implementation of a Special Purpose Static Program Analyzer

Time Embedded

Description

Niveau: Supérieur
Design and Implementation of a Special-Purpose Static Program Analyzer for Safety-Critical Real-Time Embedded Software Bruno Blanchet1, Patrick Cousot1, Radhia Cousot2, Jerome Feret1, Laurent Mauborgne1, Antoine Mine1, David Monniaux1, Xavier Rival1 1 CNRS & Ecole normale superieure, 75005 Paris, France 2 CNRS & Ecole polytechnique, 91128 Palaiseau cedex, France Abstract. We report on a successful preliminary experience in the de- sign and implementation of a special-purpose Abstract Interpretation based static program analyzer for the verification of safety critical embed- ded real-time software. The analyzer is both precise (zero false alarm in the considered experiment) and efficient (less than one minute of analysis for 10,000 lines of code). Even if it is based on a simple interval analysis, many features have been added to obtain the desired precision: expan- sion of small arrays, widening with several thresholds, loop unrolling, trace partitioning, relations between loop counters and other variables. The efficiency of the tool mainly comes from a clever representation of abstract environments based on balanced binary search trees. Dedicated to Neil Jones, for his 60th birthday. 1 Introduction 1.1 General-Purpose Static Program Analyzers The objective of static program analysis is to automatically determine run-time properties, statically, that is, at compile-time. This problem is in general un- decidable, so static program analysis relies on approximations as formalized by Abstract Interpretation [8,9].

• program analyzers


• real


• software model


• problems such


• effectiveness problems


• general-purpose static


• safety critical


• special-purpose static

Sujets

• France 2
• École polytechnique
• Embedded

Informations

• Publié par: chaeh
• Nombre de lectures: 15
• Langue: English

Extrait

DesignandImplementationof aSpecial-PurposeStaticProgramAnalyzer forSafety-CriticalReal-TimeEmbedded Software BrunoBlanchet 1 ,PatrickCousot 1 ,RadhiaCousot 2 ,Je´roˆmeFeret 1 , LaurentMauborgne 1 ,AntoineMine´ 1 ,DavidMonniaux 1 ,XavierRival 1 1 CNRS&E ´ colenormalesupe´rieure,75005Paris,France 2 CNRS&E ´ colepolytechnique,91128Palaiseaucedex,France Abstract. Wereportonasuccessfulpreliminaryexperienceinthede- signandimplementationofaspecial-purposeAbstractInterpretation basedstaticprogramanalyzerfortheverificationofsafetycriticalembed- dedreal-timesoftware.Theanalyzerisbothprecise(zerofalsealarmin theconsideredexperiment)andefficient(lessthanoneminuteofanalysis for10,000linesofcode).Evenifitisbasedonasimpleintervalanalysis, manyfeatureshavebeenaddedtoobtainthedesiredprecision:expan- sionofsmallarrays,wideningwithseveralthresholds,loopunrolling, tracepartitioning,relationsbetweenloopcountersandothervariables. Theefficiencyofthetoolmainlycomesfromacleverrepresentationof abstractenvironmentsbasedonbalancedbinarysearchtrees. DedicatedtoNeilJones,forhis60 th birthday. 1Introduction 1.1General-PurposeStaticProgramAnalyzers Theobjectiveofstaticprogramanalysisistoautomaticallydeterminerun-time properties,statically,thatis,atcompile-time.Thisproblemisingeneralun- decidable,sostaticprogramanalysisreliesonapproximationsasformalizedby AbstractInterpretation[8,9].Forexample,typableprogramsdonotgowrong butuntypableprogramsdonotallgowrong. Inmanycontexts,suchasprogramtransformation,theuncertaintyinduced bytheapproximationisacceptable.Forexample,intervalanalysiscanbeused toeliminateuselessarrayboundchecksatrun-time[7].Theselectionrate(i.e. theproportionofpotentialalarmsthataredefinitivelysolvedeitherpositively ornegatively)isoftenbetween80and95%,sotheoptimizationisworthwhile. Moreover,itiscorrectsincetheremaining5to20%casesforwhichtestscannot beeliminatedatcompile-timewillbecheckedatrun-time.Sometimes,static programanalysiscandiscoverdefiniteerrorsatcompile-time(e.g.uninitialized variables),whichisusefulfordebugging.Theobjectivesofsuch general-purpose staticprogramanalyzers are:

1.tofullyhandleageneralpurposeprogramminglanguage(suchasAdaorC, includingthestandardlibraries); 2.torequirenouser-providedspecification/annotation(exceptmaybelight onessuchas,e.g.,rangesofinputvariablesorstubsforlibraryfunctions thesourceofwhichisnotavailable); 3.tobepreciseenoughtoprovideinterestinginformationformostprograms (e.g.informationpertinenttostaticprogrammanipulationordebugging); 4.tobeefficientenoughtohandleverylargeprograms(fromacostofafew megabytesandminutestogigabytesandhourswhendealingwithhundreds ofthousandsofsourcecodelines). Suchgeneral-purposestaticprogramanalyzersareverydifficulttodesignbe- causeofthecomplexityofmodernprogramminglanguagesandsystems.Some arecommerciallyavailableandhavehadsuccessesinrepairingfailuresorpre- ventingthemintheearlydevelopmentofprograms.Sincethecoverageis100%, thefalsealarmscanbehandled,e.g.,byclassicaltestingmethods,thusreduc- ingtheneedforactualtestofabsenceofrun-timeerrorbyaneconomically significantfactorof80to95%. 1.2ProgramVerification Inthecontextofsafetycriticalreal-timesoftwareasfound,e.g.,inthetrans- portationindustry,run-timecheckingoferrorsmaynotbeacceptableatall. Hence,thedebuggingcostisveryhighandsignificantlyhigherthanthesoftware developmentcostitself.Inthisparticularindustrialcontextwherecorrectness isrequiredbysafetyandcriticality,rigorousformalmethodsshouldbedirectly applicableandeconomicallyaffordable. DeductiveMethods. Inpractice,deductivemethods(see,forexample,[1,17]) arehardtoapplywhenlackingaformalspecificationandwhentheprogram sizeisverylarge.Indeed,thecostfordevelopingthespecificationandtheproof, evenwithaproofassistantoratheoremprover,isingeneralmuchhigherthan thecostfordevelopingandtestingoftheprogramitself(figuresof600person- yearsfor80,000linesofCcodehavebeenreported).Onlycriticalpartsofthe softwarecanbecheckedformallyanderrorsappearelsewhere(e.g.atinterfaces). Moreover,forembeddedsoftwarewithalifetimeoftentotwentyyears,both theprogramanditsproofhavetobemaintainedoverthatlongperiodoftime. SoftwareModelChecking. Softwaremodelchecking(see,forexample,[12]) isalsohardtoapplywhenlackingaformalspecificationandwhentheprogram sizeisverylarge.Thisisbecausethecostofdevelopingboththespecificationand themodeloftheprogramcanalsobeverylarge.Problemssuchasthedifficulty toprovidesensibletemporalspecificationsorthestateexplosionarewell-known. Ononehand,ifthemodelisnotprovedcorrect,thentheprogramcorrectness checkisnotrigorousandmostlyamountstodebugging.Ontheotherhand,the