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

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

Nguyꢀn Đꢁc Giang¹, Nguyꢀn Văn Trãi, Đinh Quang Đꢂt

Viꢀn Công nghꢀ Thông tin, Viꢀn Hàn lâm Khoa hꢁc và Công nghꢀ Viꢀt Nam

Tóm tꢂt: ꢃng dꢄng kĩ thuꢅt trꢆu tưꢇng hoá trong phân tích chương trình (program

analysis) giúp mꢈ rꢉng phꢊm vi xꢋ lí tꢌi các hꢀ thꢍng có không gian trꢊng thái lꢌn. Các

kĩ thuꢅt trꢆu tưꢇng ñang ñưꢇc sꢋ dꢄng ngày càng nhiꢎu trong phân tích phát hiꢀn lꢏi

chương trình. Quá trình phân tích phát hiꢀn lꢏi mꢉt chương trình thưꢐng gꢂn chꢑt vꢌi

viꢀc xác ñꢒnh tính khꢓ ñꢊt (reachability) cꢔa chương trình ñó. Nꢕu tính khꢓ ñꢊt ñưꢇc

chꢖng minh là ñúng trên mô hình trꢆu tưꢇng, là xꢗp xꢘ cꢔa chương trình, thì nó cũng

ñúng trong chương trình thꢙc do tính bꢓo toàn cꢔa phép trꢆu tưꢇng hoá. Tuy nhiên, sꢋ

dꢄng các kĩ thuꢅt trꢆu tưꢇng ñôi khi làm mꢗt ñi tính chính xác trong phân tích tính khꢓ

ñꢊt do mꢉt sꢍ trꢊng thái ñã bꢒ bꢚ qua, ñꢑc biꢀt khi có sꢙ xuꢗt hiꢀn cꢔa các vòng lꢑp. Mꢉt

sꢍ giꢓi pháp hiꢀn thꢐi giꢓi quyꢕt vꢗn ñꢎ này bꢛng cách sꢋ dꢄng các tꢅp bꢒ chꢑn dưꢌi và

các hàm xꢕp hꢊng (ranking function). Giꢓi pháp cꢔa chúng tôi giꢓi quyꢕt vꢗn ñꢎ theo mꢉt

cách tiꢕp cꢅn khác, không sꢋ dꢄng các tꢅp bꢒ chꢑn dưꢌi và hàm xꢕp hꢊng. Thay vào ñó,

chúng tôi dꢙa trên viꢀc kiꢜm tra các ñiꢎu kiꢀn trên ñꢝ thꢒ chương trình (program graph)

ꢖng vꢌi hꢀ thꢍng thꢙc, các ñiꢎu kiꢀn này ñưꢇc kiꢜm tra tꢙ ñꢉng ñꢍi vꢌi mô hình trꢆu tưꢇng.

Tꢆ khoá: Đꢝ thꢒ chương trình, tính khꢓ ñꢊt, hàm xꢕp hꢊng, kiꢜm chꢖng mô hình

1. GIꢃI THIꢄU

Hiꢀn nay, trong bꢁi cꢂnh phát triꢃn nhanh chóng cꢄa lĩnh vꢅc công nghꢀ thông tin

(CNTT), các hꢀ thꢁng phꢆn mꢇm trꢈ lên phꢉ biꢊn và có tꢆm ꢂnh hưꢈng quan trꢋng tꢌi

nhiꢇu hoꢍt ñꢎng kinh tꢊ ꢏ xã hꢎi. Mꢐc dù ñưꢑc sꢒ dꢓng phꢉ biꢊn, có mꢎt thꢅc tꢊ là các hꢀ

thꢁng phꢆn mꢇm thưꢔng xuyên mꢕc các lꢖi nghiêm trꢋng trong cꢂ thiꢊt kꢊ và cài ñꢐt.

Nhꢗng lꢖi này trꢈ thành mꢓc tiêu cꢄa các cuꢎc tꢘn công phá hoꢍi, ñꢐt sinh mꢍng và tài sꢂn

cꢄa ngưꢔi dân và xã hꢎi dưꢌi nhiꢇu hiꢃm hoꢍ.

Thꢁng kê cho thꢘy hꢆu hꢊt các hꢀ thꢁng phꢆn mꢇm hiꢀn nay ñꢇu không ñưꢑc kiꢃm tra,

hoꢐc ñưꢑc kiꢃm tra không ñꢆy ñꢄ trưꢌc khi ñưa vào sꢒ dꢓng. Lí do chính là do viꢀc sꢒ

dꢓng các kĩ thuꢙt kiꢃm tra không hình thꢚc (informal methods) như kiꢃm thꢒ (testing) hoꢐc

tái duyꢀt mã (code review). Các kĩ thuꢙt này chꢛ kiꢃm tra mꢎt sꢁ hꢍn chꢊ các trưꢔng hꢑp

1

Nhꢙn bài ngày 23.8.2016; gꢒi phꢂn biꢀn và duyꢀt ñăng ngày 15.9.2016

Liên hꢀ tác giꢂ: Nguyꢜn Đꢚc Giang; Email: [email protected]

36

TRƯỜNG ĐẠI HỌC THỦ ĐÔ Hꢀ NỘI

thꢅc thi, và do ñó không thꢃ khꢝng ñꢞnh ñưꢑc tính ñúng cꢄa chương trình. Tuy nhiên, do

tính dꢜ ꢚng dꢓng, miꢇn ꢚng dꢓng rꢎng và chi phí hꢑp lí mà các kĩ thuꢙt này ñang ñưꢑc sꢒ

dꢓng rꢎng rãi cho ña sꢁ các hꢀ thꢁng không ñòi hꢟi tính an toàn quá cao. Ngưꢑc lꢍi, các

phương pháp hình thꢚc (formal methods) như kiꢃm chꢚng mô hình (model checking) [3],

diꢜn giꢂi trꢠu tưꢑng (abstract interpretation) [1], chꢚng minh ñꢞnh lí (theorem prover) [11]…

lꢍi tꢙp trung vào các hꢀ thꢁng quan trꢋng, cꢆn ñꢂm bꢂo hoꢍt ñꢎng ñúng ñꢕn, an toànvà chꢘp

nhꢙn chi phí phát triꢃn lꢌn. Các phương pháp hình thꢚc thưꢔng tiꢊn hành phân tích hꢀ

thꢁng dưꢌi các lꢙp luꢙn chꢐt chꢡ cꢄa toán hꢋc, và kiꢃm tra toàn bꢎ các khꢂ năng thꢅc thi có

thꢃ ñꢃ khꢝng ñꢞnh ñưꢑc tính ñúng cꢄa chương trình.

Nhìn chung, các phương pháp hình thꢚc thưꢔng ñưꢑc thꢅc thi bꢢng cách xây dꢅng mꢎt

mô hình toán hꢋc cꢄa hꢀ thꢁng, sau ñó các tính chꢘt cꢆn kiꢃm tra ñưꢑc xác minh trên mô

hình toán hꢋc này. Mꢎt trong nhꢗng mô hình toán hꢋc phꢉ biꢊn là hꢀ dꢞch chuyꢃn trꢍng

thái, hꢀ dꢞch chuyꢃn trꢍng thái là ñꢣ thꢞ mô tꢂ dꢞch chuyꢃn giꢗa các trꢍng thái cꢄa chương

trình dꢋc theo tꢘt cꢂ các thꢅc thi có thꢃ [3]. Thêm nꢗa, ña sꢁ các phân tích trên chương

trình thưꢔng liên quan chꢐt chꢡ tꢌi viꢀc xác ñꢞnh tính khꢂ ñꢍt cꢄa chương trình ñó. Xác

ñꢞnh tính khꢂ ñꢍt trên mô hình dꢞch chuyꢃn cꢄa các hꢀ thꢁng có không gian trꢍng thái lꢌn

thưꢔng tꢁn nhiꢇu chi phí, do ñó ngưꢔi ta phꢂi sꢒ dꢓng thêm các kĩ thuꢙt trꢠu tưꢑng. Tính

khꢂ ñꢍt khi ñưꢑc chꢚng minh trên mô hình trꢠu tưꢑng ñꢣng nghĩa vꢌi viꢀc nó cũng ñưꢑc

thoꢂ mãn trên mô hình cꢓ thꢃ, do tính bꢂo toàn cꢄa phép trꢠu tưꢑng hoá [5]. Tuy nhiên,

phép trꢠu tưꢑng ñôi khi làm mꢘt ñi tính chính xác khi có sꢅ xuꢘt hiꢀn cꢄa vòng lꢐp, ñiꢇu

này ꢂnh hưꢈng trꢅc tiꢊp tꢌi kꢊt quꢂ xác ñꢞnh tính khꢂ ñꢍt, quá trình phân tích tính khꢂ ñꢍt

trên mô hình trꢠu tưꢑng ñã bꢟ qua các trꢍng thái chi tiꢊt mà chương trình tꢌi ñưꢑc thông

qua vòng lꢐp.

Trong nhiꢇu trưꢔng hꢑp, hꢀ thꢁng là lꢌn, tuy nhiên không gian trꢍng thái vꢤn hꢗu hꢍn.

Mꢓc tiêu cꢄa bài báo nhꢢm ñưa ra giꢂi pháp ñꢃ giꢂi quyꢊt vꢘn ñꢇ phân tích tính khꢂ ñꢍt

trong ñiꢇu kiꢀn như vꢙy, thông qua viꢀc sꢒ dꢓng mꢎt mô hình trꢠu tưꢑng hoá vꢞ tꢠñꢃ giꢂm

bꢌt chi phí tính toán nhưng không làm mꢘt ñi tính chính xác khi có sꢅ xuꢘt hiꢀn cꢄa vòng

lꢐp, hoꢐc lꢔi gꢋi ñꢀ quy.

2. NꢅN TꢆNG

2.1. Tính khꢇ ñꢂt

2.1.1. Hꢈ dꢉch chuyꢊn trꢂng thái

a. Khái niꢈm

Trong khoa hꢋc máy tính hꢀ dꢞch chuyꢃn trꢍng thái thưꢔng ñưꢑc sꢒ dꢓng như mꢎt mô

hình mô tꢂ hành vi cꢄa hꢀ thꢁng. Vꢇ cơ bꢂn hꢀ dꢞch chuyꢃn trꢍng thái là mꢎt ñꢣ thꢞ có

TẠP CHÍ KHOA HỌC − SỐ 8/2016

37

hưꢌng, các nút biꢃu diꢜn trꢍng thái cꢄa hꢀ thꢁng, các cꢍnh mô hình sꢅ dꢞch chuyꢃn trꢍng

thái. Mꢎt trꢍng thái miêu tꢂ các thông tin vꢇ hꢀ thꢁng tꢍi mꢎt thꢔi ñiꢃm nhꢘt ñꢞnh trong

chuꢖi các hành vi cꢄa hꢀ thꢁng ñó. Thông thưꢔng, trꢍng thái trong chương trình máy tính

tuꢆn tꢅ thꢃ hiꢀn qua giá trꢞ hiꢀn thꢔi cꢄa tꢘt cꢂ các biꢊn trong chương trình và con ñꢊm

chương trình trꢟ tꢌi lꢀnh tiꢊp theo sꢡ ñưꢑc thꢅc hiꢀn. Các dꢞch chuyꢃn quy ñꢞnh làm thꢊ

nào ñꢃ hꢀ thꢁng có thꢃ chuyꢃn tꢠ mꢎt trꢍng thái này sang mꢎt trꢍng thái khác. Trong các

chương trình tuꢆn tꢅ, mꢎt dꢞch chuyꢃn thưꢔng xꢂy ra khi thꢅc thi mꢎt ñoꢍn mã làm thay

ñꢉi giá trꢞ các biꢊn và con ñꢊm chương trình.

Hꢈ dꢉch chuyꢊn trꢂng thái 3 (Transition System ꢏ TS) là mꢎt bꢎ (S, →, I) trong ñó:

•

S là tꢙp các trꢍng thái;

→

⊆

S × S là tꢙp quan hꢀ dꢞch chuyꢃn;

I

⊆

S

là tꢙp trꢍng thái khꢈi ñꢆu.

Hoꢍt ñꢎng cꢄa hꢀ dꢞch chuyꢃn có thꢃ mô tꢂ như sau. Hꢀ dꢞch chuyꢃn bꢕt ñꢆu vꢌi mꢎt

trong các trꢍng thái s₀và biꢊn ñꢉi theo các quan hꢀ dꢞch chuyꢃn →. Nghĩa là, nꢊu s là

trꢍng thái hiꢀn thꢔi, thì mꢎt dꢞch chuyꢃn (s → s′) bꢕt ñꢆu tꢠ trꢍng thái ñưꢑc lꢅa chꢋn

không ñơn ñꢞnh và thꢅc hiꢀn. Hꢀ thꢁng chuyꢃn tꢠ trꢍng thái tꢌi trꢍng thái s′. Quá trình

∈

I

s

này tiꢊp tꢓc lꢐp lꢍi vꢌi trꢍng thái s′ và kꢊt thúc khi gꢐp mꢎt trꢍng thái mong ñꢑi hoꢐc không

tꢣn tꢍi dꢞch chuyꢃn nào tiꢊp theo. Trong trưꢔng hꢑp tꢍi mꢎt trꢍng thái có nhiꢇu dꢞch chuyꢃn

có thꢃ lꢅa chꢋn hoꢐc có nhiꢇu trꢍng thái khꢈi ñꢆu thì viꢀc lꢅa chꢋn dꢞch chuyꢃn và mꢎt

trong các trꢍng thái khꢈi ñꢆu là không ñơn ñꢞnh.

Cho mꢎt trꢍng thái

c

∈

S

. Kí hiꢀu

successor ꢞ s(c) là tꢙp các trꢍng thái kꢊ tiꢊp cꢄa c: s(c) = {c’

predecessor ꢞ p(c) là tꢙp các trꢍng thái liꢇn kꢇ trưꢌc cꢄa c: p(c) = {c’

c → c’: trꢍng thái c’ là tꢌi ñưꢑc (khꢂ ñꢍt) tꢠ c thông qua tꢙp dꢞch chuyꢃn →

•

∈

S | c → c’};

S | c’→ c};

∈

∗

Mꢎt hꢀ dꢞch chuyꢃn trꢍng thái TS ñưꢑc gꢋi là ñơn ñꢞnh (deterministic) nꢊu mꢋi trꢍng

thái chꢛ có mꢎt trꢍng thái kꢊ tiꢊp duy nhꢘt. Mꢎt TS là ñơn ñꢞnh nghꢞch (reverseꢏ

deterministic) nꢊu mꢖi trꢍng thái chꢛ có mꢎt phꢆn tꢒ liꢇn kꢇ trưꢌc duy nhꢘt.

Ví dꢋ: Xét ví dꢓ 1 vꢇ phương thꢚc Increment như sau:

voidincrement (int n)

{

int x:=0;

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ꢒ trꢍng thái cꢄa chương trình ñưꢑc xây dꢅng dꢅa trên tꢙp giá trꢞ có thꢃ cꢄa biꢊn

x

thì hꢀ dꢞch chuyꢃn trꢍng tháicꢄa phương thꢚc Increment trên ñưꢑc xây dꢅng như hình 1.

Hình 1. Hꢀ dꢒch chuyꢜn cꢔa thꢔ tꢄc Increment

Hꢀ dꢞch chuyꢃn trꢍng thái trong hình 1 mô tꢂ quá trình thay ñꢉi trꢍng thái chương trình

thông qua giá trꢞ cꢄa biꢊn . Lúc ñꢆu khi khꢈi tꢍo chương trình ñưꢑc gán giá trꢞ bꢢng

Sau vòng lꢐp thꢚ nhꢘt ñꢍt tꢌi giá trꢞ , thoát khꢟi vòng lꢐp thꢚ nhꢘt, giá trꢞ cꢄa biꢊn

ñưꢑc coi là giá trꢞ khꢈi tꢍo vꢌi vòng lꢐp thꢚ 2. Tương tꢅ như thꢊ, ñꢍt ñꢊn giá trꢞ 3n và

x

0.

x

n

x

thoát khꢟi vòng lꢐp cuꢁi cùng và chương trình thꢅc thi lꢀnh printf ("reached") ñꢃ in ra

chuꢖi "reached".

2.1.2. Tính khꢇ ñꢂt (Reachability)

Cho hꢀ dꢞch chuyꢃn TS = (S, →, I). Mꢎt trꢍng thái

s

∈

S ñưꢑc gꢋi là khꢂ ñꢍt trong TS

nꢊu tꢣn tꢍi mꢎt dãy dꢞch chuyꢃn trꢍng thái xuꢘt phát tꢠ mꢎt trꢍng thái khꢈi tꢍo s₀

∈

I, có ñꢎ

dài hꢗu hꢍn như sau:

s₀→ s₁→ s₂ꢥ ꢥ ꢥ → s_nꢏ1→ s_n= s

Trong ví dꢓ 1 vꢇ phương thꢚc Increment trên, mꢎt minh hoꢍ vꢇ tính khꢂ ñꢍt là xác

ñꢞnh xem liꢀu chương trình có thꢅc sꢅ ñꢍt tꢌi trꢍng thái chuꢖi "reached" ñưꢑc in ra hay

không, ñꢣng nghĩa vꢌi viꢀc chương trình ñꢍt tꢌi trꢍng thái lꢀnh printf ("reached") ñưꢑc

thꢅc thi. Trên hꢀ dꢞch chuyꢃn trꢍng thái dꢜ thꢘy ñiꢇu này ñꢣng nghĩa vꢌi tính khꢂ ñꢍt cꢄa

trꢍng thái "x = 3n", nꢊu trꢍng thái này ñꢍt ñꢊn, chꢕc chꢕn lꢀnh printf ("reached") sꢡ ñưꢑc

thꢅc thi.

TẠP CHÍ KHOA HỌC − SỐ 8/2016

39

2.2. Trꢌu tưꢍng hoá vꢉ tꢌ

Các kiꢃm tra dꢅa trên hꢀ dꢞch chuyꢃn cꢄa hꢀ thꢁng thưꢔng xuyên gꢐp phꢂi vꢘn ñꢇ

bùng nꢉ không gian trꢍng thái do thꢅc tꢊ phꢚc tꢍp cꢄa chương trình và miꢇn giá trꢞ cꢄa

biꢊn lꢌn. Trꢠu tưꢑng hoá vꢞ tꢠ (predicate abstraction 5) trong khoꢂng thꢔi gian gꢆn ñây nꢉi

lên là mꢎt kĩ thuꢙt ñꢆy hꢚa hꢦn giúp giꢂi quyꢊt bài toán không gian trꢍng thái lꢌn. Phương

pháp trꢠu tưꢑng hoá này làm giꢂm kích cꢧ cꢄa mô hình bꢢng cách xoá bꢟ nhꢗng chi tiꢊt dư

thꢠa, chꢛ tꢙp trung theo các dꢗ liꢀu cꢆn thiꢊt. Ý tưꢈng cꢄa phương pháp trꢠu tưꢑng hoá vꢞ

tꢠ là sꢒ dꢓng các vꢞ tꢠ ñꢃ ñꢍi diꢀn cho các khoꢂng, các bꢎ dꢗ liꢀu, hoꢐc mꢎt sꢁ các trꢍng

thái cꢓ thꢃ cùng thoꢂ mãn mꢎt vꢞ tꢠ. Mꢎt ví dꢓ minh hoꢍ sꢒ dꢓng trꢠu tưꢑng hoá vꢞ tꢠ cho

mô hình cꢄa chương trình có các trꢍng thái ñưꢑc biꢃu diꢜn thông qua giá trꢞ cꢄa hai biꢊn

x,y như hình 2 và hình 3.

Hình 2. Mô hình chi tiꢕt (ví dꢄ 1)

Sꢒ dꢓng hai vꢞ tꢠ p₁và p₂như sau ñꢃ tiꢊn hành trꢠu tưꢑng hoá:

•

p_{1 ⇔}x > y

p_{2 ⇔}y = 0

Mô hình chi tiꢊt trong hình 2 ñưꢑc trꢠu tưꢑng hoá thành mô hình như trong hình 3.

Hình 3. Mô hình sau khi trꢆu tưꢇng hoá theo vꢒ tꢆ p₁, p₂(ví dꢄ 1)

Cꢐp trꢍng thái (x=2; y=0) và (x=1; y=0) thoꢂ mãn hai thuꢎc tính x>y và y=0 do ñó

cꢐp hai trꢍng thái này thoꢂ mãn p₁và

p₂. Trꢍng thái (x=2; y=1) thoꢂ mãn thuꢎc tính x>y

nhưng không thoꢂ mãn trꢍng thái y=0 nên trꢍng thái này thoꢂ mãn p₁và không thoꢂ mãn

40

TRƯỜNG ĐẠI HỌC THỦ ĐÔ Hꢀ NỘI

p₂(¬p₂). Tương tꢅ như vꢙy vꢌi các trꢍng thái còn lꢍi. Dꢜ thꢘy sꢁ lưꢑng trꢍng thái trên mô

hình trꢠu tưꢑng ñưꢑc giꢂm thiꢃu so vꢌi sꢁ trꢍng thái trên mô hình chi tiꢊt, ñꢣng thꢔi thông

tin cũng ñưꢑc lưꢑc bꢟ bꢌt tính chi tiꢊt sau khi các trꢍng thái ñưꢑc ñꢍi diꢀn bꢈi các giá trꢞ

cꢄa các vꢞ tꢠ trꢠu tưꢑng.

Mꢎt cách hình thꢚc, có thꢃ ñꢞnh nghĩa trꢠu tưꢑng hoá vꢞ tꢠ như sau [5]: Đꢐt

Φ = {θ₁, θ₂, …, θ_n} là tꢙp các vꢞ tꢠ trên tꢙp

cꢄa chương trình, là mꢎt công thꢚc logic, kí hiꢀu

giá trꢞ true)ꢈ trꢍng thái

và chꢛ chi ⊨∧Φ_i

X

các biꢊn cꢄa chương trình,

⊨ ϕ tꢚc là công thꢚc

và mꢎt trꢍng thái , ta nói rꢢng thoꢂ mãn a

c

là mꢎt trꢍng thái

là ñúng (có

khi

ϕ

c

ϕ

c

. Vꢌi tꢙp

a

⊆

Φ

c

ϕ

.

a

i

Trong trꢠu tưꢑng hoá vꢞ tꢠ, nhiꢇu trꢍng thái chi tiꢊt ñưꢑc kꢊt hꢑp vào trong mꢎt trꢍng

thái trꢠu tưꢑng. Trꢍng thái trꢠu tưꢑng là trꢍng thái ñưꢑc ñꢞnh nghĩa bꢈi mꢎt tꢙp con cꢄa tꢙp

các vꢞ tꢠ. Do ñó, mꢎt trꢍng thái trꢠu tưꢑng ñưꢑc cho bꢈi mꢎt tꢙp hꢑp các vꢞ tꢠ

Đôi khi a ñưꢑc biꢃu diꢜn dưꢌi dꢍng mꢎt công thꢚc, là hꢎi cꢄa các vꢞ tꢠ trong . Ví dꢓ, nꢊu

a = {(x ≥ y), (0 ≤ x < n)} thì a cũng ñưꢑc biꢃu diꢜn bꢈi công thꢚc (x ≥ y) (0 ≤ x < n)

Kí hiꢀu γ(a) ñꢃ chꢛ tꢙp hꢑp các trꢍng thái chi tiꢊt ꢚng vꢌi trꢍng thái trꢠu tưꢑng , tꢚc là tꢘt

cꢂ các trꢍng thái thoꢂ mãn γ(a) = {c | c a}

a

⊆

Φ.

a

∧

.

a

c

a

,

⊨

.

2.3. Các dꢉch chuyꢊn trên mô hình trꢌu tưꢍng

Cho mꢎt hꢀ dꢞch chuyꢃn trꢍng thái TS và tꢙp các vꢞ tꢠ trꢠu tưꢑng

Φ. Lí thuyꢊt trꢠu

tưꢑng hoá vꢞ tꢠ 4 chꢛ ra trong hꢀ dꢞch chuyꢃn trꢠu tưꢑng sꢡ bao gꢣm 3 loꢍi quan hꢀ dꢞch

chuyꢃn có thꢃ giꢗa hai trꢍng thái trꢠu tưꢑng

a

c

và a^’

(

a, a^’

⊆

Φ

).

γ(a^’), sao cho c → c^’

•

may(a, a^’) nꢊu tꢣn tꢍi mꢎt trꢍng thái

must⁺a, a^’) nꢊu và chꢛ nꢊu vꢌi mꢋi

must^ꢞa, a^’) nꢊu và chꢛ nꢊu vꢌi mꢋi c^’

∈

γ(a) và c^’

∈

(

c

∈

γ(a), tꢣn tꢍic^’

γ(a^’), tꢣn tꢍi

∈

γ(a^’), sao cho c → c^’

γ(a), sao cho c → c^’

(

∈

c

∈

Theo lí thuyꢊt trꢠu tưꢑng hoá vꢞ tꢠ các dꢞch chuyꢃn must^(+,ꢞ)ñóng vꢌi tính bꢕc cꢆu, và

có thꢃ sꢒ dꢓng ñꢃ chꢚng minh tính khꢂ ñꢍt trong các hꢀ thꢁng. Nꢊu có mꢎt chuꢖi các dꢞch

chuyꢃn must⁺liên tiꢊp tꢠ

tꢍic^’γ(a^’), màc → c^’. Nꢊu có mꢎt chuꢖi các dꢞch chuyꢃn must^ꢞliên tiꢊp tꢠ

(ñưꢑc kí hiꢀu bꢈi must ^ꢞ*a, a^’)) thì vꢌi mꢋi c^’γ(a^’), tꢣn tꢍi

γ( ), mà c →

lꢍi các quan hꢀ dꢞch chuyꢃn may không ñóngvꢌi tính bꢕc cꢆu. Dꢜ thꢘy, ví dꢓ trưꢔng hꢑp có

may

a, a^’), may a^’, a^’’), nhưng vꢌi mꢋi và c^’’a^’’không thꢃ khꢝng ñꢞnh c → c^’’.

a

ñꢊn a^’(kí hiꢀu bꢈi must^+*

(

a, a^’)) thì vꢌi mꢋi

c

∈

γ(

a

), tꢣn

∈

∗

a

ñꢊn a^’

(

∈

c

∈

a

∗

c^’. Ngưꢑc

(

c

∈

a

∈

∗

TẠP CHÍ KHOA HỌC − SỐ 8/2016

41

2.4. Tiꢎn ñiꢎu kiꢈn yꢏu nhꢐt và hꢑu ñiꢎu kiꢈn mꢂnh nhꢐt

Trong nhiꢇu ꢚng dꢓng cꢄa trꢠu tưꢑng hoá vꢞ tꢠ, tꢙp vꢞ tꢠ trꢠu tưꢑng

Φ

bao gꢣm mꢎt vꢞ

tꢠ biꢃu diꢜn con ñꢊm chương trình (program counter). Do ñó, mꢖi trꢍng thái trꢠu tưꢑng sꢡ

liên quan chꢐt chꢡ ñꢊn mꢎt vꢞ trí cꢄa chương trình, vì vꢙy ñꢣng nghĩa nó cũng liên quan

ñꢊn mꢎt câu lꢀnh. Cho mꢎt câu lꢀnh s và mꢎt vꢞ tꢠ e trên tꢙp X các biꢊn cꢄa chương trình,

tiꢇn ñiꢇu kiꢀn yꢊu nhꢘt (weakest precondition) ꢏ WP(s, e) và hꢙu ñiꢇu kiꢀn mꢍnh nhꢘt

(strongest postcondition)ꢏ SP(s, e) ñưꢑc ñꢞnh nghĩa như sau [5]:

•

Nꢊu

ñꢊn mꢎt trꢍng thái thoꢂ mãn e, và WP(s, e) là vꢞ tꢠ yꢊu nhꢘt ñꢂm bꢂo ñiꢇu này.

Nꢊu s ñưꢑc thꢅc thi tꢠ mꢎt trꢍng thái thoꢂ mãn thì chương trình sꢡ chuyꢃn ñꢊn mꢎt

trꢍng thái thoꢂ mãn SP( ), và SP( ) là vꢞ tꢠ mꢍnh nhꢘt thoꢂ mãn ñiꢇu này.

s ñưꢑc thꢅc thi tꢠ mꢎt trꢍng thái thoꢂ mãn WP(s, e) thì chương trình sꢡ chuyꢃn

•

e

s

,

e

s, e

Ví dꢓ, trong thꢄ tꢓc 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 dꢞch chuyꢃn must^(+,ꢞ)có thꢃ ñưꢑc tính toán tꢅ ñꢎng sꢒ dꢓng các tiꢇn ñiꢇu kiꢀn yꢊu

nhꢘt và hꢙu ñiꢇu kiꢀn mꢍnh nhꢘt. Thꢅc tꢊ, câu lꢀnh

khi và chꢛ khi

WP(s,a^’), và tꢍo ra dꢞch chuyꢃn must ^ꢞ(a, a^’) khi và chꢛ khi a^’

Đôi khi ngưꢔi ta cũng sꢒ dꢓng khái niꢀm vꢞ tꢠ tiꢇn ñiꢇu kiꢀn (preꢏpredicate). Cho mꢎt câu

lꢀnh và mꢎt vꢞ tꢠ , nꢊu ñưꢑc thꢅc thi tꢠ mꢎt trꢍng thái thoꢂ mãn pre(s, e) thì chương

trình sꢡ chuyꢃn tꢌi mꢎt trꢍng thái thoꢂ mãn . Dꢜ thꢘy, pre(s, e) = ¬ WP(s, ¬e).

s

thꢅc thi tꢍo ra dꢞch chuyꢃn must⁺

( )

a, a^’

a

⇒

SP(s,a).

s

e

s

e

3. MꢒT PHƯƠNG PHÁP TRꢓU TƯꢔNG HOÁ Đꢕ PHÂN TÍCH TÍNH

KHꢆ ĐꢖT

3.1. Mꢋc tiêu

Trꢠu tưꢑng hoá vꢞ tꢠ ñưꢑc sꢒ dꢓng giúp phân tích nhꢗng chương trình có không gian

trꢍng thái lꢌn. Phương pháp trꢠu tưꢑng này rꢘt hꢗu ích trong viꢀc chꢚng minh các tính chꢘt

cꢄa chương trình nhưng có nhiꢇu hꢍn chꢊ trong viꢀc xác ñꢞnh lꢖi [5]. Mꢎt trong nhꢗng lí do

chính là viꢀc phân tích phát hiꢀn lꢖi phꢓ thuꢎc rꢘt nhiꢇu vào xác ñꢞnh tính khꢂ ñꢍt, tuy

nhiên phân tích tính khꢂ ñꢍt khi ñã ꢚng dꢓng trꢠu tưꢑng hoá vꢞ tꢠ lꢍi bꢟ qua nhiꢇu trꢍng

thái cꢄa hꢀ thꢁng khi có sꢅ xuꢘt hiꢀn cꢄa vòng lꢐp [6] [7]. Xét thꢄ tꢓc Increment trong ví

42

TRƯỜNG ĐẠI HỌC THỦ ĐÔ Hꢀ NỘI

dꢓ trên, thꢄ tꢓc này ñơn giꢂn là tăng giá trꢞ cꢄa biꢊn x, và dꢜ dàng ñꢃ thꢘy rꢢng giá trꢞ cꢄa x

sꢡ ñꢍt ñꢊn 3n và lꢀnh printf ("reached") sꢡ ñưꢑc thꢅc thi. Tuy nhiên, hꢆu hꢊt các phương

pháp phân tích sꢡ sinh ra mꢎt vꢞ tꢠ cho mꢖi vòng lꢐp, dꢤn tꢌi bùng nꢉ không gian trꢍng thái

và do ñó nhanh chóng vưꢑt quá khꢂ năng xꢒ lí cꢄa máy tính.

Xét thꢄ tꢓc Increment trong ví dꢓ 1 và hꢀ dꢞch chuyꢃn trꢠu tưꢑng cꢄa thꢄ tꢓc 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ꢀ dꢒch chuyꢜn trꢆu tưꢇng cꢔa thꢔ tꢄc Increment

Mꢎt cách chi tiꢊt, hình 1 và hình 4, biꢃu diꢜn không gian trꢍng thái cꢄa thꢄ tꢓc

Increment và mô hình trꢠu tưꢑng hoá theo bꢎ các vꢞ tꢠ {0≤x<n, n≤x<2n, 2n≤x<3n, 3n≤x}

,

qua phép trꢠu tưꢑng vꢞ tꢠ, các quan hꢀ dꢞch chuyꢃn trꢈ thành may và không ñóng vꢌi phép

bꢕc cꢆu, do ñó không thꢃ dꢅa trên mô hình trꢠu tưꢑng ñꢃ kꢊt luꢙn rꢢng, mꢎt trꢍng thái cꢓ

thꢃ thuꢎc a₃là tꢌi ñưꢑc tꢠ mꢎt trꢍng thái cꢓ thꢃ thuꢎc

chuyꢃn trꢠu tưꢑng, tꢘt cꢂ các dꢞch chuyꢃn ñꢇu mang tính "có thꢜ". Mꢋi trꢍng thái chi tiꢊt

trong a₃ñꢇu có mꢎt trꢍng thái liꢇn trưꢌc trong

₂, vì vꢙy ta có must^–(a₂, a₃). Tꢘt cꢂ các

a₀. Nói cách khác, trong hꢀ dꢞch

a

quan hꢀ dꢞch chuyꢃn còn lꢍi trong mô hình trꢠu tưꢑng ñꢇu là các dꢞch chuyꢃn may. Do ñó

không thꢃ kꢊt luꢙn rꢢng trꢍng thái in ra chuꢖi "reached" là tꢌi ñưꢑc tꢠ trꢍng thái khꢈi tꢍo.

Mꢓc tiêu bài báo muꢁn trình bày là cách tiꢊp cꢙn ñꢃ xác ñꢞnh tính khꢂ ñꢍt trong trưꢔng hꢑp

như vꢙy mà không cꢆn tinh chꢛnh lꢍi mô hình trꢠu tưꢑng ñꢃ bꢉ sung các trꢍng thái tꢌi ñưꢑc

qua vòng lꢐp.

Chꢚng minh tính khꢂ ñꢍt khi xuꢘt hiꢀn các vòng lꢐp hiꢀn nay là mꢎt thách thꢚc lꢌn ñꢁi

vꢌi trꢠu tưꢑng hoá vꢞ tꢠ và phân tích chương trình. Gꢆn ñây ñã có nhꢗng tiꢊn bꢎ ñáng kꢃ

trong chꢚng minh tꢅ ñꢎng tính kꢊt thúc cꢄa chương trình [8], [9]. Các tiꢊn bꢎ này có ý

nghĩa lꢌn trong viꢀc xác ñꢞnh tính khꢂ ñꢍt. Ý tưꢈng chính trong các chꢚng minh này là sꢒ

dꢓng các hàm thꢚ hꢍng và tꢙp bꢞ chꢐn dưꢌi. Tuy nhiên, kĩ thuꢙt này yêu cꢆu sinh ra các

hàm thꢚ hꢍng và thưꢔng không phù hꢑp ñꢃ chꢚng minh tꢣn tꢍi mꢎt ñưꢔng dꢤn tꢌi ñưꢑc

mꢎt trꢍng thái cꢓ thꢃ trong hꢀ thꢁng không ñơn ñꢞnh.

Trong nhiꢇu trưꢔng hꢑp (ñꢐc biꢀt, trong tꢘt cꢂ các hꢀ thꢁng phꢆn mꢇm thꢅc tꢊ), các hꢀ

thꢁng thưꢔng rꢘt lꢌn nhưng vꢤn có hꢗu hꢍn trꢍng thái. Mꢓc tiêu cꢄa bài báo là nhꢢm giꢂi

quyꢊt trong nhꢗng trưꢔng hꢑp như vꢙy vꢤn có khꢂ năng phân tích tính khꢂ ñꢍt cꢄa hꢀ thꢁng

bꢢng phương pháp trꢠu tưꢑng hoá vꢞ tꢠ, mà không phꢂi xét duyꢀt toàn bꢎ các trꢍng thái chi

TẠP CHÍ KHOA HỌC − SỐ 8/2016

43

tiꢊt trong các vòng lꢐp. Phương thꢚc trong bài báo sꢒ dꢓng tꢌi các ñiꢇu kiꢀn dꢅa trên cꢘu

trúc ñꢣ thꢞ chương trình (program graph) tương ꢚng vꢌi hꢀ thꢁng chi tiꢊt và các ñiꢇu kiꢀn

này có thꢃ cho phép kiꢃm tra tꢅ ñꢎng.

3.2. Giꢇi pháp

Như ñã trình bày ꢈ phꢆn trưꢌc, các dꢞch chuyꢃn may không ñưꢑc ñóng dưꢌi tính bꢕc

cꢆu, do ñó các phương pháp trꢠu tưꢑng không thꢃ ñꢁi phó vꢌi tính khꢂ ñꢍt cꢄa chương

trình có vòng lꢐp. Trong phꢆn này chúng tôi sꢡ mô tꢂ phương pháp ñꢃ ñꢁi phó vꢌi vòng lꢐp.

Đꢞnh nghĩa mꢎt entry port 4 cꢄa mꢎt trꢍng thái trꢠu tưꢑng

γ(e_a) γ(a) và vꢌi mꢋi c_eγ(e_a),c_elà khꢈi tꢍo hoꢐc p(c_e) \ γ(a)≠

cꢓ thꢃ _eñưꢑc thꢃ hiꢀn bꢈi entry port e_abên trong và _elà trꢍng thái khꢈi tꢍo hoꢐc là mꢎt

vài trꢍng thái trưꢌc cꢄa _enꢢm ngoài a.

Đꢞnh nghĩa mꢎt exit port 4 cꢄa mꢎt trꢍng thái trꢠu tưꢑng

γ(x_a) γ(a) và vꢌi mꢋi c_xγ(x_a),s(c_x)\ γ(a)≠ Tꢚc là mꢋi trꢍng thái cꢓ thꢃ

hiꢀn bꢈi exit port _atrong và mꢎt vài trꢍng thái kꢊ tiꢊp cꢄa _xnꢢm ngoài a.

a

là mꢎt vꢞ tꢠ

e_asao cho

⊆

∈

∅

. Tꢚc là mꢋi trꢍng thái

c

a

c

a

là mꢎt vꢞ tꢠ x_asao cho

_xñưꢑc thꢃ

⊆

∈

∅

.

c

x

a

c

Đꢉnh lí 1: Xét mꢉt trꢊng thái trꢆu tưꢇng a, lꢗy e_avà x_alà entry và exit port cꢔa a sao

cho tꢗt cꢓ nhꢟng ñiꢎu kiꢀn sau ñưꢇc thoꢓ mãn.

1. γ(a) là hꢟu hꢊn;

2. Vꢌi mꢁi c ∈ γ(a ⋀ ¬x_a), chúng ta có |s(c) ∩ γ(a)| ≤ 1,tꢖc là mꢁi trꢊng thái chi tiꢕt

trong γ(a ⋀ ¬x_a) có ít nhꢗt mꢉt trꢊng thái kꢕ tiꢕp trong γ(a);

3. must⁻(a ⋀ ¬x_a,a ⋀ ¬e_a),tꢖc là mꢁi trꢊng thái chi tiꢕt trong γ(a ⋀ ¬e_a) có trꢊng

thái liꢎn trưꢌc trong γ(a ⋀ ¬x_a).

Thì must^−*(e_a,x_a),tꢖc là vꢌi mꢁi c’ ∈ γ(x_a), tꢝn tꢊi c ∈ γ(e_a) sao cho c→*c’.

Chú ý rꢢng ñiꢇu kiꢀn 1 và 3 có nghĩa rꢢng e_akhông thꢃ là rꢖng (trꢠ khi x_alà rꢖng,

trưꢔng hꢑp này chꢚng minh dꢜ dàng)

Chꢖng minh ñꢒnh lí 1: Chꢚng minh ñꢞnh lí 1 ñưꢑc dꢅa trên viꢀc xây dꢅng mꢎt ñꢣ thꢞ

có hưꢌng không chu trình ꢏ DAG trong ñó tꢘt cꢂ các trꢍng thái có thꢃ tꢌi ñưꢑc tꢠ ñꢛnh

nguꢣn. Tính hꢗu hꢍn cꢄa γ(a) có nghĩa rꢢng ñꢛnh nguꢣn cꢄa DAG ñưꢑc chꢚa trong γ(e_a).

Giꢂ sꢒ rꢢng γ(e_a) không rꢖng, ngưꢑc lꢍi dꢜ dàng chꢚng 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à tꢙp

các ñꢛnh không có ñꢛnh kꢇ trưꢌc trong G. Xây dꢅng mꢎt chuꢖi DAGs: G₀, G₁,… sao cho

44

TRƯỜNG ĐẠI HỌC THỦ ĐÔ Hꢀ NỘI

vꢌi mꢋi k ≥ 0, DAG G_k= <V_k, E_k> thoꢂ mãn γ(x_a) ⊆ V_k⊆ γ(a) và mꢋi trꢍng thái trong có

thꢃ tꢌi ñưꢑc tꢠ trꢍng thái nào ñó trong source(G_k). Ngoài ra, vꢌi mꢋi k ≥ 0, hoꢐc source

(G_k) ⊆ γ(e_a) hoꢐc có thꢃ xây dꢅng mꢎt DAG G_k+1thoꢂ mãn 2 tính chꢘt trên và chꢚa hoàn

toànG_k. Doγ(a) là hꢗu hꢍn [ñiꢇu kiꢀn 1 cꢄa ñꢞnh lí], tꢠ ñó có k ≤ |γ(a)| mà source (G_k) ⊆ γ(e_a).

Lưu ý rꢢng vì G_klà ñꢣ thꢞ con cꢄa hꢀ thꢁng chi tiꢊt, tính khꢂ ñꢍt tương ꢚng vꢌi

must^ꢞ*(source(G_k), V_k). Vì thꢊ, nꢊu tꢣn tꢍi DAG G_kthoꢂ mãn tꢘt cꢂ ba thuꢎc tính, thì

must^ꢞ*(e_a, x_a).

Xác ñꢞnh G_kbꢢng phương pháp quy nꢍp theo k, là chiꢇu cao cꢄa DAG. Dꢅa vào ñó,

cho G₀= <V₀, E₀> vꢌi V₀= γ(x_a) và E₀= ∅. Dꢜ thꢘy G₀thoꢂ mãn cꢂ hai thuꢎc tính thoát

và khꢂ ñꢍt như trên. Đꢐc biꢀt, do E₀= ∅, ta có source(G_k) = V₀, do tính khꢂ ñꢍt thoꢂ mãn

ñꢁi vꢌi ñưꢔng rꢖng. Lưu ý rꢢng vì γ(x_a) không rꢖng, vì thꢊ có V₀vàsource(G₀).

Vꢌi bưꢌc quy nꢍp, cho k ≥ 0 sao cho G_kthoꢂ mãn cꢂ hai thuꢎc tính thoát và khꢂ ñꢍt và

không thoꢂ mãn thuꢎc tính vào. Ta có thꢃ xây dꢅng mꢎt DAG G_k+1thoꢂ mãn thuꢎc tính

thoát và khꢂ ñꢍt và hoàn toàn chꢚa G_k.

LꢘyS_k= source(G_k)\γ(e_a). Đꢃ ý rꢢng tꢠ G_kkhông thoꢂ mãn thuꢎc tính ñꢆu vào và

source(G_k) không rꢖng, thì ta có tꢙp S_kcũng không rꢖng. Domust⁻(a ∧¬x_a, a ∧ ¬e_a)(ñiꢇu

kiꢀn 3 cꢄa ñꢞnh lí) và S_k∩γ(e_a) = ∅ (theo ñꢞnh nghĩa cꢄa S_k), mꢋi trꢍng thái trong S_kcó mꢎt

trꢍng thái liꢇn kꢇ trưꢌc trong γ(a ∧¬x_a).LꢘyV’_k= {p(c) ∩γ(a ∧¬x_a) | c ∈ S_k},(V’_k≠ 0). Đꢐt

V_k+1= V_k∪ V’_k, và ñꢐt E_k+1= E_k∪ {<c’,c>| c

∈ S_k&& c’ ∈ p(c) ∩ γ(a ∧¬x_a)}. Do ñó, G_k+1

thêm vào các trꢍng thái G_ktrong γ(a ∧¬x_a) có mꢎt dꢞch chuyꢃn tꢌi các trꢍng thái trong

source(G_k)\γ(e_a), và cũng thêm vào các dꢞch chuyꢃn tꢠ các trꢍng thái ñó tꢌi các trꢍng thái

trong source(G_k)\γ(e_a). Tꢠ V_k⊆V_k+1và tꢠ giꢂ thiꢊt quy nꢍp, thì γ(x_a) ⊆ V_k+1, do vꢙy

G_k+1thoꢂ mãn vꢌi các thuꢎc tính thoát.

Tꢠ giꢂ thiꢊt quy nꢍp, G_klà mꢎt DAG, thì G_k+1cũng là mꢎt DAG. Thꢙt vꢙy, các ñꢛnh

mã ñã thêm vào G_klà các ñꢛnh tꢠ V’_ktꢌi V_k. Ngoài ra, tꢠ V’_k≠∅, dꢜ dàng nhꢙn thꢘy rꢢng

nꢊuV_kvà V’_klà tách rꢔi thì V_k+1chꢛ chꢚa ñúng V_k.

Vꢌi trưꢔng hꢑp k=0, chúng ta có V₀= γ(x_a). Do V’_kchꢚa chꢛ các trꢍng thái trong

γ(a ∧¬x_a), rõ ràng rꢢng V₀∩ V’₀= ∅. Vꢌi trưꢔng hꢑp k>0, giꢂ sꢒ ngưꢑc lꢍi rꢢng tꢣn tꢍi mꢎt c

∈

V’_k∩ V_k. Do V’_kvà γ(x_a) là tách rꢔi, nên rõ ràng rꢢng c

sao cho c V’_j. Do ñó, có mꢎt c’ s(c) ∩ γ(a) hay c’ γ(a) là nút kꢊ tiꢊp cꢄa c. Do vꢙy,

c’ S_k. Nhưng c’ là liꢇn kꢇ trưꢌc cꢄa c trong G_k, c’ không nꢢm trong source(G_k). Nên c’ ∉ S_k.

Điꢇu này mâu thuꢤn. Nên G_k+1thoꢂ mãn tính khꢂ ñꢍt. Theo ñꢞnh nghĩa, source(G_k+1) = V’_k,

∈ V_k, tꢚc là có mꢎt j, 1 ≤ j < k

∈

TẠP CHÍ KHOA HỌC − SỐ 8/2016

45

nhưng theo giꢂ thiꢊt quy nꢍp, tꢘt cꢂ các trꢍng thái trong V_klà tꢌi ñưꢑc tꢠ mꢎt vài trꢍng thái

trong source(G_k). Tꢠ mꢖi trꢍng thái trong source(G_k) là kꢊ tiꢊp cꢄa mꢎt vài trꢍng thái trong

V’_k, dꢤn ñꢊn rꢢng mꢋi trꢍng thái trong V_k+1là tꢌi ñưꢑc tꢠ mꢎt vài trꢍng thái trong

source(G_k+1).

Tương tꢅ, có ñꢞnh lí 2 như sau:

Đꢉnh lí 2: Xét mꢉt trꢊng thái trꢆu tưꢇng a, lꢗy e_avà x_alà entry và exit port cꢔa a sao

cho tꢗt cꢓ nhꢟng ñiꢎu kiꢀn sau ñꢎu thoꢓ mãn.

1. γ(a) là hꢟu hꢊn;

2. Vꢌi mꢁi c ∈ γ(a ⋀ ¬e_a), có |p(c) ∩ γ(a)| ≤ 1, tꢖc là mꢁi trꢊng thái chi tiꢕt trong

γ(a ⋀ ¬e_a) có ít nhꢗt mꢉt trꢊng thái kꢕ tiꢕp trong γ(a);

3. must⁺(a ⋀ ¬x_a,a ⋀ ¬e_a), tꢖc là mꢁi trꢊng thái chi tiꢕt trong γ(a ⋀ ¬x_a) ñꢎu có

trꢊng thái liꢎn trưꢌc trong γ(a ⋀ ¬e_a).

Thì must^+*(e_a,x_a),tꢖc là vꢌi mꢁi c∈ γ(e_a), tꢝn tꢊi c’∈ γ(x_a) sao cho c→*c’.

Chꢖng minh ñꢒnh lí 2: Chꢚng minh tương tꢅ ñꢞnh lí 1

Đꢉnh lí 3: Cho a₁và a₂là các trꢍng thái trꢠu tưꢑng vꢌi entry port lꢆn lưꢑt là e_a1và e_a2,

và exit port lꢆn lưꢑt là x_a1và x_a2. Giꢂ sꢒ rꢢng vꢌi mꢋi i ∈ {1,2}, ta có γ(a_i) là hꢗu hꢍn, vꢌi

mꢋi c ∈ γ(a_i⋀ ¬x_ai)ta có|s(c) ∩ γ(a_i)| ≤ 1, và ta cũng có must⁻(a_i⋀ ¬x_ai,a_i⋀ ¬e_ai),

must^−*(x_a1,e_a2). Thì must^−*(e_a1,x_a2).

Chꢖng minh ñꢒnh lí 3: Theo ñiꢇu kiꢀn cꢄa ñꢞnh lí, các ñiꢇu kiꢀn cꢄa ñꢞnh lí 1 ñưꢑc thoꢂ

mãn vꢌi a₁và a₂cùng nhꢗng entry port, exit portchú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 bꢕc cꢆu cꢄa các quan hꢀ dꢞch

chuyꢃn kiꢃu must⁻. Tương tꢅ, các dꢞch chuyꢃn must⁺cũng có tính bꢕc cꢆu, áp dꢓng ñꢞnh lí

2 ta có ñiꢇu phꢂi chꢚng minh.

3.3. ꢗng dꢋng

Phương pháp trꢠu tưꢑng hoá mô hình dꢞch chuyꢃn trꢍng thái theo vꢞ tꢠ ñã trình bày có

thꢃ ñưꢑc ꢚng dꢓng trong kiꢃm chꢚng mô hình 10, hoꢐc phân tích chương trình tĩnh ñꢃ xác

ñꢞnh tính khꢂ ñꢍt. Quá trình trꢠu tưꢑng, sinh vꢞ tꢠ có thꢃ tꢅ ñꢎng hoá bꢢng cách kꢊt hꢑp

tương ꢚng mꢎt trꢍng thái trꢠu tưꢑng vꢌi mꢎt lꢀnh thꢅc thi và các trꢍng thái chi tiꢊt phát

sinh khi thꢅc thi lꢀnh ñó. Thꢅc hiꢀn chia làm 2 giai ñoꢍn chính:

• Tính toán các entry port và exit port tương ꢚng vꢌi các trꢍng thái trꢠu tưꢑng dꢋc

theo ñưꢔng thꢅc thi;

46

TRƯỜNG ĐẠI HỌC THỦ ĐÔ Hꢀ NỘI

• Kiꢃm tra các ñiꢇu kiꢀn tương ꢚng vꢌi giꢂi pháp 1 hoꢐc 2, sau ñó kꢊt luꢙn.

Ví dꢋ: Xem xét lꢍi ví dꢓ vꢇ thꢄ tꢓc Increment và trꢠu tưꢑng cꢄa thꢄ tꢓc này. Áp dꢓng

phương pháp tiꢊp cꢙn trên cꢄa bài báo cho trꢠu tưꢑng cꢄa phương thꢚc Increment ñưꢑc

minh hoꢍ như 0.

Hình 5. Phân tích tính khꢓ ñꢊt trên trꢆu tưꢇng cꢔa thꢔ tꢄc Increment

Trꢍng thái trꢠu tưꢑng a₀: 0 ≤ x ≤ n có entry port x=0 và exit port x = nꢞ1. Các ñiꢇu

kiꢀn trong ñꢞnh lí 1 ñưꢑc thoꢂ mãn trong a₀vꢌi entry port và exit port này do:

1. n là hꢗu hꢍn do ñó γ(a₀) là hꢗu hꢍn.

2. Do thꢄ tꢓc thꢅc hiꢀn theo cơ chꢊ ñơn ñꢞnh, nên mꢖi trꢍng thái chi tiꢊt chꢛ có mꢎt

trꢍng thái kꢊ tiꢊp duy nhꢘt.

3. Mꢖi trꢍng thái cꢓ thꢃ trꢠ x=0 có mꢎt nút liꢇn kꢇ trưꢌc trong a₀.

Có thꢃ kꢊt luꢙn rꢢng must^−*(x=0,x=nꢞ1). Vꢌi chꢚng minh tương tꢅ, các ñiꢇu kiꢀn ñưꢑc

thoꢂ mãn tꢍi a₁vꢌi entry port là x=n và exit portlà 2nꢞ2 ≤ x < 2n, và tꢍi a₂vꢌi entry port là

2n ≤ x ≤ 2n+1 và exit port là 3nꢞ3 ≤ x < 3n. Tꢠ ñây ta có thꢃ kꢊt luꢙn ñưꢑc must^−*(x=n,2nꢞ

2≤ x < 2n) và must^−*(2n≤ x ≤ 2n+1, 3nꢞ3≤x<3n). Ngoài ra, must⁻(x=nꢞ1,x=n), must⁻(2nꢞ

2≤x<2n, 2n≤x≤2n+1) và must⁻(3nꢞ3≤x<3n, 3n<x). Như vꢙy, có thꢃ kꢊt luꢙn ñưꢑc

must^−*(x=0,3n≤x) (do tính chꢘt bꢕc cꢆu cꢄa must⁻).

4. KꢘT LUꢙN

Trong bài báo chúng tôi ñã trình bày mꢎt phương pháp trꢠu tưꢑng hoá theo vꢞ tꢠ giúp

phân tích tính khꢂ ñꢍt ñꢁi vꢌi các hꢀ thꢁng có không gian trꢍng thái lꢌn. Kꢊt quꢂ chính cꢄa

phương pháp là có thꢃ xác ñꢞnh chính xác tính khꢂ ñꢍt mà không phꢂi làm mꢞn mô hình

trꢠu tưꢑng khi xuꢘt hiꢀn nhiꢇu vòng lꢐp trong hꢀ thꢁng.

Trong tương lai chúng tôi sꢡ dꢅ ñꢞnh tiꢊp tꢓc nghiên cꢚu ñꢃ phát triꢃn công cꢓ kiꢃm

chꢚng mô hình tꢅ ñꢎng dꢅa trên nꢎi dung lí thuyꢊt ñã nghiên cꢚu.

TẠP CHÍ KHOA HỌC − SỐ 8/2016

47

TÀI LIꢄU THAM KHꢆO

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, JoostꢏPieter 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.491ꢏ503.

5. Cormac Flanagan, Shaz Qadeer (2002), "Predicate abstraction for software verification",

Proceeding POPL '02 Proceedings of the 29th ACM SIGPLANꢞSIGACT symposium on

Principles of programming languages, pp.191ꢏ202.

6. A.R. Bradley, Z. Manna, H. Sipma (2005), "Linear Ranking with Reachability", In Proc. of

17thCAV, LNCS 3576, pp.491ꢏ504.

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.152ꢏ199.

8. Byron Cook, Andreas Podelski, Andrey Rybalchenko (2011), "Proving Program Termination",

Communications of the ACM, vol. 54 Issue 5, pp.88ꢏ98.

9. B. Cook, A. Podelski, A. Rybalchenko (2006), "Termination proofs for systems code", In

Proc. ACM PLDI, pp.415ꢏ426.

10. P. Godefroid, R. Jagadeesan (2002), "Automatic abstraction using generalized model

checking", In Proc. 14th CAV, LNCS 2404, pp.137ꢏ150.

11. Loveland, Donald W (1978), "Automated Theorem Proving: A Logical Basis", Fundamental

Studies in Computer Science, Volume 6, NorthꢏHolland Publishing.

BASING ON THE GRAPH OF PROGRAM TO ANALYZE THE

AVAILABILITY OF THE PROGRAM

Abstract: 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.

Keywords: The graph of program, availability, ranking function, model checking