Dựa trên đồ thị chương trình phân tích tính khả đạt của chương trình

Nội dung text: Dựa trên đồ thị chương trình phân tích tính khả đạt của chương trình

1. TẠP CHÍ KHOA HỌC −−− SỐ 8/2016 35 DỰA TRÊN ĐỒ THỊ CHƯƠNG TRÌNH PHÂN TÍCH TÍNH KHẢ ĐẠT CỦA CHƯƠNG TRÌNH Nguyn Đc Giang 1, Nguyn Văn Trãi, Đinh Quang Đt Vin Cơng ngh Thơng tin, Vin Hàn lâm Khoa hc và Cơng ngh Vit Nam Tĩm tttttt: ng dng kĩ thut tru tưng hố trong phân tích chương trình (program analysis) giúp m rng phm vi x lí ti các h thng cĩ khơng gian trng thái ln. Các kĩ thut tru tưng đang đưc s dng ngày càng nhiu trong phân tích phát hin li chương trình. Quá trình phân tích phát hin li mt chương trình thưng gn cht vi vic xác đnh tính kh đt (reachability) ca chương trình đĩ. Nu tính kh đt đưc chng minh là đúng trên mơ hình tru tưng, là xp x ca chương trình, thì nĩ cũng đúng trong chương trình thc do tính bo tồn ca phép tru tưng hố. Tuy nhiên, s dng các kĩ thut tru tưng đơi khi làm mt đi tính chính xác trong phân tích tính kh đt do mt s trng thái đã b b qua, đc bit khi cĩ s xut hin ca các vịng lp. Mt s gii pháp hin thi gii quyt vn đ này bng cách s dng các tp b chn dưi và các hàm xp hng (ranking function). Gii pháp ca chúng tơi gii quyt vn đ theo mt cách tip cn khác, khơng s dng các tp b chn dưi và hàm xp hng. Thay vào đĩ, chúng tơi da trên vic kim tra các điu kin trên đ th chương trình (program graph) ng vi h thng thc, các điu kin này đưc kim tra t đng đi vi mơ hình tru tưng. TTTT khố: Đ th chương trình, tính kh đt, hàm xp hng, kim chng mơ hình 1. GII THIU Hin nay, trong bi cnh phát trin nhanh chĩng ca lĩnh vc cơng ngh thơng tin (CNTT), các h thng phn mm tr lên ph bin và cĩ tm nh hưng quan trng ti nhiu hot đng kinh t xã hi. Mc dù đưc s dng ph bin, cĩ mt thc t là các h thng phn mm thưng xuyên mc các li nghiêm trng trong c thit k và cài đt. Nhng li này tr thành mc tiêu ca các cuc tn cơng phá hoi, đt sinh mng và tài sn ca ngưi dân và xã hi dưi nhiu him ho. Thng kê cho thy hu ht các h thng phn mm hin nay đu khơng đưc kim tra, hoc đưc kim tra khơng đy đ trưc khi đưa vào s dng. Lí do chính là do vic s dng các kĩ thut kim tra khơng hình thc (informal methods) như kim th (testing) hoc tái duyt mã (code review). Các kĩ thut này ch kim tra mt s hn ch các trưng hp 1 Nhn bài ngày 23.8.2016; gi phn bin và duyt đăng ngày 15.9.2016 Liên h tác gi: Nguyn Đc Giang; Email: ndgiang@ioit.ac.vn
2. 36 TRƯỜNG ĐẠI HỌC THỦ ĐƠ H NỘI thc thi, và do đĩ khơng th khng đnh đưc tính đúng ca chương trình. Tuy nhiên, do tính d ng dng, min ng dng rng và chi phí hp lí mà các kĩ thut này đang đưc s dng rng rãi cho đa s các h thng khơng địi hi tính an tồn quá cao. Ngưc li, các phương pháp hình thc (formal methods) như kim chng mơ hình (model checking) [3], din gii tru tưng (abstract interpretation) [1], chng minh đnh lí (theorem prover) [11] li tp trung vào các h thng quan trng, cn đm bo hot đng đúng đn, an tồnvà chp nhn chi phí phát trin ln. Các phương pháp hình thc thưng tin hành phân tích h thng dưi các lp lun cht ch ca tốn hc, và kim tra tồn b các kh năng thc thi cĩ th đ khng đnh đưc tính đúng ca chương trình. Nhìn chung, các phương pháp hình thc thưng đưc thc thi bng cách xây dng mt mơ hình tốn hc ca h thng, sau đĩ các tính cht cn kim tra đưc xác minh trên mơ hình tốn hc này. Mt trong nhng mơ hình tốn hc ph bin là h dch chuyn trng thái, h dch chuyn trng thái là đ th mơ t dch chuyn gia các trng thái ca chương trình dc theo tt c các thc thi cĩ th [3]. Thêm na, đa s các phân tích trên chương trình thưng liên quan cht ch ti vic xác đnh tính kh đt ca chương trình đĩ. Xác đnh tính kh đt trên mơ hình dch chuyn ca các h thng cĩ khơng gian trng thái ln thưng tn nhiu chi phí, do đĩ ngưi ta phi s dng thêm các kĩ thut tru tưng. Tính kh đt khi đưc chng minh trên mơ hình tru tưng đng nghĩa vi vic nĩ cũng đưc tho mãn trên mơ hình c th, do tính bo tồn ca phép tru tưng hố [5]. Tuy nhiên, phép tru tưng đơi khi làm mt đi tính chính xác khi cĩ s xut hin ca vịng lp, điu này nh hưng trc tip ti kt qu xác đnh tính kh đt, quá trình phân tích tính kh đt trên mơ hình tru tưng đã b qua các trng thái chi tit mà chương trình ti đưc thơng qua vịng lp. Trong nhiu trưng hp, h thng là ln, tuy nhiên khơng gian trng thái vn hu hn. Mc tiêu ca bài báo nhm đưa ra gii pháp đ gii quyt vn đ phân tích tính kh đt trong điu kin như vy, thơng qua vic s dng mt mơ hình tru tưng hố v tđ gim bt chi phí tính tốn nhưng khơng làm mt đi tính chính xác khi cĩ s xut hin ca vịng lp, hoc li gi đ quy. 2. NN TNG 2.1. Tính kh đt 2.1.1. H dch chuyn trng thái a. Khái nim Trong khoa hc máy tính h dch chuyn trng thái thưng đưc s dng như mt mơ hình mơ t hành vi ca h thng. V cơ bn h dch chuyn trng thái là mt đ th cĩ
3. TẠP CHÍ KHOA HỌC −−− SỐ 8/2016 37 hưng, các nút biu din trng thái ca h thng, các cnh mơ hình s dch chuyn trng thái. Mt trng thái miêu t các thơng tin v h thng ti mt thi đim nht đnh trong chui các hành vi ca h thng đĩ. Thơng thưng, trng thái trong chương trình máy tính tun t th hin qua giá tr hin thi ca tt c các bin trong chương trình và con đm chương trình tr ti lnh tip theo s đưc thc hin. Các dch chuyn quy đnh làm th nào đ h thng cĩ th chuyn t mt trng thái này sang mt trng thái khác. Trong các chương trình tun t, mt dch chuyn thưng xy ra khi thc thi mt đon mã làm thay đi giá tr các bin và con đm chương trình. H dch chuyn trng thái 3 (Transition System TS) là mt b ( S, →, I ) trong đĩ: • S là tp các trng thái; • → ⊆ S × S là tp quan h dch chuyn; • I ⊆ S là tp trng thái khi đu. Hot đng ca h dch chuyn cĩ th mơ t như sau. H dch chuyn bt đu vi mt trong các trng thái s0∈ I và bin đi theo các quan h dch chuyn →. Nghĩa là, nu s là trng thái hin thi, thì mt dch chuyn (s → s′) bt đu t trng thái s đưc la chn khơng đơn đnh và thc hin. H thng chuyn t trng thái s ti trng thái s′. Quá trình này tip tc lp li vi trng thái s′ và kt thúc khi gp mt trng thái mong đi hoc khơng tn ti dch chuyn nào tip theo. Trong trưng hp ti mt trng thái cĩ nhiu dch chuyn cĩ th la chn hoc cĩ nhiu trng thái khi đu thì vic la chn dch chuyn và mt trong các trng thái khi đu là khơng đơn đnh. Cho mt trng thái c ∈ S . Kí hiu • successor s(c) là tp các trng thái k tip ca c: s(c) = {c’ ∈ S | c → c’}; • predecessor p(c) là tp các trng thái lin k trưc ca c: p(c) = {c’ ∈ S | c’→ c}; • c →∗ c’ : trng thái c’ là ti đưc (kh đt) t c thơng qua tp dch chuyn → Mt h dch chuyn trng thái TS đưc gi là đơn đnh (deterministic) nu mi trng thái ch cĩ mt trng thái k tip duy nht. Mt TS là đơn đnh nghch (reverse deterministic) nu mi trng thái ch cĩ mt phn t lin k trưc duy nht. Ví d: Xét ví d 1 v phương thc Increment như sau: voidincrement (int n) { int x:=0;
4. 38 TRƯỜNG ĐẠI HỌC THỦ ĐƠ H NỘI while (x < n) do x:=x+1; while (x < 2n) do x:=x+2; while (x < 3n) do x:=x+3; printf("reached"); } Gi s trng thái ca chương trình đưc xây dng da trên tp giá tr cĩ th ca bin x thì h dch chuyn trng tháica phương thc Increment trên đưc xây dng như hình 1. Hình 1. H dch chuyn ca th tc Increment H dch chuyn trng thái trong hình 1 mơ t quá trình thay đi trng thái chương trình thơng qua giá tr ca bin x. Lúc đu khi khi to chương trình x đưc gán giá tr bng 0. Sau vịng lp th nht x đt ti giá tr n, thốt khi vịng lp th nht, giá tr n ca bin x đưc coi là giá tr khi to vi vịng lp th 2. Tương t như th, x đt đn giá tr 3n và thốt khi vịng lp cui cùng và chương trình thc thi lnh printf ("reached") đ in ra chui " reached ". 2.1.2. Tính kh đt (Reachability) Cho h dch chuyn TS = (S, →, I) . Mt trng thái s ∈ S đưc gi là kh đt trong TS nu tn ti mt dãy dch chuyn trng thái xut phát t mt trng thái khi to s0∈ I , cĩ đ dài hu hn như sau: s0 → s 1 → s 2 → s n1→ s n = s Trong ví d 1 v phương thc Increment trên, mt minh ho v tính kh đt là xác đnh xem liu chương trình cĩ thc s đt ti trng thái chui " reached " đưc in ra hay khơng, đng nghĩa vi vic chương trình đt ti trng thái lnh printf ("reached") đưc thc thi. Trên h dch chuyn trng thái d thy điu này đng nghĩa vi tính kh đt ca trng thái "x = 3n" , nu trng thái này đt đn, chc chn lnh printf ("reached") s đưc thc thi.
5. TẠP CHÍ KHOA HỌC −−− SỐ 8/2016 39 2.2. Tru tưng hố v t Các kim tra da trên h dch chuyn ca h thng thưng xuyên gp phi vn đ bùng n khơng gian trng thái do thc t phc tp ca chương trình và min giá tr ca bin ln. Tru tưng hố v t (predicate abstraction 5) trong khong thi gian gn đây ni lên là mt kĩ thut đy ha hn giúp gii quyt bài tốn khơng gian trng thái ln. Phương pháp tru tưng hố này làm gim kích c ca mơ hình bng cách xố b nhng chi tit dư tha, ch tp trung theo các d liu cn thit. Ý tưng ca phương pháp tru tưng hố v t là s dng các v t đ đi din cho các khong, các b d liu, hoc mt s các trng thái c th cùng tho mãn mt v t. Mt ví d minh ho s dng tru tưng hố v t cho mơ hình ca chương trình cĩ các trng thái đưc biu din thơng qua giá tr ca hai bin x,y như hình 2 và hình 3. Hình 2. Mơ hình chi tit (ví d 1) S dng hai v t p1 và p2 như sau đ tin hành tru tưng hố: • p1 ⇔ x > y • p2 ⇔ y = 0 Mơ hình chi tit trong hình 2 đưc tru tưng hố thành mơ hình như trong hình 3. Hình 3. Mơ hình sau khi tru tưng hố theo v t p1, p 2 (ví d 1) Cp trng thái (x=2; y=0) và (x=1; y=0) tho mãn hai thuc tính x>y và y=0 do đĩ cp hai trng thái này tho mãn p1 và p2. Trng thái (x=2; y=1) tho mãn thuc tính x>y nhưng khơng tho mãn trng thái y=0 nên trng thái này tho mãn p1 và khơng tho mãn
6. 40 TRƯỜNG ĐẠI HỌC THỦ ĐƠ H NỘI p2 (¬p 2). Tương t như vy vi các trng thái cịn li. D thy s lưng trng thái trên mơ hình tru tưng đưc gim thiu so vi s trng thái trên mơ hình chi tit, đng thi thơng tin cũng đưc lưc b bt tính chi tit sau khi các trng thái đưc đi din bi các giá tr ca các v t tru tưng. Mt cách hình thc, cĩ th đnh nghĩa tru tưng hố v t như sau [5]: Đt Φ = {θ1, θ2, , θn} là tp các v t trên tp X các bin ca chương trình, c là mt trng thái ca chương trình, ϕ là mt cơng thc logic, kí hiu c ⊨ ϕ tc là cơng thc ϕ là đúng (cĩ giá tr true ) trng thái c. Vi tp a ⊆ Φ và mt trng thái c, ta nĩi rng c tho mãn a khi và ch chi c ⊨∧Φi ∈ a ϕi. Trong tru tưng hố v t, nhiu trng thái chi tit đưc kt hp vào trong mt trng thái tru tưng. Trng thái tru tưng là trng thái đưc đnh nghĩa bi mt tp con ca tp các v t. Do đĩ, mt trng thái tru tưng đưc cho bi mt tp hp các v t a ⊆ Φ. Đơi khi a đưc biu din dưi dng mt cơng thc, là hi ca các v t trong a. Ví d, nu a = {(x ≥ y), (0 ≤ x < n)} thì a cũng đưc biu din bi cơng thc (x ≥ y) ∧ (0 ≤ x < n) . Kí hiu γ(a) đ ch tp hp các trng thái chi tit ng vi trng thái tru tưng a, tc là tt c các trng thái c tho mãn a, γ(a) = {c | c ⊨ a} . 2.3. Các dch chuyn trên mơ hình tru tưng Cho mt h dch chuyn trng thái TS và tp các v t tru tưng Φ. Lí thuyt tru tưng hố v t 4 ch ra trong h dch chuyn tru tưng s bao gm 3 loi quan h dch chuyn cĩ th gia hai trng thái tru tưng a và a’(a, a ’ ⊆Φ). • may(a, a ’) nu tn ti mt trng thái c ∈ γ(a) và c ’ ∈ γ(a ’), sao cho c → c ’ • must +(a, a ’) nu và ch nu vi mi c ∈ γ(a) , tn ti c’∈ γ(a’), sao cho c → c ’ • must (a, a ’) nu và ch nu vi mi c’∈ γ(a ’), tn ti c∈ γ(a) , sao cho c → c ’ Theo lí thuyt tru tưng hố v t các dch chuyn must (+,) đĩng vi tính bc cu, và cĩ th s dng đ chng minh tính kh đt trong các h thng. Nu cĩ mt chui các dch chuyn must + liên tip t a đn a’ (kí hiu bi must +* (a, a ’)) thì vi mi c ∈ γ(a), tn ti c’∈ γ(a’), mà c →∗ c ’. Nu cĩ mt chui các dch chuyn must liên tip t a đn a’ (đưc kí hiu bi must *(a, a ’)) thì vi mi c’∈ γ(a’), tn ti c ∈ γ(a), mà c →∗ c ’. Ngưc li các quan h dch chuyn may khơng đĩngvi tính bc cu. D thy, ví d trưng hp cĩ may (a, a ’), may (a’, a ’’ ), nhưng vi mi c∈ a và c ’’ ∈ a’’ khơng th khng đnh c →∗ c ’’ .
7. TẠP CHÍ KHOA HỌC −−− SỐ 8/2016 41 2.4. Tin điu kin yu nht và hu điu kin mnh nht Trong nhiu ng dng ca tru tưng hố v t, tp v t tru tưng Φ bao gm mt v t biu din con đm chương trình (program counter). Do đĩ, mi trng thái tru tưng s liên quan cht ch đn mt v trí ca chương trình, vì vy đng nghĩa nĩ cũng liên quan đn mt câu lnh. Cho mt câu lnh s và mt v t e trên tp X các bin ca chương trình, tin điu kin yu nht (weakest precondition) WP(s, e) và hu điu kin mnh nht (strongest postcondition) SP(s, e) đưc đnh nghĩa như sau [5]: • Nu s đưc thc thi t mt trng thái tho mãn WP(s, e) thì chương trình s chuyn đn mt trng thái tho mãn e, và WP(s, e) là v t yu nht đm bo điu này. • Nu s đưc thc thi t mt trng thái tho mãn ethì chương trình s chuyn đn mt trng thái tho mãn SP( s, e), và SP( s, e) là v t mnh nht tho mãn điu này. Ví d, trong th tc Increment ví d 1, chúng ta cĩ WP(x: = x +2, n ≤ x ≤ 2n) = n ≤ x +2 < 2n, SP(x: = x +2, n ≤ x < 2n) = n+2 ≤ x < 2n+2. Các dch chuyn must (+,) cĩ th đưc tính tốn t đng s dng các tin điu kin yu nht và hu điu kin mnh nht. Thc t, câu lnh s thc thi to ra dch chuyn must +(a, a ’) khi và ch khi a ⇒ WP(s,a ’), và to ra dch chuyn must (a, a ’) khi và ch khi a’ ⇒ SP(s,a) . Đơi khi ngưi ta cũng s dng khái nim v t tin điu kin (prepredicate). Cho mt câu lnh s và mt v t e, nu s đưc thc thi t mt trng thái tho mãn pre(s, e) thì chương trình s chuyn ti mt trng thái tho mãn e. D thy, pre(s, e) = ¬ WP(s, ¬e). 3. MT PHƯƠNG PHÁP TRU TƯNG HỐ Đ PHÂN TÍCH TÍNH KH ĐT 3.1. Mc tiêu Tru tưng hố v t đưc s dng giúp phân tích nhng chương trình cĩ khơng gian trng thái ln. Phương pháp tru tưng này rt hu ích trong vic chng minh các tính cht ca chương trình nhưng cĩ nhiu hn ch trong vic xác đnh li [5]. Mt trong nhng lí do chính là vic phân tích phát hin li ph thuc rt nhiu vào xác đnh tính kh đt, tuy nhiên phân tích tính kh đt khi đã ng dng tru tưng hố v t li b qua nhiu trng thái ca h thng khi cĩ s xut hin ca vịng lp [6] [7]. Xét th tc Increment trong ví
8. 42 TRƯỜNG ĐẠI HỌC THỦ ĐƠ H NỘI d trên, th tc này đơn gin là tăng giá tr ca bin x, và d dàng đ thy rng giá tr ca x s đt đn 3n và lnh printf ("reached") s đưc thc thi. Tuy nhiên, hu ht các phương pháp phân tích s sinh ra mt v t cho mi vịng lp, dn ti bùng n khơng gian trng thái và do đĩ nhanh chĩng vưt quá kh năng x lí ca máy tính. Xét th tc Increment trong ví d 1 và h dch chuyn tru tưng ca th tc này theo các v t {0≤x<n,n≤x<2n,2n≤x<3n,3n≤x} đưc minh ho trong hình. Hình 4. H dch chuyn tru tưng ca th tc Increment Mt cách chi tit, hình 1 và hình 4, biu din khơng gian trng thái ca th tc Increment và mơ hình tru tưng hố theo b các v t {0≤x<n, n≤x<2n, 2n≤x<3n, 3n≤x} , qua phép tru tưng v t, các quan h dch chuyn tr thành may và khơng đĩng vi phép bc cu, do đĩ khơng th da trên mơ hình tru tưng đ kt lun rng, mt trng thái c th thuc a3 là ti đưc t mt trng thái c th thuc a0. Nĩi cách khác, trong h dch chuyn tru tưng, tt c các dch chuyn đu mang tính " cĩ th". Mi trng thái chi tit – trong a3 đu cĩ mt trng thái lin trưc trong a2, vì vy ta cĩ must (a 2, a 3). Tt c các quan h dch chuyn cịn li trong mơ hình tru tưng đu là các dch chuyn may . Do đĩ khơng th kt lun rng trng thái in ra chui " reached " là ti đưc t trng thái khi to. Mc tiêu bài báo mun trình bày là cách tip cn đ xác đnh tính kh đt trong trưng hp như vy mà khơng cn tinh chnh li mơ hình tru tưng đ b sung các trng thái ti đưc qua vịng lp. Chng minh tính kh đt khi xut hin các vịng lp hin nay là mt thách thc ln đi vi tru tưng hố v t và phân tích chương trình. Gn đây đã cĩ nhng tin b đáng k trong chng minh t đng tính kt thúc ca chương trình [8], [9]. Các tin b này cĩ ý nghĩa ln trong vic xác đnh tính kh đt. Ý tưng chính trong các chng minh này là s dng các hàm th hng và tp b chn dưi. Tuy nhiên, kĩ thut này yêu cu sinh ra các hàm th hng và thưng khơng phù hp đ chng minh tn ti mt đưng dn ti đưc mt trng thái c th trong h thng khơng đơn đnh. Trong nhiu trưng hp (đc bit, trong tt c các h thng phn mm thc t), các h thng thưng rt ln nhưng vn cĩ hu hn trng thái. Mc tiêu ca bài báo là nhm gii quyt trong nhng trưng hp như vy vn cĩ kh năng phân tích tính kh đt ca h thng bng phương pháp tru tưng hố v t, mà khơng phi xét duyt tồn b các trng thái chi
9. TẠP CHÍ KHOA HỌC −−− SỐ 8/2016 43 tit trong các vịng lp. Phương thc trong bài báo s dng ti các điu kin da trên cu trúc đ th chương trình (program graph) tương ng vi h thng chi tit và các điu kin này cĩ th cho phép kim tra t đng. 3.2. Gii pháp Như đã trình bày phn trưc, các dch chuyn may khơng đưc đĩng dưi tính bc cu, do đĩ các phương pháp tru tưng khơng th đi phĩ vi tính kh đt ca chương trình cĩ vịng lp. Trong phn này chúng tơi s mơ t phương pháp đ đi phĩ vi vịng lp. Đnh nghĩa mt entry port 4 ca mt trng thái tru tưng a là mt v t easao cho γ(e a) ⊆ γ(a) và vi mi ce∈ γ(e a),c e là khi to hoc p(c e) \ γ(a)≠∅. Tc là mi trng thái c th ce đưc th hin bi entry port e a bên trong a và ce là trng thái khi to hoc là mt vài trng thái trưc ca ce nm ngồi a. Đnh nghĩa mt exit port 4 ca mt trng thái tru tưng a là mt v t xa sao cho γ(x a) ⊆ γ(a) và vi mi cx∈ γ(x a),s(c x)\ γ(a)≠∅. Tc là mi trng thái c th cx đưc th hin bi exit port xa trong a và mt vài trng thái k tip ca cx nm ngồi a. Đnh lí 1: Xét mt trng thái tru tưng a, ly e a và x a là entry và exit port ca a sao cho tt c nhng điu kin sau đưc tho mãn. 1. γ(a) là hu hn; 2. Vi mi c ∈ γ(a ⋀ ¬x a), chúng ta cĩ |s(c) ∩ γ(a)| ≤ 1,tc là mi trng thái chi tit trong γ(a ⋀ ¬x a) cĩ ít nht mt trng thái k tip trong γ(a); − 3. must (a ⋀ ¬x a, a ⋀ ¬e a),tc là mi trng thái chi tit trong γ(a ⋀ ¬e a) cĩ trng thái lin trưc trong γ(a ⋀ ¬x a). −* Thì must (e a,x a),tc là vi mi c’ ∈ γ(x a), tn ti c ∈ γ(e a) sao cho c→*c’. Chú ý rng điu kin 1 và 3 cĩ nghĩa rng ea khơng th là rng (tr khi xa là rng, trưng hp này chng minh d dàng) Chng minh đnh lí 1: Chng minh đnh lí 1 đưc da trên vic xây dng mt đ th cĩ hưng khơng chu trình DAG trong đĩ tt c các trng thái cĩ th ti đưc t đnh ngun. Tính hu hn ca γ(a) cĩ nghĩa rng đnh ngun ca DAG đưc cha trong γ(e a). −∗ Gi s rng γ(e a) khơng rng, ngưc li d dàng chng minh must (e a, x a). Xét đ th cĩ hưng khơng chu trình G = (V,E) , cho source (G) ={c ∈ V | ∀c’∈ V, ¬E(c ’, c)} là tp các đnh khơng cĩ đnh k trưc trong G. Xây dng mt chui DAGs: G 0, G 1, sao cho
10. 44 TRƯỜNG ĐẠI HỌC THỦ ĐƠ H NỘI vi mi k ≥ 0 , DAG G k = tho mãn γ(x a) ⊆ V k⊆ γ(a) và mi trng thái trong cĩ th ti đưc t trng thái nào đĩ trong source(G k). Ngồi ra, vi mi k ≥ 0 , hoc source (G k) ⊆ γ(e a) hoc cĩ th xây dng mt DAG Gk+1 tho mãn 2 tính cht trên và cha hồn tồn Gk. Do γ(a) là hu hn [điu kin 1 ca đnh lí], t đĩ cĩ k ≤ |γ(a)| mà source (G k) ⊆ γ(e a). Lưu ý rng vì Gk là đ th con ca h thng chi tit, tính kh đt tương ng vi * must (source(G k), V k). Vì th, nu tn ti DAG Gk tho mãn tt c ba thuc tính, thì * must (e a, x a). Xác đnh Gk bng phương pháp quy np theo k, là chiu cao ca DAG. Da vào đĩ, cho G0 = vi V0 = γ(x a) và E0 = ∅. D thy G 0 tho mãn c hai thuc tính thốt và kh đt như trên. Đc bit, do E0 = ∅, ta cĩ source(G k) = V 0, do tính kh đt tho mãn đi vi đưng rng. Lưu ý rng vì γ(x a) khơng rng, vì th cĩ V0 và source(G 0). Vi bưc quy np, cho k ≥ 0 sao cho Gk tho mãn c hai thuc tính thốt và kh đt và khơng tho mãn thuc tính vào. Ta cĩ th xây dng mt DAG Gk+1 tho mãn thuc tính thốt và kh đt và hồn tồn cha Gk. Ly Sk = source(G k)\γ(e a). Đ ý rng t Gk khơng tho mãn thuc tính đu vào và − source(G k) khơng rng, thì ta cĩ tp Sk cũng khơng rng. Do must (a ∧¬x a, a ∧ ¬e a) (điu kin 3 ca đnh lí) và Sk ∩γ(e a) = ∅ (theo đnh nghĩa ca Sk), mi trng thái trong Sk cĩ mt trng thái lin k trưc trong γ(a ∧¬x a). Ly V’ k = {p(c) ∩γ(a ∧¬x a) | c ∈ S k } ,(V’ k ≠ 0) . Đt Vk+1 = V k∪ V’ k, và đt Ek+1 = E k∪ { | c ∈ S k&& c’ ∈ p(c) ∩ γ(a ∧¬x a)} . Do đĩ, Gk+1 thêm vào các trng thái Gk trong γ(a ∧¬x a) cĩ mt dch chuyn ti các trng thái trong source(G k)\γ(e a), và cũng thêm vào các dch chuyn t các trng thái đĩ ti các trng thái trong source(G k)\γ(e a). T Vk⊆Vk+1 và t gi thit quy np, thì γ(x a) ⊆ V k+1 , do vy Gk+1 tho mãn vi các thuc tính thốt. T gi thit quy np, Gk là mt DAG, thì Gk+1 cũng là mt DAG. Tht vy, các đnh mã đã thêm vào Gk là các đnh t V’ k ti Vk. Ngồi ra, t V’ k≠∅, d dàng nhn thy rng nu Vk và V’ k là tách ri thì Vk+1 ch cha đúng Vk. Vi trưng hp k=0 , chúng ta cĩ V0 = γ(x a). Do V’ k cha ch các trng thái trong γ(a ∧¬x a), rõ ràng rng V0∩ V’ 0 = ∅. Vi trưng hp k>0 , gi s ngưc li rng tn ti mt c ∈ V’ k∩ V k. Do V’ k và γ(x a) là tách ri, nên rõ ràng rng c ∈ V k, tc là cĩ mt j, 1 ≤ j < k sao cho c ∈ V’ j. Do đĩ, cĩ mt c’ ∈ s(c) ∩ γ(a) hay c’ ∈ γ(a) là nút k tip ca c. Do vy, c’ ∈ S k. Nhưng c’ là lin k trưc ca c trong Gk, c’ khơng nm trong source(G k). Nên c’ ∉ Sk. Điu này mâu thun. Nên Gk+1 tho mãn tính kh đt. Theo đnh nghĩa, source(G k+1 ) = V’ k,
11. TẠP CHÍ KHOA HỌC −−− SỐ 8/2016 45 nhưng theo gi thit quy np, tt c các trng thái trong Vk là ti đưc t mt vài trng thái trong source(G k). T mi trng thái trong source(G k) là k tip ca mt vài trng thái trong V’ k, dn đn rng mi trng thái trong Vk+1 là ti đưc t mt vài trng thái trong source(G k+1 ). Tương t, cĩ đnh lí 2 như sau: Đnh lí 2: Xét mt trng thái tru tưng a, ly e a và x a là entry và exit port ca a sao cho tt c nhng điu kin sau đu tho mãn. 1. γ(a) là hu hn; 2. Vi mi c ∈ γ(a ⋀ ¬e a), cĩ |p(c) ∩ γ(a)| ≤ 1, tc là mi trng thái chi tit trong γ(a ⋀ ¬e a) cĩ ít nht mt trng thái k tip trong γ(a); + 3. must (a ⋀ ¬x a, a ⋀ ¬e a) , tc là mi trng thái chi tit trong γ(a ⋀ ¬x a) đu cĩ trng thái lin trưc trong γ(a ⋀ ¬e a). +* Thì must (e a,x a),tc là vi mi c ∈ γ(e a), tn ti c’ ∈ γ(x a) sao cho c→*c’. Chng minh đnh lí 2: Chng minh tương t đnh lí 1 Đnh lí 3: Cho a1 và a2 là các trng thái tru tưng vi entry port ln lưt là ea1 và ea2 , và exit port ln lưt là xa1 và xa2 . Gi s rng vi mi i ∈ {1,2} , ta cĩ γ(a i) là hu hn, vi − mi c ∈ γ(a i⋀ ¬x ai )ta cĩ |s(c) ∩ γ(a i)| ≤ 1 , và ta cũng cĩ must (a i⋀ ¬x ai, ai⋀ ¬e ai) , −* −* must (x a1, ea2 ). Thì must (e a1, xa2 ). Chng minh đnh lí 3: Theo điu kin ca đnh lí, các điu kin ca đnh lí 1 đưc tho −* mãn vi a1 và a2cùng nhng entry port , exit port chúng. Do đĩ, ta cĩ must (e a1 ,x a1 ) và −* −* must (e a2 ,x a2 ). T đĩ must (x a1 ,e a2 ) tho mãn do tính bc cu ca các quan h dch chuyn kiu must −. Tương t, các dch chuyn must + cũng cĩ tính bc cu, áp dng đnh lí 2 ta cĩ điu phi chng minh. 3.3. ng dng Phương pháp tru tưng hố mơ hình dch chuyn trng thái theo v t đã trình bày cĩ th đưc ng dng trong kim chng mơ hình 10, hoc phân tích chương trình tĩnh đ xác đnh tính kh đt. Quá trình tru tưng, sinh v t cĩ th t đng hố bng cách kt hp tương ng mt trng thái tru tưng vi mt lnh thc thi và các trng thái chi tit phát sinh khi thc thi lnh đĩ. Thc hin chia làm 2 giai đon chính: • Tính tốn các entry port và exit port tương ng vi các trng thái tru tưng dc theo đưng thc thi;
12. 46 TRƯỜNG ĐẠI HỌC THỦ ĐƠ H NỘI • Kim tra các điu kin tương ng vi gii pháp 1 hoc 2, sau đĩ kt lun. Ví d: Xem xét li ví d v th tc Increment và tru tưng ca th tc này . Áp dng phương pháp tip cn trên ca bài báo cho tru tưng ca phương thc Increment đưc minh ho như 0. Hình 5. Phân tích tính kh đt trên tru tưng ca th tc Increment Trng thái tru tưng a0: 0 ≤ x ≤ n cĩ entry port x=0 và exit port x = n1. Các điu kin trong đnh lí 1 đưc tho mãn trong a0 vi entry port và exit port này do: 1. n là hu hn do đĩ γ(a 0) là hu hn. 2. Do th tc thc hin theo cơ ch đơn đnh, nên mi trng thái chi tit ch cĩ mt trng thái k tip duy nht. 3. Mi trng thái c th tr x=0 cĩ mt nút lin k trưc trong a0. Cĩ th kt lun rng must −* (x=0,x=n1). Vi chng minh tương t, các điu kin đưc tho mãn ti a1 vi entry port là x=n và exit port là 2n2 ≤ x < 2n , và ti a 2 vi entry port là 2n ≤ x ≤ 2n+1 và exit port là 3n3 ≤ x < 3n . T đây ta cĩ th kt lun đưc must −* (x=n,2n 2≤ x < 2n ) và must −* (2n≤ x ≤ 2n+1, 3n3≤x<3n). Ngồi ra, must −(x=n1,x=n), must −(2n 2≤x<2n, 2n≤x≤2n+1) và must −(3n3≤x<3n, 3n<x). Như vy, cĩ th kt lun đưc must −* (x=0,3n≤x) (do tính cht bc cu ca must −). 4. KT LUN Trong bài báo chúng tơi đã trình bày mt phương pháp tru tưng hố theo v t giúp phân tích tính kh đt đi vi các h thng cĩ khơng gian trng thái ln. Kt qu chính ca phương pháp là cĩ th xác đnh chính xác tính kh đt mà khơng phi làm mn mơ hình tru tưng khi xut hin nhiu vịng lp trong h thng. Trong tương lai chúng tơi s d đnh tip tc nghiên cu đ phát trin cơng c kim chng mơ hình t đng da trên ni dung lí thuyt đã nghiên cu.
13. TẠP CHÍ KHOA HỌC −−− SỐ 8/2016 47 TÀI LIU THAM KHO 1. Patrick Cousot, Jer C.Hunsaker (2005), "An informal overview of abstract interpretation", Massachusetts Institute of Technology Department of Aeronautics Astronautics , Course 16.399. 2. Michael I. Schwartzbach, "Lecture Notes on Static Analysis", BRICS, Department of Computer Science University of Aarhus , Denmark. 3. Christel Baier, JoostPieter Katoen (2008), "Principles of Model Checking", The MIT Press . 4. Thomas Ball, Orna Kupferman, Mooly Sagiv (2007), "Leaping loops in the presence of abstraction", Proceeding CAV'07 Proceedings of the 19th International conference on Computer aided verification , pp.491503. 5. Cormac Flanagan, Shaz Qadeer (2002), "Predicate abstraction for software verification", Proceeding POPL '02 Proceedings of the 29th ACM SIGPLANSIGACT symposium on Principles of programming languages , pp.191202. 6. A.R. Bradley, Z. Manna, H. Sipma (2005), "Linear Ranking with Reachability", In Proc. of 17thCAV, LNCS 3576 , pp.491504. 7. Rajeev Alur, Thao Dang, Franjo Ivančić (2006), "Predicate abstraction for reachability analysis of hybrid systems", Journal ACM Transactions on Embedded Computing Systems (TECS) , vol. 5 Issue 1, pp.152199. 8. Byron Cook, Andreas Podelski, Andrey Rybalchenko (2011), "Proving Program Termination", Communications of the ACM , vol. 54 Issue 5, pp.8898. 9. B. Cook, A. Podelski, A. Rybalchenko (2006), "Termination proofs for systems code", In Proc. ACM PLDI , pp.415426. 10. P. Godefroid, R. Jagadeesan (2002), "Automatic abstraction using generalized model checking", In Proc. 14th CAV, LNCS 2404 , pp.137150. 11. Loveland, Donald W (1978), "Automated Theorem Proving: A Logical Basis", Fundamental Studies in Computer Science , Volume 6, NorthHolland Publishing. BASING ON THE GRAPH OF PROGRAM TO ANALYZE THE AVAILABILITY OF THE PROGRAM AbstractAbstract: The application of abstract technique in analytical program helps us expand the scope of the system processor to system of large space. The abstract technique has been using more and more in fault detection analysis programs. The analysis detected that a program error is tied to the determination of the availability of the program. If the availability proved its correction in the abstract model as the approximation of the program, it is also true in the program due to the preservation of abstraction. However, sometimes, the use of the abstract technique also caused the loss of accuracy in analyzing the availability due to a number of states was ignored, especially the appearance of the loop. Some current solutions solve this problem by using the below blocked file and ranking functions. Our solution did not use the below blocked file and ranking functions. Instead, we base on checking the conditions on the graph of program which corresponding with the real system, the conditions are checked automatically with abstract model. KeywordsKeywords: The graph of program, availability, ranking function, model checking