现代软件工程SoftwareVerification资料课件

Morden Software Engineering Shengbing RSchool of Software,Central South UniversitySoftware Verification21.Software QualitywAriane 5Exploded 37 seconds after takeoff-the reason was an overflow in a conversion of a 64 bit floating point number into a 16 bit integer.3More Software Bugshttp:/www5.in.tum.de/huckle/bugse.html42.Software VerificationwTesting(using the system itself)wSimulation(using a model of the system)wDeductive verification(mathematical(manual)proof of correctness,in practice done with computer aided proof assistants/proof checkers)wModel Checking(exhaustive testing of a model of the system)wPeer Reviewing:amounts to software inspection cataches 31%93%of the defects5Testing Is HardTesting parallel and distributed systems is not always cost effective.wTesting concurrency related problems is often done only when rest of the system is in place fixing bugs late can be very costly.wIt is labour intensive to write good tests.wIt is hard if not impossible to reproduce bugs due to concurrency encountered in testing.wTesting can only prove the existence of bugs,not their in-existence.6SimulationwThe main method for the validation of hardware designs.wConsider using simulation/prototyping for software.7Deductive VerificationwProving things correct by mathematical means.wComputer aided proof assistants,such as HOL4.wVery high cost,requires highly skilled personnel.wOnly for truly critical systems.8Model Checking9Model CheckingMModelCheckerp F qyesnoError Trace10wTuring Award 2007wE.M.Clarke,E.A.Emerson and J.Sifakis11Model Checking ProcesswModeling PhasewModel the systemwPerform some simulationwFormalize the propertywRuning PhasewRun the model checkerwTo check the validity of the property in the system modelwAnalysis PhasewProperty satisfied:check the next propertywProperty violated:wAnalyzed generated counterexample by simulationwRefine the model,design,or propertywRepeat the entire procedurewOut of memory:try to reduce the model and try again12The specification of system propertieswFunctional correctnesswDoes the system do what it is supposed to do?wReachabilitywIs it possible to end up in a deadlock state?wSafetywSomething bad never happenswLivenesswSomething good will eventually happenwFairnesswDoes,under certain conditions,an event occur repeatedly?wReal-time propertieswIs the system acting in time?13Benefits of Model CheckingwIn principle automated:Given a system model and a property,the model checking algorithm is fully automaticwCounterexamples are valuable for debuggingwAlready the process of modelling catches a large percentage of the bugs:rapid prototyping of concurrency related featureswIt supports partial verification.wIt can be easily integrated in existing development cycles.wIt has a sound and mathematical underpinning.14Model Checking Applied in the Earlier Phasesanalysisrequirementsspecificationdesigncodingtestingreleasemaintain15Drawbacks of Model CheckingwState explosion problem:Capacity limits of model checkers often exceededwManual modelling often needed:wModel checker used might not support all features of the implementation languagewAbstraction needed to overcome capacity problemswReverse engineering of existing already implemented systems to obtain models is time consuming and often futilewIt verifies a system model.wIt is mainly appropriate to control-intensive applications.16Verification and ValidationwVerification:wTo check that the design satisfies the requirements that have been identified.wTo check that we are buildings the things right.wValidation:wTo check whether the formal model is consistent with the informal conception of the design.wTo check that we are verifying the right thing.173.Model Checker:SPINwSPIN (Simple Promela Interpreter)wDeveloper:Gerard J.Holzmann wIt was the winner of the 2001 ACM Software System AwardwSome other Software System Award winners:w1983 UNIXw1986 TeXw1987 SMALLTALKw1991 TCP/IPw2002 JavawThe award citation:For SPIN,a highly successful and widely used software model-checking system based on formal methods from Computer Science.It has made advanced theoretical verification methods applicable to large and highly complex software systems.Gerard J.Holzmann NASA JPL Laboratory for Reliable Software18Model Checker:SPINwispin安装w1)安装ActiveTCL，运行ispin.tcl界面描述程序w2）安装cygwin,select packages选中Devel为Installw3）安装graphviz2.26.3,图形显示自动机w4）将PC-Spin625解压到某文件夹，例如：C:ispinw5）修改c:ispin中的ispin.tcl文件，将set DOT dot改为set DOT“c:/program files/graphviz2.26.3/bin/dot”,即dot执行文件所在的目录。w6）在windows环境变量path中增加ispin，cygwinbin及graphviz2.26.3bin目录路径。w7）运行ispin.tcl。19Spin,Promela,iSpinC compilerSPINAnalyzer(exec)VerificationoutputErrortrailModel(Promelasource)SimulationoutputSimulation:random,interactiveguidedAnalyzer(C source)Verification20Model Checker:SPINwIspin界面：创建或打开PML模型（*.pml文件）21Model Checker:SPINw模型验证如果有错误，则如果有错误，则生成生成*.trail文件。文件。22Model Checker:SPINw仿真或回放234.Model Checker:NuSMVwNuSMV(New Symbolic Model Verifier)wNuSMV是开源的wSPIN仅仅支持LTL属性检测wNuSMV支持LTL属性和CTL属性检测w是Carnegie Mellon University(CMU)和Italy的ITC-IRST的合作项目，是对CMU的SMV再工程的结果w增强用户与系统的交互能力w提供更多启发式策略w结构更加模块化w实现更加鲁棒化和模块化w点击NuSMV-zchaff-2.5.4-i386-pc-mingw32.rar即可安装。24NuSMV结结构构25SMV：HistoryCMUSMVCadenceSMVNuSMVlStrong abstraction functionslGUIlNew languagelOldest VersionlNo GUITwo versionsl2.x:Open Source,many new features,BDD and SAT based backendsl1.x:Original version,had a GUI26Model Checker:NuSMVw运行NuSMV:w在NuSMV输入reset,复位系统;w在NuSMV输入read-model i,加载一个模型w之后便可以进行仿真和模型检测w仿真步骤：w在NuSMV输入go,建立模型w在NuSMV输入pick-state r随机选择一个起始状态w在NuSMV输入simulate进行仿真w在NuSMV输入show-traces显示执行结果27w模型检测步骤：w在NuSMV输入go 建立系统模型w在NuSMV输入Check_ltlspec 检测LTL属性规范w在NuSMV输入show_property 显示属性的状态w【属性类型 属性状态 反例号 属性名】w如果有反例号，则可以用show_traces 反例号 显示检测情况w有界模型检测步骤：w在NuSMV输入go_bmcw在NuSMV输入check_ltlspec_bmc_onepb k -l w其中，x表示界限长度，y表示循环展开长度28NuSMV实实例例wMODULE mainwVARw y:0.15;wASSIGNw init(y):=0;wTRANSw casew y=7:next(y)=0;w TRUE:next(y)=(y+1)mod 16;w esacw-LTLSPEC!G F(y=2)wLTLSPEC F(X y=9);29NuSMV仿真仿真30NuSMV模型模型检测检测w属性不满足，存在反例！31NuSMV模型模型检测检测32Useful LinkswNuSMV home pagewhttp:/nusmv.fbk.eu/wNuSMV tutorialwhttp:/nusmv.fbk.eu/NuSMV/tutorial/v25/tutorial.pdfwNuSMV user manualwhttp:/nusmv.fbk.eu/NuSMV/userman/v25/nusmv.pdfwNuSMV FAQwhttp:/nusmv.fbk.eu/faq.htmlwNuSMV on Andreww/afs/andrew.cmu.edu/usr11/arieg/public/nusmv/2.5.3/wNuSMV examplesw/share/nusmv/exampleswKen McMillan,Symbolic Model Checking:An Approach to the State Explosion Problem,1993whttp:/ Logicw在一个模型中，公式的真与假是动态的。w时态逻辑：把包含时态动词的语句形式化，并把含有这种语句的推理系统化w例如：F A表示将来某个时间命题A为真w模态逻辑：涉及必然性和可能性。w必然算子 可能算子 w两种常用的时态逻辑：w线性时态逻辑LTL（Linear-time Temporal Logic）w计算树逻辑CTL(Computation Tree Logic)w在软件验证（模型检测）中，采用时态逻辑描述系统属性。34线线性性时态逻辑时态逻辑wLTL:Linear-time Temporal LogicwIt has some connectives for referring to the futurewIt models time as a sequence of states,extending infinitely to futurewcomputation pathwThe future is not determined,we should consider several paths for different futureswAny one of the paths can be the actual path that is realizedAmir PnueliThe Weizmann Institute of Science 35Syntax of LTLwwhere p is any propositional atom from some set AtomswX,F,G,U,R,W:temporal connectives36AtomswThey stands for atomic facts which hold for a systemwProcess 897 is blockedwThe variable x2 is zerowThe content of register R1 is 0101037Temporal ConnectiveswX:neXt statewF:some Future state(eventually)wG:all future states(Globally)wU:Until（1 U 2表示1 成立直到2 成立）wR:Release（1 R 2表示2 成立直到1 成立，或者2一直成立，即1 释放 2）wW:Weak-until（1 W 2表示1 成立直到2 成立，或者1一直成立）38LTL Informal SemanticswGlobally p:G pwG p is true in a state if p holds at all points of time(along the path)starting from that state p=Suppose G p holds in the initial state012339LTL Informal SemanticswEventually p:F pwF p is true in a state if p holds at some points in the future,stating from the state p=Suppose F p holds in the initial state012340LTL Informal SemanticswNext p:X pwX p is true along a path starting in a state if p holds in the next state p=Suppose X p holds in state at t=2012341LTL Informal Semanticswp Until q:p U qwp U q is true in state s ifwq is true in some state reachable from swp is true in all states from s until q holds p=q=Suppose p U q holds in the initial state012342LTL Informal SemanticswUntil says nothing about what happens after the Until has been realizedwThis can be different from natural English speakingwFor example:w“She continued working until she married”wWe may interpret the sentence as she discontinued working after marriagewThe above understanding is related to this formulawworking U(marriage G working)43LTL Informal Semanticswp Relase q:p R qwp R q is true in state s ifwp is true in some state reachable from swq is true in all states from s until p holdsOrwq is true in all states q=p=Suppose p R q holds in the initial state012344LTL Informal Semanticswp Weak-Until q:p W qwp W q is true in state s ifwq is true in some state reachable from swp is true in all states from s until q holdsOrwp is true in all states p=q=Suppose p W q holds in the initial state012345LTL Formal SemanticswTransition SystemwA transition system is a structure M=(S,L)wherewS:a finite set of statesw:a binary relation on S,such that every s S has some s S with s s wL:a labeling function L:S P(Atoms)wP(Atoms)means the power set of AtomswThe interpretation of the labeling function is that each state s has a set of atomic propositions L(s)which are true at that particular stateKripke structure46LTL Formal SemanticswTransition System Examplep,qq,rqs0s1s2S=s0,s1,s2transitions=s0 s1,s1 s1,s2 s1,s2 s0,s0 s2L(s0)=p,q L(s1)=q L(s2)=q,r47LTL Formal SemanticswPathswA path in a model M=(S,L)is an infinite sequence of states s1,s2,s3,in S such that,for each i 1,si si+1.wWe write paths as s1 s2 s3 wEach arbitrary path(e.g.=s1 s2)represents a possible future of the systemwfirst it is in s1,then s2 and so onwWe write i for the suffix starting at siw2 is s2 s3 48LTL Formal SemanticswLet M=(S,L)be a model and =s1 be a path in MwWhether satisfies an LTL formula is defined by the satisfaction relation as follows:1234567891049LTL Formal SemanticswUntil and Release are dual:R (U )111250LTL Formal Semanticsw W :Weak Until is related to the Until with the difference that it does not require that is eventually holdwEssentially W is a short form for writing U G51LTL satisfaction by a systemwSuppose M=(S,L)is a model,s S,and an LTL formulawWe write M,s if for every execution path of M starting at s,we have wSometimes M,s is abbreviated as s p,qq,rqs0s1s2p,qp,qs0q,rs2qs1qs1q,rs2s0p,qq,rs2s0qs1q,rs2qs1an arbitrary path1.M,s0 X q 2.M,s0 G(p r)3.M,s1 G q4.M,s0 p U q52Some practical patternswIt is impossible to get to a state where started holds,but ready does not holdwG(started ready)wFor any state,if a request occurs,then it will eventually be acknowledgedwG(requested F acknowledged)wWhatever happens,a certain process will eventually be permanently deadlockedwF G deadlockwA certain process is enabled infinitely often on every computation pathwG F enabledwIn other words,in a path of the system there must never be a point at which the condition enabled becomes false and stays false foreverwIf a process is enabled infinitely often,then it runs infinitely oftenwG F enabled G F running53LTL WeaknesswThe features which assert the existence of a path are not(directly)expressible in LTLwThis problem can be solved by:checking whether all paths satisfy the negation of the required propertywA positive answer to this is a negative answer to our original question and vice versa.wBUT:properties which mix universal and existential path quantifiers cannot in general be expressed in LTL54LTL Weakness：ExampleswLTL cannot express these features:wFrom any state it is possible to get to a restart state(i.e.,there is a path from all states to a state satisfying restart)wThe lift can remain idle on the third floor with its door closed(i.e.,from the state in which it is on the third floor,there is a path along which it stays there)wLTL cannot assert these because it cannot directly assert the existence of pathswHowever,CTL can express these properties55LTL Exercisew如果有乘客想去第五层，一个上行的电梯在第二层不应该改变方向。w floor2表示第二层为真w directionup表示上行为真w buttonPressed5表示按了按钮5w floor5表示第五层为真56计计算算树逻辑树逻辑CTLwLinear-time logics think of time as a set of pathswpath is a sequence of time instanceswBranching time logics represent time as a treewit is rooted at the present moment and branches out into the future57Linear vs.BranchingwLinear TimewEvery moment has a unique successorwInfinite sequences(words)wLinear Time Temporal Logic(LTL)wBranching TimewEvery moment has several successorswInfinite treewComputation Tree Logic(CTL)58CTL Syntax:=F|T|p|()|(/)|(/)|(-)|AX|EX|AU|EU|AG|EG|AF|EFWhere p ranges over atomic formulas注：1）CTL时态连接词是一对符号，第一个是A或E，第二个是X,F,G或U 2）当A或E后面配对的算子是U时，使用方括号，有助阅读 A:表示对所有路径 E:表示存在一条路径59Formal SemanticswLet M=(S,L)be a model and =s1 be a path in MwWhether satisfies an CTL formula is defined by the satisfaction relation as follows:1.M,s|=T and M,s|F for all s S2.M,s|=p iff p L(s)3.M,s|=iff M,s|4.M,s|=1/2 iff M,s|=1 and M,s|=25.M,s|=1/2 iff M,s|=1 or M,s|=26.M,s|=1-2 iff M,s|1 or M,s|=27.M,s|=AX iff for all s1 such that s-s1 we have M,s|=.Thus,AX says“in every next state”8.M,s|=EX iff for some s1 such that s-s1 we have M,s|=.Thus,EX says“in some next state”60Formal Semantics9.M,s|=AG holds iff for all paths s1-s2-s3-where s1 equals s,and for all si along the path,we have M,si|=.For all computation paths beginning in s the property holds Globally(including the initial state).10.M,s|=EG holds iff there is a path s1-s2-s3-where s1 equals s,and for all si along the path,we have M,si|=.There exist a path beginning in s such that the property holds Globally(including the initial state).61Formal Semanticsw11.M,s|=AF holds iff for all paths s1-s2-s3-where s1 equals s,there is some si along the path,such that we have M,si|=.For all computation paths beginning in s there will be some Future state where holds.w12.M,s|=EF holds iff there is a path s1-s2-s3-where s1 equals s,and for some si along the path,we have M,si|=.There exist a path beginning in s such that the property holds in some Future state.w13.M,s|=A1 U 2 holds iff for all paths s1-s2-s3-where s1 equals s,that path satisfies 1 U 2,i.e.there is some si along the path,such that we have M,si|=2,and,for each j s2-s3-where s1 equals s,that path satisfies 1 U 2,i.e.there is some si along the path,such that we have M,si|=2,and,for each j 0 rendezvous:dim=0mtype,constants,typedefs(records)69ProcesswA process is defined by a proctype definitionwexecutes concurrently with all other processes,independently of speed or behaviorwcommunicates with other processes wusing global(shared)variableswusing channelswThere may be several processes of the same type.wEach process has its own local state:wprocess counter(location within the proctype)wcontents of the local variables70ProcesswA process type(proctype)consist ofwa namewa list of formal parameterswlocal variable declarationswbodyproctype Sender(chan in;chan out)bit sndB,rcvB;do :out!MSG,sndB-in?ACK,rcvB;if :sndB=rcvB-sndB=1-sndB :else-skip fi odnamebodyformal parametersThe body consist of a sequence of statements.local variables71Processproctype Foo(byte x).init int pid2=run Foo(2);run Foo(27);active3 proctype Bar().wProcess are created using the run statement(which returns the process id).wProcesses can be created at any point in the execution(within any process).wProcesses start executing after the run statement.wProcesses can also be created by adding active in front of the proctype declaration.number of procs.(opt.)parameters will be initialised to 072Variables and TypesBasic typesbit turn=1;0.1bool flag;0.1byte counter;0.255short s;-215.215 1 int msg;-231.231 1Arraysbyte a27;bit flags4;Typedef(records)typedef Record short f1;byte f2;Record rr;rr.f1=.wFive different(integer)basic types.wArrayswRecords(structs)wType conflicts are detectedat runtimewDefault initial value of basic variables(local and global)is 0array indexing start at 0variable declaration73Variables and Typesint ii;bit bb;bb=1;ii=2;short s=-1;typedef Foo bit bb;int ii;Foo f;f.bb=0;f.ii=-2;ii*s+27=23;printf(“value:%d”,s*s);wVariables should be declared.wVariables can be given a value by:winitializationwassignmentwargument passingwmessage passingwVariables can be used in expressions.assignment=equality test=declaration&initialization74StatementswA statement is eitherwExecutable:if evaluates to non-zerowBlocked:if evaluates to zerowAn assignment statement is always executablewExamples:w1 always executablew0always blocked(halt)w2 3 always executablewX ),arrow is sometimes also used to show causal relation between successive statements75if-statementwIf there is at least one choice executable,if statement is executablewOne of the executable choices is non-deterministically chosenwIf no choice is executable,the if-statement is blocked until it becomes executableif:choice1-stat1.1;stat1.2;stat1.3;:choice2-stat2.1;stat2.2;stat2.3;:choicen-statn.1;statn.2;statn.3;fi76do-statementwBehaves in the same way as if-statement with respect to choiceswThe only difference is it repeatswbreak(always executable)exits a do-loopdo:choice1-stat1.1;stat1.2;stat1.3;:choice2-stat2.1;stat2.2;stat2.3;:choicen-statn.1;statn.2;statn.3;od77Interleaving semanticswPromela processes execute concurrently.wNon-deterministic scheduling of processes.wProcesses are interleaved,not statements within a single process.wStatements of different processes do not occur at the same time.wAll statements are atomic.78Assertionsproctype receiver(chan in)int value;in?value;assert(value=0|value=1)79Atomic Stepsint value;proctype increment()atomic x=value;x=x+1;value=x;80Message Passingchan qname=16 of shortqname!expr writing(appending)to channelqname?expr reading(from head)of the channelqname?expr “peaking”(without removing content)qname!expr checking if there is room to writecan declare channel for exclusive read or write:chan in,out;xr in;xs out;qname!exp1,exp2,exp3 writing several varsqname!expr1(expr2,expr3)type and paramsqname?vari(var2,var3)qname?cons1,var2,cons2 can send constantswLess parameters sent than received others are undefinedwMore parameters sent remaining values are lost wConstants sent must match with constants received81Examplesproctype A(chan q1)chan q2;q1?q2;q2!123proctype B(chan qforb)int x;qforb?x;print(“x=%dn”,x)initchan qname=1 of chan;chan qforb=1 of int;run A(gname);run B(qforb);qname!qforb82Randez-vous CommunicationswBuffer of size 0 can pass but not store messageswMessage interactions by definition synchronous#define msgtype 33chan name=0 of byte,byte;proctype A()name!msgtype(123);name!msgtype(121);/*non-executable*/proctype B()byte state;name?msgtype(state)initatomic run A();run B()83DiscussionwIf channel name has zero buffer capacity:wHandshake on message msgtype and transfer of value 123 to variable state.wThe second statement will not be executable since no matching receive operation in BwIf channel name has size 1:wProcess A can complete its first send but blocks on the second since channel is filled.wB can retrieve this message and complete.wThen A completes,leaving the last message in the channelwIf channel name has size 2 or more:wA can finish its execution before B even starts846.2 SMV ProgramwAn SMV program consists of:wDeclarations of the state variables(b0 in the example);the state variables determine the state space of the model.wAssignments that define the valid initial states(init(b0):=0).w Assignments that define the transition relation(next(b0):=!b0).85ExampleMODULE mainVAR request:boolean;state:ready,busy;ASSIGN init(state):=ready;next(state):=casestate=ready&request:busy;TRUE :ready,busy;esac;SPEC AG(request-AX(state=busy)86ready!requestbusy!requestreadyrequestbusyrequest87SMV ExpressionsExpr:atom -symbolic constant|number -numeric constant|id -variable identifier|“!”Expr -logical not|Expr&Expr-logical and|Expr|Expr -logical or|Expr-Expr -logical implication|Expr Expr -logical equivalence|“next”“(“id“)”-next value|Cas