Software-Reliability-Methods--PPT

1SoftrareReliabilityMethodsProf.DoronA.PeledBarIlanUniversity,IsraelAndUniveristyofwarwick,UKVersion20082Somerelatedbooks:Also:Mainly:~doron3Goal:softwarereliabilityUsesoftwareengineeringmethodologiestodevelopthecode.Useformalmethodsduringcodedevelopment4Whatareformalmethods?Techniquesforanalyzingsystems,basedonsomemathematics.Thisdoesnotmeanthattheusermustbeamathematician.Someoftheworkisdoneinaninformalway,duetocomplexity.5ExamplesforFMDeductiveverification:Usingsomelogicalformalism,proveformallythatthesoftwaresatisfiesitsspecification.Modelchecking:Usesomesoftwaretoautomaticallycheckthatthesoftwaresatisfiesitsspecification.Testing:Checkexecutionsofthesoftwareaccordingtosomecoveragescheme.6Typicalsituation:Boss:Mark,Iwantthatthenewinternetmarketingsoftwarewillbeflawless.OK?Mark:Hmmm.Well,...,Aham,Oh!Ah???WheredoIstart?Bob:Ihavejustthesolutionforyou.Itwouldsolveeverything.7SomeconcernsWhichtechnique?Whichtool?Whichexperts?Whatlimitations?Whatmethodology?Atwhichpoints?Howexpensive?Howmanypeople?Neededexpertise.Kindoftraining.Sizelimitations.Exhaustiveness.Reliability.Expressiveness.Support.8BadmouthFormalmethodscanonlybeusedbymathematicians.Theverificationprocessisitselfpronetoerrors,sowhybother?Usingformalmethodswillslowdowntheproject.9Someanswers...Formalmethodscanonlybeusedbymathematicians.Wrong.Theyarebasedonsomemathbuttheusershouldnotcare.Theverificationprocessisitselfpronetoerrors,sowhybother?Weopttoreducetheerrors,noteliminatethem.Usingformalmethodswillslowdowntheproject.Maybeitwillspeeditup,onceerrorsarefoundearlier.10SomeexaggerationsAutomaticverificationcanalwaysfinderrors.Deductiveverificationcanshowthatthesoftwareiscompletelysafe.Testingistheonlyindustrialpracticalmethod.11OurapproachLearnseveralmethods(deductiveverification,modelchecking,testingprocessalgebra).Learnadvantagesandlimitations,inordertochoosetherightmethodsandtools.Learnhowtocombineexistingmethods.12EmphasisTheprocess:Selectingthetools,Modeling,Verification,Locatingerrors.Useoftools:Handson.PVS,SPINVisualnotation:Statecharts,MSCs,UML.13SomeemphasisTheprocessofselectingandusingformalmethods.Theappropriatenotation.Inparticular,visualnotation.Hands-onexperiencewithtools.14TheunbearableeasinessofgradingDuringclass,choosesomesmallprojectingroups,e.g.,Exploresomeexamplesusingtools.Implementingasimplealgorithm.Dealingwithnewmaterial.orcoveringadvancedsubject.-Officepresentation(1hour).-Writtendescription(2-3pages+computeroutputor6-10pages).-Classpresentation(0.5-1.5hourspergroup).15ExampletopicsProject:Verifysomeexampleusingsometools.Communicationprotocols.Mutualexclusion.Advancedtopics:Abstractions.Reductions.Partitions.Staticanalysis.Verifyingpushdownautomata.Verifyingsecurityprotocols.16Wheredowestart?Boss:Mark,canyouverifythisforme?Mark:OK,firstIhaveto...17ThingstodoCheckthekindofsoftwaretoanalyze.Choosemethodsandtools.Expresssystemproperties.Modelthesoftware.Applymethods.Obtainverificationresults.Analyzeresults.Identifyerrors.Suggestcorrection.18DifferenttypesofsoftwareSequential.Concurrent.Distributed.Reactive.Protocols.Abstractalgorithms.Finitestate.19Specification:Informal,textual,visualThevalueofxwillbebetween1and5,untilsomepointwhereitwillbecome7.Inanycaseitwillneverbenegative.(1=x=5U(x=7/\[]x=0))1=x=5X=7X=020VerificationmethodsFinitestatemachines.Applymodelchecking.Applydeductiveverification(theoremproving).Programtoobig,toocomplicated.Applytestingtechniques.Applyacombinationoftheabove!21ModelingUsetheprogramtext.Translatetoaprogramminglanguageembeddedinsomeproofsystem.Translatetosomenotation(transitionsystem).Translatetofiniteautomata.Usevisualnotation.Specialcase:blackboxsystem.22ModelingSoftwareSystemsforAnalysis(Book:Chapter4)23ModellingandspecificationforverificationandvalidationHowtospecifywhatthesoftwareissupposedtodo?CanweusetheUMLmodelorpartsofit?Howtomodelitinawaythatallowsustocheckit?24SystemsofinterestSequentialsystems.Concurrentsystems(multi-threaded).1.Distributivesystems.2.Reactivesystems.3.Embeddedsystems(software+hardware).25Sequentialsystems.Performsomecomputationaltask.Havesomeinitialcondition,e.g.,0inA[i]integer.Havesomefinalassertion,e.g.,0in-1A[i]A[i+1].(Whatistheproblemwiththisspec?)Aresupposedtoterminate.26ConcurrentSystemsInvolveseveralcomputationagents.Terminationmayindicateanabnormalevent(interrupt,strike).Mayexploitdiversecomputationalpower.Mayinvolveremotecomponents.Mayinteractwithusers(Reactive).Mayinvolvehardwarecomponents(Embedded).27ProblemsinmodelingsystemsRepresentingconcurrency:-Allowonetransitionatatime,or-Allowcoincidingtransitions.Granularityoftransitions.Assignmentsandchecks?Applicationofmethods?Global(allthesystem)orlocal(onethreadatatime)states.28Modeling.Thestatesbasedmodel.V={v0,v1,v2,…}-asetofvariables,oversomedomain.p(v0,v1,…,vn)-aparametrizedassertion,e.g.,v0=v1+v2/\v3v4.Astateisanassignmentofvaluestotheprogramvariables.Forexample:s=v0=1,v1=3,v3=7,…,v18=2Forpredicate(firstorderassertion)p:p(s)ispunde