ࡱ> Y(   ~*murali@cs.clemson.edu8mailto:murali@cs.clemson.edu/ 0DTimes New RomanTT؂ܖ 0ܖDGaramond RomanTT؂ܖ 0ܖ DWingdingsRomanTT؂ܖ 0ܖ0DArialngsRomanTT؂ܖ 0ܖ"@DComic Sans MSnTT؂ܖ 0ܖBPDSymbolans MSnTT؂ܖ 0ܖ A .  @n?" dd@  @@``   (  AD   3""! )WU O fW&! !#$& 0AA 3@T! g4dddd 0d8ppp@ R ʚ;l8ʚ;<4!d!d l 0 <4dddd l 0 h___PPT2001D<4X0___PPT10 2___PPT9/ 0? %,  0` 3` ff>>\fg` J*T333` QYmx~3ft` \ғhEy`` cb^DDf`Y˵W` sg7xGr` K%ޯd{mG/` 33f>?" dd@,?nFd@    @ `  n?" dd@   @@``PR    @ ` `<p>> 0n(    6\ #" `b `  H*0    6h #" `` `  J* 0  xT ~  "~\ {  "{  c BB CDEFd @ bb   H   T W6Vw}\gFQ6<1++11 1L b6xQrq 6\}N   - c    0 A Q g     S    6N KawF bFy0 a*ly7lE;uz  B | a F 0 ! 1 < B < & l L 0  @`"T   c |BC+DEFyd @ ==gL6cI}\eA& w6m!W<! &<W!r6W}F6\}>68QNlX^XH8+Sgg|@`"Jo 5 J   B! CDEF @ ))\*l{FDNF W% W ! !   ! 6X L b x_ /aF6b}SA$|l\\TX@`s"*  T  u4   B C%DEF ss&QW}k6D Q r 8 N c t y y ;t Qi gS }8     T   :0\-Q4*%%v*o(V}5q;  S   < s } l \ g} \, L ;n &  Z}\[6 }WF<! e C }h m W ]  ,t B RxkqA,Rg@`" {b    BCDEFy @ ,,Lh6\}mWG &a*zCxsh-&jG]~5g6&LLZ\@`s"*   u(     BCDE|Fy @ __@% M|f4@{ f0`lA}L\A+h MB6ww FJl{ 0V|{J  *5KlGn a*:Pf\|6 /6Kbf|F kP}5x}VvaP@@@`s"*   =>    c BlCrDEF"d@ rlrl@`"~   6Xq " `}  T Click to edit Master title style! !  6xv #" ``   J* 0  $  0u " `  RClick to edit Master text styles Second level Third level Fourth level Fifth level!     SB  s *޽h ? 3___PPT10i. u%.+D=' = @B +  Stream  0 @-(  xT ~  "~\ {  "{  c BB CDEFd @ bb   H   T W6Vw}\gFQ6<1++11 1L b6xQrq 6\}N   - c    0 A Q g     S    6N KawF bFy0 a*ly7lE;uz  B | a F 0 ! 1 < B < & l L 0  @`"T   c |BC+DEFyd @ ==gL6cI}\eA& w6m!W<! &<W!r6W}F6\}>68QNlX^XH8+Sgg|@`"Jo 5 J   B! CDEF @ ))\*l{FDNF W% W ! !   ! 6X L b x_ /aF6b}SA$|l\\TX@`s"*  T  u4  B C%DEF ss&QW}k6D Q r 8 N c t y y ;t Qi gS }8     T   :0\-Q4*%%v*o(V}5q;  S   < s } l \ g} \, L ;n &  Z}\[6 }WF<! e C }h m W ]  ,t B RxkqA,Rg@`" {b   BCDEFy @ ,,Lh6\}mWG &a*zCxsh-&jG]~5g6&LLZ\@`s"*   u(     BCDE|Fy @ __@% M|f4@{ f0`lA}L\A+h MB6ww FJl{ 0V|{J  *5KlGn a*:Pf\|6 /6Kbf|F kP}5x}VvaP@@@`s"*   =>    c BlCrDEF"d@ rlrl@`"~   < "F   T Click to edit Master title style! !   0Ȁ " `    W#Click to edit Master subtitle style$ $   6ȑ #" `` `  H*0    6䛷 #" `b   J* 0    6Ȧ #" `d `  J* 0  B  s *޽h ? 3___PPT10i. u%.+D=' = @B +  0` ̙33` ` ff3333f` 333MMM` f` f` 3>?" dd@,|?" dd@   " @ ` n?" dd@   @@``PR    @ ` ` p>> `(    6Pn "P n T Click to edit Master title style! !$  0*  0,n "`  n @*  0 Xn "`  n @*H  0޽h ? ̙33 $Blank Presentation 0 `(    <E*pp < YThis research is funded in part the U. S. National Science Foundation grant CCR-0113181. ZY   <~4$ c!DEET for Component-Based Software&"!3   <8O*?-Z  zMurali Sitaraman, Durga P. Gandi Clemson University Wolfgang Kchlin, Carsten Sinz Universitt Tbingen Bruce W. Weide The Ohio State University*5`E  Z  <]* P  HCorrespondence: murali@cs.clemson.edu http://www.cs.clemson.edu/~resolve(I&#3*  0%H  0޽h ? ̙33y___PPT10Y+D=' = @B + 0 0(    6 *  C What is DEET?3  0*    bDEET is Best Bug Repellent  New England Journal of Medicine, 2002. DEET is Detecting Errors Efficiently without Testing. :{  @H  0޽h ? ̙33___PPT10i.?I+D=' = @B +' 0 NF@(    6T*  d.Correctness Problem and Well-Known Approaches//3  0*  P  tProblem: Does the program do what is specified to do? Formal verification objective: Prove that it does, using static analysis. Testing (and runtime checking) objective: Find errors, i.e., find mismatches between specified intent and program behavior, through execution.2   H  0޽h ? ̙33y___PPT10Y+D=' = @B + 0 P(    6*  W!DEET vs. Verification vs. Testing""3  0*    )DEET is a static analysis approach, like formal verification. DEET is intended for error detection, like testing. DEET has potential to serve as a cost-effective and efficient prelude to both testing and verification.  H  0޽h ? ̙33y___PPT10Y+D=' = @B +e 0 |t` (    6*  SBenefits of the DEET Approach3  06 ` 5It can analyze one component at a time in a modular fashion. It does not depend on code or even stub availability for reused components; it can detect substitutability bugs. It is automatic and does not require manual input selection. It can pinpoint the origin of the error in a component-based system. L=  q   6H  0޽h ? ̙33___PPT10i. +D=' = @B + 0 pt(    6T6  o9Contextual Differences Between DEET and Other Approaches::3_  0h 6   7Context of Alloy and ESC industrial languages, such as Java objectives are incremental based on current practice minimal expectations of programmers Context of DEET research language, i.e., Resolve objectives are set in the context of software practice as it could be a competent programmer hypothesis      ^'H  0޽h ? ̙33___PPT10i.b`:+D=' = @B + 0  c(     B0CDEF"p `0@`S" ``   6,6  q;Component-Based Software Using Design-By-Contract Paradigm<<32  3 r?Pp P 2  3 r?P P 2  3 r?P 0 ^B   6D j ^B  @ 6Dz  j    <%6   <uses   3 r?P    <$*6  B implements   3 r?P @  3 r?P@   3 r?P @dB  <Do  dB  <Do@ @` dB  <Do@ 0 dB  <Do p dB  <Do  dB  <DԔ 0 dB  <Do   <06 NF  B implements ^B @ 6D@0 ^B  6Dp P ^B  6D @ 0  <66@ <  <uses  <;6 P  B implements ^B @ 6D@ ^B  6D     <@6& <usesH  0޽h ? ̙33___PPT10i.+D=' = @B + 0 V(    6TG6  ]'Ramifications of Contextual Differences((3S  0I6  0  DEET is a step towards meeting the larger objective of specification-based modular verification. In Resolve, components have specifications, and implementations are expected to have loop invariants, representation invariants, abstraction relations. Clean and rich semantics of Resolve allows variables to be viewed as having values from arbitrary mathematical spaces; references are not an issue. 2   H  0޽h ? ̙33___PPT10i.b`:+D=' = @B +3 0 JB`(  ` ` 6L6 > < An Example 3H ` 0޽h ? ̙33___PPT10i.7+D=' = @B +B 0 ia(    6pl6 ` Abstraction in Specification,3,  06   sThink of a List as a pair of mathematical strings: A string of entries that are to the left of the "current position", and A string of entries to the right. Initially, both strings are empty. 3 j $  3$;%H  0޽h ? ̙33y___PPT10Y+D=' = @B +O 0 v n e (    6`6 ` (View of a List of Trees with Abstraction,)(3, ~ $ J3  c"$P0z N K S X99?$HB LB C DAHB M C DAmHB N C DmHB O C DAB HB PB C DHB Q C DHB R C DHB SB C D7HB T C DcHB U C D7cHB V C D+ HB W C D  X 3 6X"`9 ]-  E S1 = ( <  Y 3 H6Y"`m/  =,  Z 3 6Z"`]7-  A> , <  [ 3 6["`c]!-  ?> ) HB \B C DA. m3HB ] C Dm. /3HB ^ C DA-//HB _ C Dm3nf ` 3 L6`"`9  E S2 = ( <  a 3 6a"`  A> , <  b 3 `6b"` Q! ?> ) HB c C Dm. n/ d 3 6d"`& @Left  e 3 p6e"`&}" ARight H  0޽h ? ̙33y___PPT10Y+D=' = @B + 0  0(    6l6 ` }View After Insert (T, S2),3,~~ $ {3  c"$0 N | S X99?$HB }B C DbHB ~ C DAbHB  C DbAdHB  C DbHB B C DZ_HB  C DZ_HB  C D\^HB B C D ^HB  C D7^HB  C D ^7_HB  C D^HB  C Da  3 d6"`w )S E S2 = ( <   3 6"`A =,   3 |6"`)  A> , <   3 6"`7)  ?> )   3 H6"`9 _ '/  AT =  HB B C D  HB  C D  HB  C D  HB  C D  (2  S_  HB B C DiHB  C DAiHB  C DiAlHB  C DiHB B C Db gHB  C Db gHB  C DceHB B C D% eHB  C D%  eHB  C De gHB  C D% e& HB  C Di  3 @6"`w 0S E S2 = ( <   3 6"`A =,   3 T6"`0  A> , <   3 6"` 0?$ ?> ) HB B C DunHB  C DfHB  C DnHB  C Dufh(2   07e  3 6"` =, H  0޽h ? ̙33y___PPT10Y+D=' = @B + 0 t;(  t t 67  WMathematical Modeling&3> t 0P7,p Concept List_Template (type Entry); uses String_Theory, & ; Type List is modeled by ( Left: String(Entry); Right: String(Entry) ); exemplar S; initialization ensures S.Left = empty_string and S.Right = empty_string; ... end List_Template;p 3 30  ,)!BH t 0޽h ? ̙33___PPT10i.x+D=' = @B + 0 x(  x x 67  QList Operations&3 x 0=7P TConcept List_Template (type Entry); uses & Type List is modeled by & Oper Insert(E: Entry; S: List); Oper Remove(E: Entry; S: List); Oper Advance(S: List); Oper Reset(S: List); Oper Advance_To_End(S: List); Oper Left_Length(S: List): Integer; Oper Right_Length(S: List): Integer; Oper Swap_Rights(S1, S2: List); end List_Template;DV 3 3333 3 3  3 3 3, F!BH x 0޽h ? ̙33___PPT10i.`+D=' = @B +\ 0 sk|(  | | 6@7  h&Design and Specification of Operations&'&3 | 0$7` Operation Insert(clears E: Entry; updates S: List); Ensures S.Left = #S.Left and S.Right = <#E> #S.Right; Operation Remove(replaces E: Entry; updates S: List); Requires |S.Right| > 0; Ensures S.Left = #S.Left and #S.Right = S.Right; 3   $ $    3   $ $   & E !BH | 0޽h ? ̙33___PPT10i. dR+D=' = @B +H 0 _W (    67 > QPart II: Erroneous Code Example 3H  0޽h ? ̙33___PPT10i.`:+D=' = @B +~ 0 0%(    6t7  aA Specification of List Reverse& 3  0L7 xOperation Reverse(updates S: List); Requires |S.Left| = 0; Ensures S.Left = #S.RightRev and S.Right = empty_string;y 3    P/ !BH  0޽h ? ̙33___PPT10i.Pڱ+D=' = @B +8  0 O G @%P (  P P 6|W7 ` Example Behavior of Reverse,3,L P c $X99?P0z FB P@ S DJ@ "FB P S DJ ` "FB  P S D"@ ` #FB  P S D" FB  P@ S D !FB  P S D!FB  P S D  FB P S D! P C 7P"``@ i Q#S = ( < > , <  P C 7P"` X  =,  P C D7P"`i ?> ) FB P@ S D0 9 FB P S D 9 FB P S D7 0 8 FB P S D9  P C 7P"` `0  G S = ( <  P C 7P"` @  A> , <  P C x7P"`   ?> )  P C ,7P"` Y @Left   P C 7 P"`` Y ARight @B !P@ C D` p 8 @B "P C D` 8 @B #P C D8 p 9 @B $P C D8  %P 3 `7%P"` h g =, H P 0޽h ? ̙33___PPT10i.0+D=' = @B +o 0 ~P (      6L7  ]An Erroneous Implementation&3   0I   Procedure Reverse (updates S: List); decreasing |S.Right|; Var E: Entry; If Right_Length(S) > 0 then Remove(E, S); Reverse(S); Insert(E, S); end; end Reverse;     /3 H   0޽h ? ̙33___PPT10i.[+D=' = @B +G 0 ^V`,(  , , 6I > PDEET Steps for Error Detection3H , 0޽h ? ̙33___PPT10i. ~+D=' = @B +  0 p8 (  8 8 68 I  _)Step 1: Verification Condition Generation**3 8 0I   eWhat do we need to prove that the code is correct? What can we assume? What do we need to confirm? $d  fH 8 0޽h ? ̙3380___PPT10.JM 0 @8$(  $ $ 64I  k)Step 1: Verification Condition Generation&*)3 $ 0`#I   _ Procedure Reverse (updates S: List); decreasing |S.Right|; Var E: Entry; 0 Assume: |S0.Left| = 0; If Right_Length(S) > 0 then Remove(E, S); Reverse(S); Insert(E, S); end; 5 Confirm: S5.Left = S0.RightRev and S5.Right = empty_string end Reverse;8      33 /33 33333 333 3 33 H $ 0޽h ? ̙3380___PPT10.[ 0 :2((  ( ( 6@I  _)Step 1: Verification Condition Generation**3 ( 0|HI 0 0 e7State Path Assume Confirm Condition 0 |S0.Left| = 0 If Right_Length(S) > 0 then 1 |S0.Right| > 0 S1 = S0 |S1.Right| > 0 Remove(E, S); 2 |S0.Right| > 0 S2.Left = S1 .Left and S1.Right = S2 .Right |S0.Left| = 0 and |S2.Right| < |S0.Right| Reverse(S); 3 ... ...83 33 33 33 33 $ 33 33 33 333333H ( 0޽h ? ̙3380___PPT10.s 0 }L(  L L 6KI  Y#Step 2: Error Hypothesis Generation$$3 L 0?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqrstuvwxyz{|}~Root EntrydO)0 $߽Current UserPSummaryInformation(UPowerPoint Document(XDocumentSummaryInformation8\؂ܖ 0ܖDGaramond RomanTT؂ܖ 0ܖ DWingdingsRomanTT؂ܖ 0ܖ0DArialngsRomanTT؂ܖ 0ܖ"@DComic Sans MSnTT؂ܖ 0ܖBPDSymbolans MSnTT؂ܖ 0ܖ A .  @n?" dd@  @@``   (  AD   3""! )WU O gW&! !#$& 0AA 3@T! g4dddd 0 ppp@ R ʚ;l8ʚ;<4!d!d l 0 <4dddd l 0 h___PPT2001D<4X0___PPT10 2___PPT9/ 0? %, 0   fH (    6`6 ` (View of a List of Trees with Abstraction,)(3, ~ $ J3  c"$P0z  K s **X99?$ .EHB LB C DAHB M C DAmHB N C DmHB O C DAB HB PB C DHB Q C DHB R C DHB SB C D7HB T C DcHB U C D7cHB V C D+ HB W C D  X 3 6X"`9 ]-  E S1 = ( <  Y 3 H6Y"`m/  =,  Z 3 6Z"`]7-  A> , <  [ 3 6["`c]!-  ?> ) HB \B C DA. m3HB ] C Dm. /3HB ^ C DA-//HB _ C Dm3nf ` 3 L6`"`9  E S2 = ( <  a 3 6a"`  A> , <  b 3 `6b"` Q! ?> ) HB c C Dm. n/ d 3 6d"`& @Left  e 3 p6e"`&}" ARight H  0޽h ? ̙33y___PPT10Y+D=' = @B +r> .wY(   ~*murali@cs.clemson.edu8mailto:murali@cs.clemson.edu/ 0 ՜.+,D՜.+,\    On-screen ShowWVUX %Times New Roman Garamond WingdingsArialComic Sans MSSymbolStreamBlank PresentationSlide 1Slide 2Slide 3Slide 4Slide 5Slide 6Slide 7Slide 8Slide 9 Slide 10 Slide 11 Slide 12 Slide 13 Slide 14 Slide 15 Slide 16 Slide 17 Slide 18 Slide 19 Slide 20 Slide 21 Slide 22 Slide 23 Slide 24 Slide 25 Slide 26 Slide 27 Slide 28 Slide 29  Fonts UsedDesign Template Slide Titles 8@ _PID_HLINKSAtmailto:murali@cs.clemson.edu(_XMurali SitaramanMurali Sitaraman)WU O gW&! !#$& 0AA 3@T! g4dddd 0ppp@ R ʚ;l8ʚ;<4!d!d l 0 <4dddd l 0 h___PPT2001D<4X0___PPT10 2___PPT9/ 0? %,r[G7GXwRoot EntrydO) γs@Current UserMSummaryInformation(UPowerPoint Document(X mailto:murali@cs.clemson.edu'_XGary T. LeavensGary T. Leavensn