Software Modeling and Analysis
Software Modeling and Analysis EECS 755
Popular in Course
Popular in Elect Engr & Computer Science
verified elite notetaker
This 46 page Class Notes was uploaded by Melissa Metz on Monday September 7, 2015. The Class Notes belongs to EECS 755 at Kansas taught by Staff in Fall. Since its upload, it has received 37 views. For similar materials see /class/186809/eecs-755-kansas in Elect Engr & Computer Science at Kansas.
Reviews for Software Modeling and Analysis
Report this Material
What is Karma?
Karma is the currency of StudySoup.
You can buy or earn more Karma at anytime and redeem it for class notes, study guides, flashcards, and more!
Date Created: 09/07/15
Introduction to Model Checking Ken McMillan Cadence Berkeley Labs mcmillancadencecom Outline 0 Model checking Temporal logic Model checking algorithms Expressiveness and complexity o Symbolic model checking The state explosion problem Binary Decision Diagrams Computing fixed points with BDD s Application Propositional Linear Temporal Logic 0 Express properties of Reactive Systems interactive nonterminating o For PLTL a model is an infinite state sequence 0s0sls2 0 Temporal operators Globally Gp att iff p for all fat Temporal operators Future Fp att iff p for some t zt Until pUq att iff q for some fat and p in the range t zquot Next time Xp att iff pat t1 Examples o Liveness if input then eventually output G input 2 F output i i 0 Strong fairness infinitely send implies infinitely recv GF send 2 GF recv T T in nitely often 0 Weak until no output before input noutput Winput Safety v Liveness 0 Safety Refutable by finite run 0 Liveness Refutable only by infinite run Every finite run extensible to satisfying run PLTL semantics 0 Given an infinite sequence 0 Soas19S2 0 s if q is true in state s of 0 a if q is true in state so of 0 gb if q is valid 0 A formula is an atomic proposition or true PVC P PUq XP PLTL semantics z i EQW PMQW cu F39 le a atomic Casi i 39P 0 s 19qu 091 Xfp Onasi p wfq Derived operators Ls a atomic 0s7 p 0si p or 05 q G SHI p forsome210sj q andforalliskltjz ask 1 pAqE bpv q FpEtruqu GpE F p Model Checking ClarkeEmerson QueiIIeSifakis yes temporal formula MC algorithm finitestate model counterexample Model must now represent all behaviors Kripke models o A Kripke model SERL consists of set of states 8 set of transitions R Q S x S labeling L Q S x AP 0 Kripke models from programs repeat p true p false 0 end Mutual exclusion example N noncritical T trying C critical PLTL on Kripke models o A path in made M SRL t3 3 sequence a s0sls2ES gush that 3435251 E R p O 3 p s2 s3 Fp O p A4950 f iff forallpathsa sosls2 of 0s0 f Branching time 0 Medal QHime is a tree mi 3 sequence p 0 H I0 AFp p 0 Path quanti ers Ms0 Af iff forallpaths as0sls2ofM a f Ms0 Ef iff forsomepaths O S0S1S20fM a f Computation Tree Logic 0 Every operator F G X U preceded by A or E o Univergal modalities AGp AFp CTL cont o Exig er ia madahmgs EGp EFp CTL cont o Other modalities AXp EXp Ap Uq Ep Uq 0 Some dualities AGp E EFp AFp E EGp 0 Examples mutual exclusion specs AG C1 A C2 mutual exclusion AG T1 gt AF C1 liveness AG N1 gt EX T1 nonblocking CTL model checking 0 Model checking problem Determine for given M 80 and 7 whether MOof 0 Simple algorithm Inductive over structure of formula Backward propagation of formula labels Of VV E Example AG Tl gt AF C1 lt M Vi gt Vii LIE CES algorithm 0 Need grimy medialiiiee EX eg AG 5 EFp AFp E EGIp Checking Ep U q by backward BFS Checking EG p Complexity OfV E CTL 0 Contains both CTL and LTL path formulas pUq Gp Fp Xp en in q state formulas A p E p p in LTLeApin CTL 0 Framework for comparing expressiveness Existential properties not expressible in PLTL eg AG EF p Fairness assumptions not expressible in CTL eg A GFp 9 GF q 20 Model checking complexities CTL PLTL 02fVEgt l l PSPACE COMPLETE Note all are linear in model size 21 Comparing CTL and LTL 0 Think of CTL formulas as approximations to LTL AG EF p is weaker than G F p 00 Good for nding bugs P AF AG p is stronger than F G p O p p Good for verlfylng o CTL formulas easier to verify So use CTL when it applies 22 Symbolic model checking 0 State explosion problem State graph exponential in program size 0 Symbolic model checking approach Boolean formulas represent sets and relations Use fixed point characterizations of CTL operators Model checking without building state graph Sometimes can handle much larger sate space 23 Binary Decision Diagrams Bryant ab Cd 0 Ordered deciaim tree for f OBDD reduction 0 Reduced QBDD farm 01 Key idea combine equivalent subcases 25 OBDD properties o Canonical form for fixed order direct comparison 0 Efficient apply algorithm A build BDD s for large circuits 2 0Ifl IQI 0 Variable order strongly affects size 26 Boolean quantification o If v is a boolean variable then 3vf fv0V fv1 o Multivariate quantification Elw1w2wn f Example 3076 ab V Cd a V d 0 Complexity on BDD representation worst case exponential heuristically efficient 27 Characterizing sets 0 Let M SRL be a Kripke model Let S be the set of boolean vectors v1v2vn E 01n Represent any P Q S by its characteristic function XP p v1v2vn xp Set operations Xgfase Xstrue XPUQPVQ XPOQPAQ XSP P 28 Characterizing relations 0 Transition relation F3 is a set of state pairs R v1v2vn v 1v 2v n E XR 0 Examples A synchronous sequential circuit X52 V30 39 V0A V51 Vocal1 29 Transition relations cont An asynchronous circuit quotI ol Interleaving model M q39 A q A 6739 67 v t739 FA q A q39 q Simultaneous model 0 q39 A 67 v q39 q A 4739 FA 1 v 39 a 30 Forward and reverse image 0 Forward image ImagePR v39 for some v vEP and v v39ER IL XImagePR V39 3V XPV A X12 st39 31 Images cont 0 Reverse image Imagequot1PR p Image391P R v for some v 39 v EP and VV39ER X1magePR V 3V39 X19 V39 A Xx VaV39 32 Symbolic CTL model checking o Equate a formula f with the set of states satisfying it f VES v f 0 Compute BDD s for characteristic functions p pvq pAq useBDDops EX p Image1pR AX p EX p o Remaining operators have fixedpoint characterization EFp E vaXEFp In fact this is the least fixed point 33 Fixed points of monotonic functions 0 Left be a function 8 a S 0 Say 1 is monotonic when x E y implies 17x 102 0 Fixed point Of l is ysuch that 1y y 0 H1 monotonic then it has least fixed point My ry greatest fixed point vy IY 34 Iterativer computing fixed points o Stulpncse S is finite The least fixed point My ty is the limit of false C 17false g 171false g The greatest fixed point vy ty is the limit of true 2 rtrue 2 mama 2 Note since S is finite convergence is finite 35 Example EFp 0 EF p is characterized by EFpMyvaXy 0 Thus it is the limit of the increasing series PV vaXp p EXpVEXp which we can compute entirely using BDD operations 36 Example EG p 0 EG p is characterized by EGp vy p AEXy 0 Thus it is the limit of the decreasing series pA Q EXp EXp P A EXP which we can compute entirely using BDD operations 37 Remaining operators AFp AGp EpUq ApUq icyp v AX y WP A AX y uyq v p A EX y W q v p A AX y o Allowe CTL model Checking with only BDD ope Avoid building state graph Sometimes avoid state explosion problem Now you can go home and build your own symbolic model checker 38 Example Gigamax cache protocol global bus cluster bus 0 Bus Snooping maintams local ool glotenoy 0 Message passlng protocol folquot global consistency 39 Protocol example global bus cluster bus owned copy read miss 0 Cluster 8 read gt Cluster A o Cluster A respornse gt B and main memory 0 Clusters A and B end shared 40 Protocol correctness issues 0 Protocol issues deadlock unexpected messages liveness o Coherence each address is sequentially consistent store ordering system dependent o Abstraction is relative to properties specified 41 Specifications 0 Absence of deadlock SPEC AG EF preadable amp EF pwritable o Coherence SPEC AGpreadable amp bit gt EFpreadable amp bit 43 Counterexample deadlock in 13 steps global bus UIC UIC C cluster bus iii iii owned copy from clusterA o Cluster A read gt global waits takes look 0 Cluster C read agt cluster B o Cluster B response gt C and main memory 0 Cluster C read gt clusterA takes look 44 State space explosion 0 State space growth is exponential 45 BDD performance o BDD size growth is linear 46 BDD performance 0 Run time growth is quadratic 47
Are you sure you want to buy this material for
You're already Subscribed!
Looks like you've already subscribed to StudySoup, you won't need to purchase another subscription to get this material. To access this material simply click 'View Full Document'