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

a vòng lp [6] [7]. Xét th tc Increment trong ví 
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 hoá 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 hoá 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 hoá v t, mà không phi xét duyt toàn b các trng thái chi 
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 ngoà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 ngoà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 
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). Ngoà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 hoàn 
 toà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 thoá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 thoá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 
thoát và kh ñt và hoàn toà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 thoá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. Ngoà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, 
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 hoá 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 hoá 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 toá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; 
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). Ngoà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 hoá 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. 
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