SoftwareVerification
MardavijRoozbehani1,EricFeron2,andAlexandreMegrestki3
mardavij@mit.edu,2feron@mit.edu,3ameg@mit.eduLaboratoryforInformationandDecisionSystems(LIDS),MassachusettsInstituteofTechnology,Cambridge,MA,U.S.A
1
Abstract.Modelingandanalysistechniquesarepresentedforreal-time,safety-criticalsoftware.Softwareanalysisisthetaskofverifyingwhetherthecomputercodewillexecutesafely,freeofrun-timeerrors.Thecriti-calpropertiesthatprovesafeexecutionincludebounded-nessofvariablesandterminationoftheprograminafinitenumberofsteps.Inthispa-per,dynamicalsystemrepresentationsofcomputerprogramsalongwithspecificmodelsthatarepertinenttoanalysisviaanoptimization-basedsearchforsysteminvariantsaredeveloped.Itisshownthattheauto-maticsearchforsysteminvariantsthatestablishthedesiredpropertiesofcomputercode,canbeformulatedasaconvexoptimizationproblem,suchaslinearprogramming,semidefiniteprogramming,and/orsumofsquaresprogramming.
1Introduction
Failureofreal-timecontrolsystems,suchasthoseusedinspacecrafts,satellites,multiplecoordinatingUVAs,automobilesandtherapymachinesmayleadtolossofhumanlifeorahugelossincapitalandproducts.However,safeoperationofthesesafety-criticalcontrolsystemsreliesheavilyontheembeddedsoftware.AccordingtoBoingCo.andHoneywellInc.,softwaredevelopmentaccountsfor60−80%oftheeffortspentonthedevelopmentofcomplexcontrolsystems,whilemuchofthiseffortisexpendedonvalidationandverificationofthesoftwareafterorduringitsdevelopment.
Whilereal-timesoftwaremustsatisfyvariousresourceallocation,timing,computationandperformanceconstraints,theveryleasttorequireisthatthesoftwaremustexecutesafely,freeofrun-timeerrors.Thecriticalsoftwareprop-ertiesthatmustbeverified/validatedforsafeexecutioninclude:(1)absenceofvariableoverflow,(2)absenceof‘arrayindexout-of-bounds’calls,and(3)termi-nationofthefunctionsandsub-functionsandifrequired,theprogramitselfinfinitetime.Someadditionalpropertiesthatmightbedesiredinareliable,safety-criticalsoftwareinclude:(4)robustnesstouncertaininputs,includingfeedbackfromanalogsystems,(5)validityofcertaininequalitiesrelatinginputsandout-puts,forinstance,passivityand(6)absenceof‘dead-code’.Softwareanalysis,isthetaskofverificationofsomeoralloftheaboveproperties.
PatrickCousot[5],[7],publishedoneofthemostnoteworthyresultsinthelit-eraturethatdealwithsoftwareanalysis.Themainmethodofverificationisbasedonthenotionofabstractinterpretationofcomputerprograms.Seealso[8],[17].Accordingto[5,6],abstractinterpretationisdefinedasanapproximateprogramsemanticsderivedfromthedomainofconcretesemanticoperationsbyreplacingitwithadomainofabstractsemanticoperations.Adrawbackassociatedwiththesemethodsistheintroductionofanarrowingorwideningoperator,whichoftencausesthemethodtogenerateweakinvariants,resultinginconsiderableconservatisminanalysis[4].Nevertheless,thesemethodsappeartobepracti-calfortheverificationoflimitedpropertiesofreal-time,safety-criticalsystemssuchaslarge-sizedavionicssystems.Alternativemethodsaimingatgeneratingstrongerstatementsabouttheevolutionofvariablesinsoftwaresystemsmightbefound,forexample,inthemodel-checkingliterature;however,thetrade-offoftenachievedbythesemethodsisthatofincreasedaccuracyandthegenerationofstrongerpropertiesofsoftware(orsoftwaremodel)variables,oftenatthecostofincreasedcomputationalrequirementsandlimitedscalabilitytolargesystems.Moreover,constructionoftheprogrammodelsoftencannotbefullyautomated.Recently,therehavebeenrenewedeffortsatestablishingpropertiesofsoftwaresystemsbythecombineduseofabstractionsor,better,bisimulationmechanisms,andapplyingcontroltheoreticprinciplestothem.Muchoftherelevantliteratureinthatregardmaybefoundintherecentfieldofhybridsystems[13].Seeforinstance[9].Ingeneral,itwasfoundthatmanymethodsdevelopedinsystemandcontroltheoryforsystemsdrivenbydifferentialequationswereinprincipleapplicabletohybridsystems,possiblyatthepriceofhavingtore-developsomeelementsoftheory,e.g.optimalcontroltheoryonhybridsystems[16,12,3]orcontrolofhybridsystemsusingbisimulations[15,14].
Inthispaperweintroduceasystemstheoreticapproachforsoftwareanalysis.Wepresentmodelingtechniquesthroughtheintroductionoflinear-likemodelsthatmayrepresentabroadrangeofcomputerprogramsofinteresttothispaper.Theseincludesingleflowprogramsandgainscheduledpiecewiselinearsystems,usedtocontrolphysicaldevicessuchasaerospacesystemsorautomotivecontrolsystems.Themainmethodofverificationisanoptimization-basedsearchforsysteminvariants.Wetherefore,suggestspecificLyapunov-likefunctions,whosepropertiesguaranteevariablebounded-nessaswellasotherdesiredproperties,suchasguaranteedprogramtermination.Wealsoshowhowthesearchforthesesysteminvariantsmaybeformulatedasaconvexoptimizationproblem,suchaslinearprogramming,semi-definiteprogrammingand/orasumsofsquaresprob-lem.Attheend,wesketchtheblock-wiseanalysisprocedureforimprovingthescalabilityoftheproposedmethodsasanalysisoflarge-sizecomputerprogramsisundertaken.
2AutomatedSoftwareAnalysis:Preliminaries
Inthissectionweintroducethefundamentalsofsoftwareanalysisthroughdy-namicalsystemmodels.Weconsidercomputerprogramsasdynamicalsystems
andintroducecertainLyapunov-likefunctionsascertificatesforthebehaviorofthesesystems.2.1
Computerprogramsasdynamicalsystems
Weviewacomputerprogramasadynamicalsystemwhichdefinestherulesforiterativemodificationofoperatingmemory,possiblyinresponsetoreal-timeinputs.Inparticular,weconsidermodelsdefinedingeneralbyastatespacesetXwithselectedsubsetsX0⊂XofinitialstatesandX∞⊂Xofterminalstates,andbyaset-valuedfunctionf:X→2X,suchthatf(x)⊂X∞,∀x∈X∞.ThedynamicalsystemS=S(X,f,X0,X∞)definedbyX,f,X0,X∞isunderstoodasthesetofallsequencesX=(x(0),x(1),...,x(t),...)ofelementsfromXsatisfying
x(0)∈X0,x(t+1)∈f(x(t))∀t∈Z+
(1)
s.t.f(x)⊂X∞,∀x∈X∞Theuncertaintyinthedefinitionofx(0)representstheprograms’sdependenceonparameters,andtheuncertaintyinthedefinitionofx(t+1)representsprogram’sabilitytorespondtoreal-timeinputs.Fromthisviewpoint,analysisofsoftwaremeansverificationofcertainpropertiesofsystem(1).InSection4,weelaborateonthedynamicalsystemsviewofcomputerprogramsandsuggestspecificmodelsthatareessentiallyequivalentto(1),yetaremoresuitableforanalysispurposes.Definition1.AcomputerprogramrepresentedbyadynamicalsystemS=S(X,f,X0,X∞)issaidtoterminateinfinitetimeifeverysolutionX=x(t)of(1)satisfiesx(t)∈X∞forsomet∈Z+.Inaddition,wesaythatthestatevariablesremainbounded(donotoverflow)if∀t∈Z+,x(t)doesnotbelongtoacertain(unsafe)subsetX−ofXforeverysolutionX=x(t)of(1).2.2
Lyapunovfunctionsasbehaviorcertificates
Definition2.ALyapunovfunctionforsystem(1)isdefinedtobeafunctionV:X→Rsuchthat
/X∞.V(x)<θV(x)∀x∈X,x∈f(x):x∈
whereθ∈R+isapositiveconstant.
Remark1.Theparameterθintheabovedefinition,isveryimportantinpro-vidingtheflexibilityrequiredfordesigningappropriateLyapunovfunctionsthat
establishfinite-timeterminationand/orbounded-ness.ForinstanceifV(x0)<0andθ≥1,(2)impliesthatVmuststrictlymonotonicallydecreasealongthetrajectoriesof(1)untiltheyreachaterminalstate.Aswewillseeinthesequel,thisissuitableforestablishingfinite-timetermination.However,withV(x0)<0andθ<1,Visnotrequiredtodecreasealongthetrajectoriesof(1),whileitremainsnegative.Thisisveryimportantinprovingabsenceofoverflowincom-puterprogramswithoutthefinite-timeterminationproperty.
(2)
TerminationinfinitetimeThefollowingTheoremprovidesausefulcriterionforverifyingfinite-timeterminationinsoftwareanalysis.
Theorem1.IfthereexistsaboundedfunctionV:X→R−,andaconstantθ>1satisfying
V(x)<θV(x)∀x∈X,x∈f(x):x∈/X∞.
thenaterminalstateX∞willbereachedinafinitenumberofsteps.
Proof.SinceVisbounded,thereexistsM∈R+,suchthat−M≤V(x)<0,
∀x∈X.Now,assumethatthereexistsasequenceX=(x(0),x(1),...,x(t),...)ofelementsfromXsatisfying(1)thatdoesnotreachaterminalstateinfinitetime.I.e.x(t)∈/X∞,∀t∈Z+.Then,V(x(t))<−Mfor
t>
logM−log|V(x(0))|
,
logθ(4)(3)
whichcontradictsbounded-nessofV.
AbsenceofoverflowWealreadysawthatabsenceofoverflowcanbechar-acterizedbyavoidanceofanunsafesubsetX−ofthestatespaceX.ConsideraLyapunovfunctionV,definedaccordingto(2).DefinethelevelsetsLr(V)ofV,by
Lr(V)={x∈X:V(x) Theorem2.Considerthesystem(1)andletVdenotethespaceofallLyapunovfunctionsforthissystemsatisfying(2)withsomeθ≥1.AnunsafesubsetX−ofthestatespaceXcanneverbereachedalongallthetrajectoriesof(1)ifthereexistsV∈Vsatisfying infV(x)≥supV(x)(5) x∈X− x∈X0 Inaddition,if x∈X− infV(x)≥0(6) then,θ>0issufficient. Proof.Theproofproceedsbycontradiction.Firstconsidertheθ≥1caseand assumethat(1)hasasolutionX=(x(0),x(1),...,x(t−),...),wherex(0)∈X0andx(t−)∈X−.SinceV(x)isstrictlymonotonicallydecreasingalonganysolutionof(1),wemusthave: x∈X− infV(x)≤V(x(t−)) (7) whichcontradicts(5).Now,considerthecaseθ<1forwhichmonotonicityofVisnotalwaysimplied.PartitionX0intosubsetsX0andX0suchthatX0=X0∪X0and V(x)≤0V(x)>0 ∀x∈X0∀x∈X0 NotethateitherofX0andX0mayhappentobeempty.Now,assumethat(1)hasasolutionX=(x(0),x(1),...,x(t−),...),wherex(0)∈X0andx(t−)∈X−.Notethatbyassumption,V(x(t−))≥0andthus V(x(t))>0 ∀t Now,weturnourattentiontodevelopmentofgeneralformsforsystemin-variantsthatestablishthedesiredpropertiesandareappropriateforuseinaconvexoptimizationframework.Amongseveralpropertiesofareliablesoftwarementionedearlier,absenceofoverflowandfinite-timeterminationareexpectedinmostapplications. Theorem3.ConsiderthedynamicalsystemS=S(X,f,X0,X∞)definedby(1)andassumethatthereexistsareal-valuedfunctionV:X→Rsuchthat V(x)<0∀x∈X0. V(x)<θV(x)∀x∈X,x∈f(x):x∈/X∞. °x°2°° V(x)>°°−1∀x∈X. M(8)(9)(10) whereθ∈R+isaconstant,andnoconstraintonfinitenessofthestatespaceXisimposed.Then,everysolutionX=x(t)of(1)remainsboundedinthesaferegiondefinedby|xi| Proof.Notethat(8)and(9)implynon-positivityofV(x)onX\\X∞.Moreover,by(10),V(x)isboundedfrombelowby−1.Therefore,V(x)∈(−1,0).ByTheorem1,(9)impliesfinite-timetermination.Also,theunsaferegionX−isdefinedby|xi|≥M.Therefore, °x°2°° °°≥1,∀x∈X−,M x∈X− infV(x)=0≥0=supV(x) x∈X0 Theorem2thencompletestheproof. Remark2.ByimposingaquadraticformonV,thesearchforaLyapunov-likefunctionsatisfying(8)−(10)reducestosemidefiniteprogramming[1].Asanalternative,imposingalinearorpiecewiselinearformonV,alongwithreplacingcondition(10)with2nconstraints xi −1∀x∈X,i=1..nMxi V(x)>−−1∀x∈X,i=1..n MV(x)> convertstheproblemoffindinganappropriatesysteminvarianttolinearormixedinteger/linearprogramming[2].AnotherpossibilityistoletVbeapoly-nomialfunctionofthestatevariablesxi.Inthiscase,thesearchforsysteminvariantsrestrictedtotheclassofpolynomialswithrealcoefficientscanbeformulatedasasumsofsquaresproblem[18],[19]. 3ModelsofComputerPrograms Inthissectionwedevelopspecificmodelsofsoftwarethatareconvenientforanalysispurposes.Practicalconsiderationssuchasconvenienceforautomatedparsing/compiling,availabilityofanefficientrelaxationtechniqueandcompat-ibilitywithaparticularnumericalengineforconvexoptimizationinfluencethechoiceofmodelinglanguage.3.1 Mixedinteger/linearsystems WiththefollowingProposition,wefirstprovidethemotivation/intuitionbehindusingthismodelforsoftwaresystems. Proposition1.Universalityofmixed-integerlinearmodels.Letfbeanyarbitrarypiece-wiseaffinefunctiondefinedonacompactstatespaceX,whichconsistsoffiniteunionsoffinitepolytopes.Then,fcanbedefinedprecisely,byimposinglinearequalityconstraintsonafinitenumberofbinaryvariablesandafinitenumberofanalogvariablesrangingoverboundedintervals.I.e. ThereexistsmatricesFandH,suchthat qr f(x)={F[x;w;v;1]:s.t.∃w∈[−1,1],∃v∈{−1,1}s.t.H[x;w;v;1]=0}Proof.Theproofisbyconstruction.First,noticethatwithoutlossofgenerality i=NSn Xk,whereeachXiiswemayassumethatx∈[−1,1].Now,letX=definedbyafinitesetoflinearinequalityconstraints.I.e. ©ª x≤b,k=1,...,NXi:=x|aTkiiki i=1 (11) x∈Xi,wheretheconstant2Notethatbydefinitionf(x)=2Aix+2Bi appearsforconvenienceinnotationonly.Now,assignabinaryvariablevi∈ {−1,1},toeachXi,i=1...N−1,accordingtothefollowingrule, vi=1⇐⇒x∈Xi,vi=−1⇐⇒x∈/Xi,i=1,...N−1 i=N−1Xi=1 (12) vi=−N+1⇐⇒x∈XN, Thenwehavef(x)= N−1Xi=1 i=N−1Xi=1 vi=−N+3⇐⇒x∈/XN (1+vi)(Aix+Bi)−(N−3)(ANx+BN)− subjectto N−1Xi=1 vi(ANx+BN), Now,weneedtorelate(11)and(12),whichisdoneinthefollowingway; ¡¢ x∈Xi⇐⇒aTx−b(14)ki(vi+1)≤0,k=1,...,NikiSincebyassumption,eachXiisbounded, x∈Xi i=N−1Xi=1 vi≤−N+3,and(12),andvi∈{−1,1},i=1...N(13) Rki:=minaTkix−bki existsandisfinite.Therefore,theconditionx∈Xi,isequivalentto, T aTkixvi+akix−bkivi−bki−Rki(wki+1)=0,wki∈[−1,1],k=1,...,Ni(15) Next,defineauxiliarystatevectorsyi:=xvi∈Rn.Noticethatyiisthemul-tiplicationofananalogvariablex,andabinaryvariablevi.Werepresentthis(nonlinear)transformationbyanaffinetransformationinvolvingauxiliaryanalogvariableszi∈[−1,1]n,andzi∈[−1,1]n,subjecttoasetoflinearconstraints,inthefollowingway, yi=4zi−x−vi1n−1n,zi≤zi≥0,zi≤−vi1n,zi= equivalently, yi=4zi−x−vi1n−1n,i=1,..,N¢1¡1(vi+1) zi+Wi+In1n=1n 22 ¢1¡2 zi=Wi+In1n 2¢¡1 zi+Wi3+In1n=−vi1n 21 zi=(x−zi) 2(16a)(16b)(16c)(16d)(16e) (vi+1) 1n21 (x−zi)2£¤T zwv1,where¤Now,£letXe=xy1...ynz1...znz1...n¤£113 ...wNn...wNnw=w11...wNNNw11,andv=v1...vn.Then, #\"N−1 X£¤ Ai−(N−3)ANx+A1−AN...AN−1−ANyf(x):= i=1 whereWikisdefinedby©kªk Wik=diagwji,j=1,..,n,i=1,..,N,k=1,..,3,wij∈[−1,1] (17) +B1−BN...BN−1−BNv+ whichislinearinx,y,v.Moreover,(17)issubjecttoconstraints(13),(15),(16),whicharealllinearequalityconstraintsinXe.Thiscompletestheproof.Sofar,wehaveshownthatimposinglinearequalityconstraintsonBooleanvariablesandonanalogvariablesrangingoverboundedintervalsallowsonetodefinearbitrarypiecewiselinearfunctionsonfiniteunionsofpolytopes.Thisobservationservesasthebasisforintroducingthewidelyusedclassofmodelswhichwillbereferredtoasmixedinteger/linearsystemshere.Thesemodelsarecapableofprovidingrelativelybriefdescriptionsofcomplicateddependencies.Amixedinteger/linearsystemmodelhasstatespaceX⊂Rn.Itsstatetransitionfunctionf:X→2XisdefinedbytwomatricesF,Hofdimensionsn-by-(n+q+r+1)andp-by-(n+q+r+1),accordingto f(x)={F[x;w;v;1]: qr ∃w∈[−1,1],∃v∈{−1,1}s.t.H[x;w;v;1]=0} NaturalLyapunovfunctioncandidatesformixedinteger/linearsystemsarequadraticfunctionals.Withinthisclass,checkingmonotonicityofLyapunovfunctionsalongsystemtrajectoriescanbedonebyapplicationofthetradi-tionalquadraticrelaxationtechniques,startingwiththoseusedinderivingtheboundsfortheMAX-CUTproblem,whichleadstosemidefiniteprogrammingastheLyapunovfunctiondesigntool. SearchforLyapunovinvariantsusinglinearorsemidefiniteprogram-mingThissectiondetailsourapproachtocomputeLyapunovinvariantsformixedinteger/linearsoftwaremodels.LookingforafunctionVsatisfying(8)−(10),maybeseenaninfinite-dimensionalconvexprogrammingproblemintheunknownV.Thismaybesolvedbyfirstdefininganappropriate,finite-dimensionalparameterizationofVandthensolvingtheresultingfinite-dimensional,convexoptimizationproblem. LinearparameterizationofquadraticLyapunovfunctionsappearas ∙¸T∙¸xx V(x):=P 11 £¤ N−1Xi=1 Bi+(−N+3)BN wherePisaconstant,symmetricmatrix. FortheLyapunovinvariantparameterizationconsideredabove,theproblemoffindinganinvariantthatsatisfiestheconditions(8)−(10)isaboutsolvingasetofnonlinearconstraintsarisingfromtheseconditions.Theseconditionsareoftennon-convexconditions,whichmakestheirexactsolutionoftenimpractical,but,fortunatelyalsounnecessary.Instead,wewillfocusonusingrelaxedversionsoftheseconditions,whicharemucheasiertosolveusingeitherlinearorsemidefiniteoptimizationroutines.ThemaintoolusedtowardsobtainingtheserelaxationsisaLagrangianrelaxationprocedurealsoknownasS-procedure. Forexample,thefirstofthethreeconditionsdoesnotrequiresuchaproce-dure,sinceitisalinearconstraintonthecoefficientsofP:Indeed,therequire-mentV(x(0))<0mayalsobewrittenas, ∙x(0)¸T M1 P ∙x(0)¸ M1 <0.(18) whereMistheoverflowlimit.Thesecondcondition,(9),maybewrittenas ∙F.[x(k)v(k)w(k)1]¸T M1 P ∙F.[x(k)v(k)w(k)1]¸ M1 <θ ∙x(k)¸ M1 P ∙x(k)¸ M1 (19) Theconstraintv∈{−1,1}isequivalenttothequadraticconstraint vM1v− T rXi=1 foranyx(k),v(k),w(k)satisfying £¤TqrH.x(k)w(k)v(k)1=0andw(k)∈[−1,1],v(k)∈{−1,1} r (20) forarbitraryµi,1∈R,i=1,...r.Likewise,theconstraintw∈[1,1]isequiva-lentto wTE1w− qXi=1 ©ªµi,1=0,withM1=diagµ1,1,µ2,1,...µr,1 q forarbitraryηi,1>0,i=1,...q.FormulatingtheproperLagrangianrelaxation,condition(19)holdswhenevercondition(20)holdsifthereexistsP,M1,E1≥0andy1∈Rsx×nHsuchthat TTTTTT LT1PL1−θL2PL2 where ih fwfvf1 HM:=[Mhxhwhvh1],FM:=fxMMM∙∙¸¸ FMIn0n×(sx−n) L1:=,L2:= 01×(sx−1)101×(sx−1)1 L3:=[In+q0(n+q)×(r+1)],L4:=[0(r+1)×(n+q)Ir+1],L5:=[01×(sx−1)1] ©ª ηi,1≤0,withE1=diagη1,1,η2,1,...ηq,1 Likewise,(10)maybewrittenas ∙x(k)¸T∙ M1 In00−1 ¸∙x(k)¸ M1 < ∙x(k)¸T M1 P ∙x(k)¸ M1 (22) foranyx(k),v(k),w(k)satisfying £¤T H.x(k)w(k)v(k)1=0andw(k)∈[−1,1]q,v(k)∈{−1,1}r (23) Thuscondition(22)holdswhenevercondition(23)holdsifthereexistsP,M2,E2≥0andy2∈Rsx×nHsuchthat TTTTTT LT2P0L2−L2PL2 Thus,absenceofoverflowandfiniteexecutiontimeareguaranteedifthereexistP,M1,M2,E1≥0,E2≥0,y1,andy2satisfyingconstraints(18,21and24). 3.2Linearsystemswithconditionalswitching Inthismodelthestatespaceofthesystemisthedirectproduct X={0,1,2,...,m}×Rn ={(k,v):k∈Z,0≤k≤m,v∈Rn} ofadiscretesetandann-dimensionalEuclideanspace,X0={(0,v0)},X∞={m}×Rn.Theset-valuedstatetransitionmapf:X→2XisdefinedbymatricesAk,Bk,Lk,Gk,Hk,Ik,Ck,Dk,wherek∈{0,1,...,m−1},aswellasbyafunctionp:{0,1,...,m−1}→{0,1,...,m},accordingtothefollowingrule: f(k,v)={(k+1,Akv+Bkw+Lk):w∈[−1,1]}whenCkv+Dk≤0andk whenCkv+Dk>0andk NaturalLyapunovfunctioncandidatesforlinearsystemswithconditionalswitchinghavethepiecewisequadraticorpiecewiselinearformV(k,v)=σk(v),whereforeveryk∈{0,1,...,m}thefunctionσk:Rn→Risaquadraticoranaffinefunctional. 3.3Trigonometricpolynomialmodels Themodelsdescribedintheprevioussectionsareonlycapableofdescribingpiecewiselineartransformationsofanalogvariables.Thisisnotalwaysconve-nient:forexample,multiplicationoftwoanalogstatevariablescanberepresentedthiswayonlyapproximatelyandthisrepresentationisparticularlycumbersome.Inordertocoveralargerclassofanalogoperations,thetrigonometricpolynomialmodelscouldbeuseful. AtrigonometricpolynomialmodelhasstatespaceXwhichisaclosedsub-groupofapoly-thorusTn,whereTdenotestheunitcircleinthecomplexplane.Equivalently,onecanthinkofXasadirectproductofsetsoftheformTkor q Zkq,whereZqdenotesthesetofallcomplexnumberszsuchthatz=1.Theword“trigonometric”referstothenaturalparameterizations T={cos(t)+jsin(t):t∈R} oftheunitcircle.Thestatetransitionmapf:X→2Xisdefinedbyavectorpolynomialpwithrespectto2∗n+kcomplexvariables,accordingto f(x)={y∈X:p(y,x,z)=0forsomez∈Tk}. NaturalLyapunovfunctioncandidatesfortrigonometricpolynomialmodelsarereal-valuedtrigonometricpolynomials.CheckingvalidityofaLyapunovfunc-tioncandidatereducestoverificationofpositivityofatrigonometricpolynomialsubjecttoasetofpolynomialconstraints,whichcanbedoneusingtheShor’s“sumsofsquares”argument:Apolynomialispositiveifitcanberepresentedasasumofsquaresofpolynomials.Whileitisnottruethatapositivepolynomialcanalwaysberepresentedasasumofsquaresofpolynomials,itcanbeshownthattheequivalenceholdsinthecaseoftrigonometricpolynomials. 4ANumericalExample Considerthefollowingprogram: x1=0;x2=0;whilex2≤100,ifx1≥0, x1=x1−a;else x1=x1+b;end x2=x2+1;end wherea∈[100,900]andb∈[200,800],areuncertaininputparameters.Using2slackvariablesand1binaryvariable,amixedinteger/linearmodelofthispieceofcodeisdefinedbymatricesF,andH,givenas: ∙¸0 x(0)=,n=2,q=2,r=1. 0 ¸¸∙∙MMbb−a 0−010−1000−a+2222,R=,H=F= 010R0R−100010001 M+100 ,2GivenM=1000astheoverflowlimit,using(18),(21),(24),thequadratic Lyapunovfunction V(x)= 121177720123x1−x1−x2−x2−2000500010001000010000wasfoundtoprovebounded-nessandfinite-timeterminationforallaandb. 5Block-wiseAnalysisofComputerPrograms Block-wiseanalysisisamethodforimprovingthescalability/computationalcost oftheabovetechniquesasanalysisoflargesizecomputerprogramsisunder-taken.Thebasicideahereistoconsiderlarge-sizesoftwareastheinterconnectionofsmallersizedynamicalsystems(functions,subfunctionsandproceduresthatwecallthem\"blocks\").Thesesocalledblocksinteractviaasubsetofthepro-gramstatescalled\"globalvariables\".Correctnessofeachblockisestablishedseparately,knownapriori,orassumedtemporarily.Thedynamicsofeachblockisthenabstracted/approximatedbyequalitiesand/orinequalitiesrelatingthein-putsandtheoutputs.Inobviouscases,abstractionsofthislevelmaybeprovidedbytheprogrammertofacilitatetheanalysistask.Thisway,thestates/variablesthatarelocaltoeachblockareeliminatedfromtheglobalmodel.Correctnessofthesoftwarewillbeestablishedbyverifyingbounded-nessofglobalvariables,aswellasverifyingthatwhenrequired,afinalglobalstatewillbereachedinfinite-time.Incasecorrectnessofsomeoftheblockswereassumedtemporarily,theircorrectnessneedtobeestablishedrigorously,subjecttotheboundsavail-ablenow,forglobalvariables.Tofurtherclarifytheconcept,weimplementthemethodonthefollowingexample. typedefenum{FALSE=0,TRUE=1}BOOLEAN;BOOLEANINIT1,INIT2;floatP,X; voidfilter1(){ staticfloatE[2],S[2];if(INIT1){ S[0]=X;P=X;E[0]=X;E[1]=0;S[1]=0;}else{ P=0.5*X—0.7*E[0]+0.4*E[1]+1.5*S[0]—S[1]*0.7;E[1]=E[0];E[0]=X;S[1]=S[0];S[0]=P; X=P/6+S[1]/5;}}voidfilter2(){ staticfloatE2[2],S2[2];if(INIT2){ S2[0]=0.5*X;P=X;E2[0]=0.8*X;E2[1]=0;S2[1]=0;}else{ P=0.3*X—E2[0]*0.2+E2[1]*1.4+S2[0]*0.5—S2[1]*1.7;E2[1]=0.5*E2[0];E2[0]=2*X; S2[1]=S2[0]+10;S2[0]=P/2+S2[1]/3;X=P/8+S2[1]/10;}}voidmain(){ X=0;INIT1=TRUE;INIT2=TRUE;while(1){ X=0.98*X+85;if(abs(X)<=400){ filter1();X=X+100; INIT1=FALSE; }elseif(abs(X)<=800){ filter2();X=X—50; INIT2=FALSE;}}} Duetothepresenceofstaticvariableseands,bounded-nessoftheaboverecur-sionforaninfiniteiterationmustbeverified.UsingLMIs(18)−(24)°°£numberof¤ withθ=0.9,°Pe1e0s1s0°≤2038wasproved. °£°£¤°¤°°Pe1e0s1s0°≤2038→°Ps1°≤2038sµ¶µ¶22 11 +'531|x|≤2038 65 Forautomated(block-wise)analysisofthisprogram,theanalyzermustbe provided(eitherbyacomplierorbytheprogrammer)withthesysteminvariantthatpriortoeachexecutionoffilter1(),|x|≤400.Next,filter()ismodeledinthefollowingabstractedway: wx∈[−1,1],s0(0)∈[−400,400],e0(0)∈[−400,400],P(0)∈[−400,400],s1(0)=0,e1(0)=0. ⎡⎤P(k)⎤⎡⎤⎡ ⎥P(k+1)00.4−0.7−0.71.50.5×4000⎢⎢e1(k)⎥ ⎢⎢e1(k+1)⎥⎢001⎥0000⎥⎥⎢e0(k)⎥⎢⎥⎢ ⎢⎢e0(k+1)⎥=⎢000⎥001×4000⎥⎥⎢s1(k)⎥⎢⎥⎢ ⎥⎣s1(k+1)⎦⎣0000100⎦⎢⎢s0(k)⎥ 00.4−0.7−0.71.50.5×4000⎣wx(k)⎦s0(k+1) 1 Thisprovesthatintheworstcase,thevalueofX,afterexecutionoffilter1()cannotbegreaterthan531.Similarly,priortoeachexecutionoffilter2(),|x|≤800isinvariant.Next,filter2()ismodeledinthefollowingabstractedway:wx∈[−1,1],s20(0)∈[−400,400],e20(0)∈[−0,0],P(0)∈[−800,800],s21(0)=0,e21(0)=0.⎤P(k)⎤⎡⎤⎡ ⎥01.4−0.2−1.70.50.3×8000⎢P(k+1)⎢e21(k)⎥ ⎢⎥⎢e21(k+1)⎥⎢000.50000⎥⎥⎢⎥⎢e20(k)⎥⎢ ⎢⎥⎢e20(k+1)⎥=⎢000002×8000⎥⎥⎢⎥⎢s21(k)⎥⎢ ⎣s21(k+1)⎦⎣00001010⎦⎢s20(k)⎥⎢⎥.4−0.2−1.710.50.3×80010⎣wx(k)⎦s20(k+1)012+2232231 °£¤° Again,usingLMIs(18)−(24)withθ=0.9,°Pe1e0s1s0°≤9935wasproved. °£°£¤°¤°°Pe1e0s1s0°≤9935→°Ps1°≤9935sµ¶µ¶22 11 +'1591|x|≤9935 810Thisinturn,provesthatintheworstcase,thevalueofX,afterexecution offilter2()cannotbegreaterthan1591.Themainprogramisnowabstractedinthefollowingway. ⎡ voidmain(){ X=0;while(1){ X=0.98*X+85;if(abs(X)<=400){ X=531*w1;%w1∈[−1,1]X=X+100; }elseif(abs(X)<=800){ X=1591*w2;%w2∈[−1,1]X=X—50;}}} Usingthesamemethods,analysisofthisprograminturnprovesthat|x|≤4560.Therefore,bounded-nessofallvariablesisestablished. 6Conclusions Anewframeworkforanalysisofreal-timesoftwarewasintroduced.Itwasshownthatsoftwarecanbeviewed/modeledasadynamicalsystem.Specificmodelscarryingthistaskwerealsointroduced.Systeminvariants,foundbyconvexoptimizationofcertainLyapunov-likefunctionsprovethedesiredpropertiesofthesoftware.Thesepropertiesincludebounded-nessofallvariableswithinsaferegionsandfinitetimeterminationoftheprogram.Toimprovescalabilityofthesetechniquesforapplicationtolarge-sizecomputerprograms,themethodofblock-wiseanalysisofcomputercodewassuggested.Itwasshownthroughanumericalexample,howthismethodcanbeapplied. References 1.S.Boyd,L.E.Ghaoui,E.Feron,andV.Balakrishnan.LinearMatrixInequalitiesinSystemsandControlTheory.SocietyforIndustrialandAppliedMathematics,1994. 2.D.Bertsimas,andJ.Tsitsikilis.IntroductiontoLinearOptimization.AthenaSci-entific,1997. 3.M.S.Branicky,V.S.Borkar,andS.K.Mitter.Aunifiedframeworkforhybridcon-trol:modelandoptimalcontroltheory.IEEETransactionsonAutomaticControl,43(1):31-45,1998. 4.M.A.Colon,S.Sankaranarayanan,H.B.Sipma.Linearinvariantgenerationusingnon-linearconstraintsolving.InComputerAidedVerification(CAV2003),vol.2725ofLectureNotesinComputerScience,SpringerVerlag,pp.420-433. 5.P.CousotandR.Cousot.Abstractinterpretation:aunifiedlatticemodelforstaticanalysisofprogramsbyconstructionorapproximationoffixpoints.InProc.4thACMSIGPLAN-SIGACTSymposiumonPrinciplesofProgrammingLanguages,POPL’77,pages238—252,1977. 6.P.Cousot,andR.Cousot.Systematicdesignofprogramanalysisframeworks.InConferenceRecordoftheSixthAnnualACMSIGPLAN-SIGACTSymposiumonPrinciplesofProgrammingLanguages,pages269—282,SanAntonio,Texas,1979.ACMPress,NewYork. 7.P.Cousot.Semanticfoundationsofprogramanalysis.InS.MuchnickandN.Jones,editors,ProgramFlowAnalysis:TheoryandApplications,chapter10,pages303—342.Prentice-Hall,1981. 8.D.Dams.AbstractinterpretationandpartitionrefinementforModelChecking.Ph.D.Thesis,EindhovenUniversityofTechnology,1996. 9.S.Prajna,andA.Jadbabaie.Safetyverificationofhybridsystemsusingbarriercertificates.HybridSystems:ComputationandControl.Springer-Verlaglecturenotesincomputerscience,March2004. 10.M.Johansson,andA.Rantzer.OnthecomputationofpiecewisequadraticLya-punovfunctions.InProc.36thIEEEConferenceonDecisionandControl,SanDiego,California,December1997. 11.M.Johansson,andA.Rantzer.ComputationofpiecewisequadraticLyapunov functionsforhybridsystems.IEEETransactionsonAutomaticControl,43(4),pp.555-559,April1998. 12.S.HedlundandA.Rantzer.Optimalcontrolofhybridsystems.InProc.38thIEEE ConferenceonDecisionandControl,Phoenix,Arizona,December1999. 13.R.Alur,andG.J.Pappas(Eds.):HybridSystems:ComputationandControl, 7thInternationalWorkshop,LectureNotesinComputerScience,volume2993,SpringerVerlag,March2004. 14.G.Lafferriere,G.J.Pappas,andS.Sastry.Hybridsystemswithfinitebisim-ulations.HybridSystemsV,LectureNotesinComputerScience,volume1567,Springer1999. 15.G.Lafferriere,G.J.Pappas,andS.Sastry.Reachabilityanalysisofhybridsystems usingbisimulations.InProc.ofthe37thIEEEConferenceonDecisionandControl,pages1623-1628,Tampa,1998. 16.J.Lygeros,C.Tomlin,andS.Sastry.Controllersforreachabilityspecificationsfor hybridsystems.Automatica,35(3):349-370,1999. 17.D.Monniaux.AbstractinterpretationofprogramsasMarkovdecisionprocesses. InStaticAnalysisSymposium,volume2694inLectureNotesinComputerScience,pages237-254,SpringerVerlag,2003. 18.P.A.Parrilo.MinimizingPolynomialFunctions.InAlgorithmicandQuantitative RealAlgebraicGeometry,DIMACSSeriesinDiscreteMathematicsandTheoreti-calComputerScience,Vol.60,pp.83—99,AMS. 19.K.Gatermann,andP.A.Parrilo.Symmetrygroups,semidefiniteprograms,and sumsofsquares.JournalofPureandAppl.Algebra,Vol.192,No.1-3,pp.95-128,2004.
因篇幅问题不能全部显示，请点此查看更多更全内容