B môn : Các v n đ hi n đ i công ngh ph n m m.ộ ấ ề ệ ạ ệ ầ ề
L I C M NỜ Ả Ơ
Đ hoàn thành báo cáo môn h c ể ọ các v n đ hi n đ i công nghấ ề ệ ạ ệ
ph n m mầ ề m t cách hoàn ch nh, chúng em xin bày t lòng c m n chânộ ỉ ỏ ả ơ
thành đ n các th y cô đã h ng d n chúng em t i tr ng Đ i H c Côngế ầ ướ ẫ ạ ườ ạ ọ
Ngh . Đ c bi t là th y ệ ặ ệ ầ Đ ng Đ c H nhặ ứ ạ và cô Vũ Di u H ngệ ươ , th y côầ
đã tr c ti p h ng d n t n tình, s a ch a và đóng góp nhi u ý ki n quýự ế ướ ẫ ậ ử ữ ề ế
báu giúp chúng em hoàn thành t t báo cáo môn h c c a mình.ố ọ ủ
L i c m n chân thành và sâu s c, chúng em xin g i đ n gia đình, đãờ ả ơ ắ ử ế
luôn sát cánh và đ ng viên chúng em trong nh ng giai đo n khó khăn nh t.ộ ữ ạ ấ
Chân thành c m n đ n các b n trong l p đã h tr đ chúng em cóả ơ ế ạ ớ ỗ ợ ể
th hoàn thành t t công vi c đ c giao. ể ố ệ ượ
Chúng em xin chân thành bi t n s t n tình d y d c a t t c cácế ơ ự ậ ạ ỗ ủ ấ ả
quý th y cô ầKhoa Công ngh Thông tin – Tr ng Đ i h c Công Nghệ ườ ạ ọ ệ
Thông Tin – Đ i h c Qu c gia Hà N iạ ọ ố ộ .
Chúng cũng xin chân thành g i l i c m n đ n t t c các th y cô đãử ờ ả ơ ế ấ ả ầ
gi ng d y chúng em th i gian qua, đã truy n đ t và trang b cho chúng emả ạ ờ ề ạ ị
nh ng kinh nghi m, ki n th c chuyên môn, giúp chúng em m r ng t mữ ệ ế ứ ở ộ ầ
nhìn khi thâm nh p vào th c t . chúng em xin h a s không ng ng ph nậ ự ế ứ ẽ ừ ấ
đ u n l c v n lên trong h c t p và công tác sau này.ấ ỗ ự ươ ọ ậ
B môn : Các v n đ hi n đ i công ngh ph n m m.ộ ấ ề ệ ạ ệ ầ ề
B môn : Các v n đ hi n đ i công ngh ph n m m.ộ ấ ề ệ ạ ệ ầ ề
CH NG 1ƯƠ
GI I THI UỚ Ệ
1.1 Đ t v n đặ ấ ề
Trong các công ty phát tri n ph n m m h u h t công vi c ki m thể ầ ề ầ ế ệ ể ử
c a ki m th viên đ c th c hi n th công b ng tay. Trong khi đó sủ ể ử ượ ự ệ ủ ằ ố
l ng tình hu ng ki m tra quá nhi u mà các ki m th viên không th hoànượ ố ể ề ể ử ể
t t b ng tay trong th i gian c th nào đó. Ho c khi nhóm l p trình đ a raấ ằ ờ ụ ể ặ ậ ư
nhi u phiên b n ph n m m liên ti p đ ki m tra. Th c t cho th y vi cề ả ầ ề ế ể ể ự ế ấ ệ
đ a ra các phiên b n ph n m m có th là hàng ngày, m i phiên b n baoư ả ầ ề ể ỗ ả
g m nh ng tính năng m i, ho c tính năng cũ đ c s a l i hay nâng c p.ồ ữ ớ ặ ượ ử ỗ ấ
Vi c b sung ho c s a l i code cho nh ng tính năng phiên b n m i cóệ ổ ặ ử ỗ ữ ở ả ớ
th làm cho nh ng tính năng khác đã ki m tra t t ch y sai m c dù ph nể ữ ể ố ạ ặ ầ
code c a nó không h ch nh s a. Đ kh c ph c đi u này, đ i v i t ngủ ề ỉ ử ể ắ ụ ề ố ớ ừ
phiên b n, ki m th viên không ch ki m tra ch c năng m i ho c đ cả ể ử ỉ ể ứ ớ ặ ượ
s a, mà ph i ki m tra l i t t c nh ng tính năng đã ki m tra t t tr c đó.ử ả ể ạ ấ ả ữ ể ố ướ
Đi u này khó kh thi v m t th i gian n u ki m tra thông th ng. Đ gi iề ả ề ặ ờ ế ể ườ ể ả
quy t v n đ này chúng ta áp d ng k thu t ki m th d a trên mô hình choế ấ ề ụ ỹ ậ ể ử ự
quá trình sinh các ca ki m th t đ ng. Nh ng làm sao đ th c hi n đ cể ử ự ộ ư ể ự ệ ượ
quá trình sinh các ca ki m th t đ ng chúng ta ph i áp d ng khá nhi u cácể ử ự ộ ả ụ ề
công ngh s n có và thông d ng nh t. đây chúng em xin gi i thi u mãệ ẵ ụ ấ Ở ớ ệ
nhúng C vào mô t Promela và trình bày công c Spin đ sinh ra các caả ụ ể
ki m th t đ ng t đó áp d ng vào m t bài toán c th . ể ử ự ộ ừ ụ ộ ụ ể
Trong báo cáo này chúng em t p trung trình bày v vi c nghiên c uậ ề ệ ứ
ki m th d a trên mô hình và ng d ng công c Spin vào vi c t đ ng sinhể ử ự ứ ụ ụ ệ ự ộ
các ca ki m th : Xây d ng mô hình h th ngể ử ự ệ ố và th c nghi m. Bên c nh đóự ệ ạ
chúng em cũng gi i thi u qua v trình so n th o Emac, m t công c l pớ ệ ề ạ ả ộ ụ ậ
trình khá hay và ra đ i t r t s m, ch y đ c trên nhi u h đi u hànhờ ừ ấ ớ ạ ượ ề ệ ề
thông d ng.ụ
1.2 N i dung báo cáo môn h cộ ọ
B môn : Các v n đ hi n đ i công ngh ph n m m.ộ ấ ề ệ ạ ệ ầ ề
Bài báo cáo trình bày ngôn ng Promela vào thi t k Promela và ápữ ế ế
d ng kĩ thu t s d ng công c Spin là hai n i dung quan trong nh t c a quáụ ậ ử ụ ụ ộ ấ ủ
trình sinh ca ki m th t đ ng. ể ử ự ộ
Đ xu t bài toán c th đ th c hi n công vi c Demo m t ch ngề ấ ụ ể ể ự ệ ệ ộ ươ
trình nh . T đó đem áp d ng vào ph c v cho vi c ki m ch ng ph nỏ ừ ụ ụ ụ ệ ể ứ ầ
m m.ề
Xây d ng tài li u h ng d n v ngôn ng Promela, công c Spin,ự ệ ướ ẫ ề ữ ụ
trình so n th o Emac ph c v cho vi c nghiên c u, gi ng d y và ng d ngạ ả ụ ụ ệ ứ ả ậ ứ ụ
th c ti n.ự ễ
1.3 C u trúc báo cáo môn h cấ ọ
Các ph n còn l i c a khóa lu n có c u trúc nh sau:ầ ạ ủ ậ ấ ư
Ch ng 2:ươ Trình bày các khái ni m v ngôn ng mô hình promela,ệ ề ữ
bao g m các đ nh nghĩa c b n v khai báo bi n và ki u, đ nh danh,ồ ị ơ ả ề ế ể ị
h ng s , bi u th c, ti n trình.ằ ố ể ứ ế
Ch ng 3:ươ Gi i thi u công c Spin, c u trúc cú pháp l nh, tham sớ ệ ụ ấ ệ ố
l nh và ch c năng c a nó.ệ ứ ủ
Ch ng 4: ươ Gi i thi u công c so n th o Emacs.ớ ệ ụ ạ ả
Ch ng 5:ươ Tóm t t các k t qu đã đ t đ c, k t lu n, nh ng h nắ ế ả ạ ượ ế ậ ữ ạ
ch và h ng nghiên c u phát tri n trong t ng lai.ế ướ ứ ể ươ
B môn : Các v n đ hi n đ i công ngh ph n m m.ộ ấ ề ệ ạ ệ ầ ề
CH NG 2ƯƠ
TRÌNH BÀY KHÁI NI M MÔ HÌNH PROMELAỆ
Ch ng này s l n l t trình bày nh ng khái ni m c b n v môươ ẽ ầ ượ ữ ệ ơ ả ề
hình Promela. Khái ni m c th v c u trúc cú pháp l nh, th t c hàm,ệ ụ ể ề ấ ệ ủ ụ
cách khai báo bi n trong Promela.ế
2.1 Khái ni m c b n ngôn ng Promelaệ ơ ả ữ
Xây d ng mô hình h th ng b ng ngôn ng Promela là m t công đo nự ệ ố ằ ữ ộ ạ
quan tr ng trong ki m th d a trên mô hình, đ t đó có th dùng công cọ ể ử ự ể ừ ể ụ
Spin sinh ra các ca ki m th . Ngôn ng mô hình Promela có nhi u nétể ử ữ ề
t ng đ ng v i ngôn ng C. ươ ồ ớ ữ
•Đ nh nghĩa Promela (Process meta language )ị
Promela là ngôn ng mô hình dùng đ mô t h th ng đ ng th i [ữ ể ả ệ ố ồ ờ The
Spin Model Checker: Primer and Reference Manual].
Ví d : Giao th c m ng, h th ng đi n tho i, các ch ng trình giaoụ ứ ạ ệ ố ệ ạ ươ
ti p đa lu ng,…ế ồ
•C u trúc ch ng trình Promelaấ ươ
M t ch ng trình Promela c b n g m:ộ ươ ơ ả ồ
Khai báo ki u.ể
Khai báo bi n.ế
Khai báo ti n trình.ế
[init process].
// Các khai báo ki u và bi nể ế
mtype = {MSG, ACK};
chan toS = ...
chan toR = ...
bool flag;
// M t ti n trìnhộ ế
proctype Sender() {
// Thân m t ti n trìnhộ ế
...
}