Đ I H C CÔNG NGH - Đ I H C QU C GIA HÀ N IẠ Ọ Ệ Ạ Ọ Ố Ộ
KHOA CÔNG NGH THÔNG TINỆ
BÁO CÁO
Đ tài:ề
TÌM HI UỂ
ERIGONE MODEL CHECKER
Gi ng viên h ng d n : TS. Đ ng Đ c H nhả ướ ẫ ặ ứ ạ
TS. Vũ Di u H ngệ ươ
Sinh viên th c hi n : L u Hoàng Tùngự ệ ư
Nguy n Công Đ cễ ứ
Hà n i - 2012ộ
M C L CỤ Ụ
L I NÓI Đ UỜ Ầ ............................................................................ 1
Ch ng 1. ERIGONE TRÊN CÔNG C EUIươ Ụ ........................... 2
I/ Gi i thi u t ng quanớ ệ ổ .................................................................................................................. 2
1.Gi i thi u Erigone model checkerớ ệ .......................................................................................... 2
2.Công c phát tri nụ ể ................................................................................................................. 3
2.1. Command line ............................................................................................................. 3
2.2. EUI (Erigone User Interface) ......................................................................................... 7
3.Mô ph ng và xác minh trong Erigoneỏ .................................................................................... 9
4.Ch ng trình Traceươ ................................................................................................................ 9
II/ Ví d demoụ ............................................................................................................................. 10
1.Gi i quy t hai ti n trình lo i tr l n nhauả ế ế ạ ừ ẫ ............................................................................ 10
2.Lo i tr l n nhau v i m t semaphoreạ ừ ẫ ớ ộ .................................................................................. 12
3.Xác minh m t ch ng trình Promela v i câu l nh assertộ ươ ớ ệ .................................................... 14
4.Xác minh m t thu c tính an toàn s d ng LTLộ ộ ử ụ ................................................................... 16
5.Ch ng minh khái ni m v s công b ng v i câu l nh LTLứ ệ ề ự ằ ớ ệ ................................................. 18
Ch ng 2: ERIGONE B NG CÂU L NHươ Ằ Ệ .............................. 22
I/ Tìm hi u v Erigone b ng dòng l nh:ể ề ằ ệ ..................................................................................... 22
1.Erigone: ................................................................................................................................ 22
1.1. Th c thi theo ph ng th c:ự ươ ứ ......................................................................................... 23
1.2. Hi n th l a ch n v i các đ i s :ể ị ự ọ ớ ố ố ................................................................................ 24
1.3. Biên d ch ch y thông đi p:ị ạ ệ ........................................................................................... 24
1.4. Chuy n ti p(transitions):ể ế .............................................................................................. 24
1.5. Chuy n đ i LTL:ể ổ .......................................................................................................... 25
1.6. Ki m tra l i(debug arguments)ể ỗ .................................................................................... 25
Tìm hi u v Erigone model checkerể ề Trang 1
2. List: ...................................................................................................................................... 26
3. Trace: .................................................................................................................................. 26
4. VMC .................................................................................................................................... 27
II/ Mô ph ng m t s ch ng trình Promela b ng công c Erigoneỏ ộ ố ươ ằ ự ........................................... 28
1. Mô ph ng v i quá trình truy n thông đi p(chanel)ỏ ớ ề ệ ............................................................. 28
2. Mô ph ng ch ng trình t ng tranhỏ ươ ươ ................................................................................... 34
3. Ki m ch ng đ tin c y khi s d ng LTLể ứ ộ ậ ử ụ ............................................................................ 36
III/ Ch ng trình Listươ ................................................................................................................... 37
IV/ Ch ng trình Traceươ ............................................................................................................... 37
V/ Ch ng trình VMCươ ................................................................................................................. 40
TÀI LI U THAM KH OỆ Ả ......................................................... 44
Tìm hi u v Erigone model checkerể ề Trang 2
L I NÓI Đ UỜ Ầ
Erigone là mô hình tri n khai l i c a mô hình ki m ch ng Spin đ c phátể ạ ủ ể ứ ượ
tri n v i m c đích ki m ch ng đ c d dàng tr c quan, uy n chuy n nh mể ớ ụ ể ứ ượ ễ ự ể ể ằ
thu n l i cho vi c nghiên c u và mô ph ng mô hình h th ng, erigone có thậ ợ ệ ứ ỏ ệ ố ể
đ c th c hi n b ng công c trên giao di n đ h a EUI ho c thao tác b ng câuượ ự ệ ằ ụ ệ ồ ọ ặ ằ
l nh d i d ng command line v i nhi u tùy bi n l a ch n cho phép ki mệ ướ ạ ớ ề ế ự ọ ể
ch ng ho t đ ng c a h th ng. ứ ạ ộ ủ ệ ố
Tìm hi u Erigone model checker nh m m c đích tìm hi u rõ h n v môể ằ ụ ể ơ ề
hình ki m ch ng erigone thông qua m t s ví d , đ c th c hi n b ng công cể ứ ộ ố ụ ượ ự ệ ằ ụ
đ h a EUI và b ng câu l nh command line, v i nh ng nhìn nh, phân tíchồ ọ ằ ệ ớ ữ ả
ch ng trình m t cách tr c quan.ươ ộ ự
Vì đây là l n đ u ti p xúc, tìm hi u v 1 khía c nh m i nên s khôngầ ầ ế ể ề ạ ớ ẽ
tránh kh i nh ng khó khăn d n đ n nh ng thi u sót trong báo cáo, chúng emỏ ữ ẫ ế ữ ế
mong th y (cô) b qua.ầ ỏ
Chúng em xin chân thành c m n th y cô đã ch b o h ng d n chúng em đả ơ ầ ỉ ả ướ ẫ ể
chúng em có th hoàn thành báo cáo này. ể
Tìm hi u v Erigone model checkerể ề Trang 1
Ch ng 1. ERIGONE TRÊN CÔNG C EUIươ Ụ
I/ Gi i thi u t ng quanớ ệ ổ
1. Gi i thi u Erigone model checkerớ ệ
Erigone là m t ph n tri n khai l i c a mô hình ki m ch ng Spin. Erigoneộ ầ ể ạ ủ ể ứ
tri n khai m t t p con c a Promela, nó là đ đ ch ng minh các khái ni mể ộ ậ ủ ủ ể ứ ệ
c b n c a mô hình ki m ch ng cho vi c xác minh (verification) c a cácơ ả ủ ể ứ ệ ủ
ch ng trình đ ng th i. Không m t ngôn ng c u trúc nào đ c thêm vàoươ ồ ờ ộ ữ ấ ượ
sao cho ch ng trình cho Erigone có th đ c s d ng v i Spin đ cóươ ể ượ ử ụ ớ ể
nhi u tính uy n chuy n và hi u su t t t h n mong mu n.ề ể ể ệ ấ ố ơ ố
Erigone đ c vi t b ng ADA năm 2005 cho đ tin c y, b o trì và tính linhượ ế ằ ộ ậ ả
ho t. Nó đ c s d ng nh m t chu n ki n trúc.ạ ượ ử ụ ư ộ ẩ ế
Đ c tính c a Erigone:ặ ủ
Erigone là đ n nh t, khép kín, t p tin th c thi đ cài đ t và s d ngơ ấ ậ ự ể ặ ử ụ
là d dàng.ễ
Erigone s n sinh m t v t (trace) chi ti t trong nh ng thu t toán môả ộ ế ế ữ ậ
hình ki m ch ng. N i dung các v t có th tùy ch nh và m t đ nhể ứ ộ ế ể ỉ ộ ị
d ng th ng nh t d a trên t khóa đ c s d ng đ có th đ c đ cạ ố ấ ự ừ ượ ử ụ ể ể ượ ọ
tr c ti p ho c đ c s d ng b i các công c khác.ự ế ặ ượ ử ụ ở ụ
Mô-đun hóa m r ng đ c s d ng trong vi c thi t k c a ch ngở ộ ượ ử ụ ệ ế ế ủ ươ
trình Erigone t o đi u ki n cho hi u bi t v mã ngu n. Đi u nàyạ ề ệ ể ế ề ồ ề
cũng s cho phép các nhà nghiên c u d dàng s a đ i và m r ngẽ ứ ễ ử ổ ở ộ
ch ng trình.ươ
Ngoài vi c ki m ch ng mô hình Erigone còn ch a các ch ng trìnhệ ể ứ ứ ươ
b xung riêng bi t:ổ ệ
– COMPILER: Ch y ch ng trình biên d ch c a chính nó.ạ ươ ị ủ
– LST: Đ nh d ng đ u ra c a trình biên d chị ạ ầ ủ ị
Tìm hi u v Erigone model checkerể ề Trang 2