现代软件工程SoftwareVerification

1、Satish MishraIntroduction to UML1Morden Software Engineering Shengbing RSchool of Software , Central South University2Software Verification31. 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 integ

2、er.4More Software Bugshttp:/www5.in.tum.de/huckle/bugse.html52. 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)wM

3、odel Checking ( exhaustive testing of a model of the system)wPeer Reviewing: amounts to software inspection cataches 31% 93% of the defects6Testing Is HardTesting parallel and distributed systems is not always cost effective.wTesting concurrency related problems is often done only when rest of the s

4、ystem 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.7SimulationwThe main method for the valida

5、tion of hardware designs.wConsider using simulation/prototyping for software.8Deductive 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.9Model Checking10Model

6、CheckingMModelCheckerp F qyesnoError Trace11wTuring Award 2007wE.M. Clarke, E.A. Emerson and J. Sifakis12Model Checking ProcesswModeling PhasewModel the systemwPerform some simulationwFormalize the propertywRuning PhasewRun the model checkerwTo check the validity of the property in the system modelw

7、Analysis 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 again13The specification of system propertieswFunctional corr

8、ectnesswDoes 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 ac

9、ting in time?14Benefits 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

10、related featureswIt supports partial verification.wIt can be easily integrated in existing development cycles.wIt has a sound and mathematical underpinning.15Model Checking Applied in the Earlier Phasesanalysisrequirementsspecificationdesigncodingtestingreleasemaintain16Drawbacks of Model CheckingwS

11、tate 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 obt

12、ain models is time consuming and often futilewIt verifies a system model.wIt is mainly appropriate to control-intensive applications.17Verification and ValidationwVerification:wTo check that the design satisfies the requirements that have been identified.wTo check that we are buildings the things ri

13、ght.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.183. Model Checker: SPINwSPIN (Simple Promela Interpreter) wDeveloper: Gerard J. Holzmann wIt was the winner of the 2001 ACM Software System Awa

14、rdwSome 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 a

15、pplicable to large and highly complex software systems.Gerard J. Holzmann NASA JPL Laboratory for Reliable Software19Model Checker: SPINwispin安装w1) 安装ActiveTCL，运行ispin.tcl界面描述程序w2）安装cygwin,select packages选中Devel为Installw3）安装graphviz2.26.3,图形显示自动机w4）将PC-Spin625解压到某文件夹，例如：C:ispinw5）修改c:ispin中的ispin.tc

16、l文件，将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。20Spin, Promela, iSpinC compilerSPINAnalyzer(exec)VerificationoutputErrortrailModel(Promelasource)SimulationoutputSimulation: random, interacti

17、veguidedAnalyzer(C source)Verification21Model Checker: SPINwIspin界面：创建或打开PML模型（*.pml文件）22Model Checker: SPINw模型验证如果有错误，则如果有错误，则生成生成*.trail文文件。件。23Model Checker: SPINw仿真或回放244. Model Checker: NuSMVwNuSMV (New Symbolic Model Verifier)wNuSMV是开源的wSPIN仅仅支持LTL属性检测wNuSMV支持LTL属性和CTL属性检测w是Carnegie Mellon Uni

18、versity(CMU) 和Italy的ITC-IRST的合作项目，是对CMU的SMV再工程的结果w增强用户与系统的交互能力w提供更多启发式策略w结构更加模块化w实现更加鲁棒化和模块化w点击NuSMV-zchaff-2.5.4-i386-pc-mingw32.rar即可安装。25NuSMV结构结构26SMV： HistoryCMUSMVCadenceSMVNuSMVlStrong abstraction functionslGUIlNew languagelOldest VersionlNo GUITwo versionsl2.x: Open Source, many new features

19、, BDD and SAT based backendsl1.x: Original version, had a GUI27Model 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显示执行结果28w模型检测步骤：w在NuSMV输入go 建立系统模型w在NuSMV输入Check_l

20、tlspec 检测LTL属性规范w在NuSMV输入show_property 显示属性的状态w【属性类型 属性状态 反例号 属性名】w如果有反例号，则可以用show_traces 反例号 显示检测情况w有界模型检测步骤：w在NuSMV输入go_bmcw在NuSMV输入check_ltlspec_bmc_onepb k -l w其中，x表示界限长度，y表示循环展开长度29NuSMV实例实例wMODULE mainwVARw y:0.15;wASSIGNw init(y):=0;wTRANSw casew y=7: next(y) = 0;w TRUE: next(y) = (y+1) mod 1

21、6;w esacw- LTLSPEC !G F (y=2)wLTLSPEC F(X y=9 );30NuSMV仿真仿真31NuSMV模型检测模型检测w属性不满足，存在反例！32NuSMV模型检测模型检测33Useful 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:/n

22、usmv.fbk.eu/faq.htmlwNuSMV on Andreww/afs//usr11/arieg/public/nusmv/2.5.3/wNuSMV examplesw/share/nusmv/exampleswKen McMillan, Symbolic Model Checking: An Approach to the State Explosion Problem, 1993whttp:/ Temporal Logicw在一个模型中，公式的真与假是动态的。w时态逻辑：把包含时态动词的语句形式化，并把含有这种语句的推理系统化w例如： F A表示将来

23、某个时间命题A为真w模态逻辑：涉及必然性和可能性。w必然算子 可能算子 w两种常用的时态逻辑：w线性时态逻辑LTL （Linear-time Temporal Logic）w计算树逻辑CTL (Computation Tree Logic)w在软件验证（模型检测）中，采用时态逻辑描述系统属性。35线性时态逻辑线性时态逻辑wLTL : Linear-time Temporal LogicwIt has some connectives for referring to the futurewIt models time as a sequence of states, extending inf

24、initely 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 36Syntax of LTLwwhere p is any propositional atom from some set AtomswX, F,

25、 G, U, R, W : temporal connectives37AtomswThey stands for atomic facts which hold for a systemwProcess 897 is blockedwThe variable x2 is zerowThe content of register R1 is 0101038Temporal ConnectiveswX : neXt statewF : some Future state ( eventually)wG : all future states (Globally)wU : Until （1 U 2

26、表示1 成立直到2 成立）wR : Release（ 1 R 2表示2 成立直到1 成立，或者2一直成立，即1 释放 2 ）wW : Weak-until （1 W 2表示1 成立直到2 成立，或者1一直成立）39LTL 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 state012340LTL Inf

27、ormal 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 state012341LTL 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 hold

28、s in state at t=2012342LTL 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 state012343LTL Informal SemanticswUntil says nothing about what happens after t

29、he 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)44LTL Info

30、rmal 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 state012345LTL Informal Semanticswp Weak-Until q : p W qwp W q is true in state s i

31、fwq 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 state012346LTL Formal SemanticswTransition SystemwA transition system is a structure M = (S, , L) wherewS: a finite set of statesw : a binary r

32、elation 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 structure47LTL F

33、ormal 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,r48LTL 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 w

34、rite 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 49LTL Formal SemanticswLet M = (S, , L) be a model and = s1 be a path in MwWhether satisfies an LTL formula

35、 is defined by the satisfaction relation as follows:1234567891050LTL Formal Semanticsw Until and Release are dual : R ( U )111251LTL 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

36、 U G52LTL 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 pathM, s0 X q M, s0 G (p r)M

37、, s1 G qM, s0 p U q53Some 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

38、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

39、, then it runs infinitely oftenwG F enabled G F running54LTL 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 negativ

40、e answer to our original question and vice versa.wBUT: properties which mix universal and existential path quantifiers cannot in general be expressed in LTL55LTL 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

41、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, C

42、TL can express these properties56LTL Exercisew如果有乘客想去第五层，一个上行的电梯在第二层不应该改变方向。w floor2表示第二层为真w directionup表示上行为真w buttonPressed5表示按了按钮5w floor5表示第五层为真57计算树逻辑计算树逻辑CTLwLinear-time logics think of time as a set of pathswpath is a sequence of time instanceswBranching time logics represent time as a treewi

43、t is rooted at the present moment and branches out into the future58Linear vs. Branchingw Linear TimewEvery moment has a unique successorwInfinite sequences (words)wLinear Time Temporal Logic (LTL)w Branching TimewEvery moment has several successorswInfinite treewComputation Tree Logic (CTL)59CTL Sy

44、ntax:= 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:表示存在一条路径60Formal SemanticswLet M = (S, , L) be a model and = s1 be a path in MwWhether satisfies an CTL

45、 formula is defined by the satisfaction relation as follows:n M,s|= T and M,s|F for all s SnM,s |= p iff p L(s)nM,s |= iff M,s | nM,s |= 1 / 2 iff M,s |= 1 and M,s |= 2nM,s |= 1 / 2 iff M,s |= 1 or M,s |= 2nM,s |= 1 - 2 iff M,s | 1 or M,s |= 2wM,s |= AX iff for all s1 such that s-s1 we have M,s|= .

46、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”61Formal Semanticsw9. 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 i

47、n s the property holds Globally (including the initial state).w10. 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).62Formal Semantic

48、sw11. 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

49、 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

50、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)70ProcesswA process is defined by a proctype definitionwexecutes concurrently with all other proce

51、sses, 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 variables71ProcesswA

52、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

53、of statements.local variables72Processproctype 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 execu

54、ting 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 073Variables and TypesBasic typesbit turn=1;0.1bool flag;0.1byte counter;0.255short s;-215. 215 1 int msg; -231. 231 1Arraysbyte

55、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 declaration74Var

56、iables 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 expressio

57、ns.assignment =equality test =declaration &initialization75StatementswA 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

58、 sometimes also used to show causal relation between successive statements76if-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 execu

59、tableif: choice1 - stat1.1; stat1.2; stat1.3; : choice2 - stat2.1; stat2.2; stat2.3; : : choicen - statn.1; statn.2; statn.3; fi77do-statementwBehaves in the same way as if-statement with respect to choiceswThe only difference is it repeatswbreak ( always executable ) exits a do-loopdo: choice1 - st

60、at1.1; stat1.2; stat1.3; : choice2 - stat2.1; stat2.2; stat2.3; : : choicen - statn.1; statn.2; statn.3; od78Interleaving semanticswPromela processes execute concurrently.wNon-deterministic scheduling of processes.wProcesses are interleaved, not statements within a single process.wStatements of differen