Xem mẫu
- Báo cáo môn học 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.
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.
2
- Bộ môn : Các vấn đề hiện đại công nghệ phần mềm.
Ph l c
LỜI CẢM ƠN ......................................................................................................... 1
CHƯƠNG 1 GIỚI THIỆU ...................................... Error! Bookmark not defined.
1.1Đặt vấn đề ...................................................... Error! Bookmark not defined.
1.2Nộ i dung báo cáo môn học ............................. Error! Bookmark not defined.
1.3Cấu trúc báo cáo môn học .............................. Error! Bookmark not defined.
CHƯƠNG 2 TRÌNH BÀY KHÁI NIỆM MÔ HÌNH PROMELA.............................5
Khái niệm cơ bản ngôn ngữ Promela......................................................6
2.1
2.2 Biến và Kiểu ...........................................................................................6
2.3 Định danh, Hằng số và Biểu thức...........................................................7
2.4 Tiến trình.................................................................................................8
2.5 Lệnh và cấu trúc lệnh Promela............................................................... 9
2.6 Sự khác biệt khi sử dụng 2 từ khóa Atomic, D-step trong bài toán cụ
thể....................................................................................................................10
CHƯƠNG 3 TRÌNH BÀY CÔNG CỤ SPIN, THAM SỐ, CÚ PHÁP LỆNH.....17
Sơ lược về công c ụ spin...................................................................17
3.1
Lịch sử p hát triển công cụ SPIN..........................................................17
3.2
Một số yếu tố thành công của SPIN......................................................17
3.3
Kiến trúc SPIN – Cấp độ tổ chức Spin.................................................18
3.4
Công cụ dòng lệnh................................................................................18
3.4
CHƯƠNG 4 GIỚ I THIỆU CÔNG CỤ SOẠN TH ẢO EMACS.....................21
4.1 Khái niệm và chức năng của GNU Emacs............................................21
Các lo ại trình soạn thảo Emacs.............................................................22
4.2
Bộ gõ.................................................................................................. ...23
4.4
Giao diện trình so ạn thảo Emacs...........................................................23
4.4
Cấu trúc lệnh Emac...............................................................................24
4.6
Các phím đơn..................................................................................... .24
4.5
3
- Bộ môn : Các vấn đề hiện đại công nghệ phần mềm.
4.6 Các phím tiền tố và tổ hợp................................................................... 25
CHƯƠNG 5 KẾT LUẬN ....................................... Error! Bookmark not defined.
TÀI LIỆU THAM KHẢO....................................... Error! Bookmark not defined.
4
- 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ốngvà 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
5
- 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,
b ao 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.
6
- 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.
Khái niệm cơ bản ngôn ngữ Promela
2.1
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:
K hai báo kiểu.
K hai báo biến.
K hai 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
...
}
7
- Bộ môn : Các vấn đề hiện đại công nghệ phần mềm.
proctype Receiver() {
...
}
// Tiến trình init
init {
// Tạo một tiến trình
...
}
Biến và Kiểu
2.2
Giố ng như nhiều ngôn ngữ lập trình khác, Promela yêu cầu các biến
phải được khai báo trước khi chúng có thể được sử dụng. Khai báo biến theo
phong cách của ngôn ngữ lập trình C. Theo mặc đ ịnh tất cả các biến của các
loại biến cơ bản được bắt đầu từ 0. Cũng như trong C thì 0 được coi như sai
và khác 0 được coi là đúng. Một biến có thể là biến toàn cục hoặc là biến địa
phương của mỗi tiến trình.
Kiểu dữ liệu
Kiều Miền giá trị
bit or bool { 0, 1}
byte 0…255
-2 15 … 215 - 1
short
-2 31 … 231 – 1
int
• Kiểu khai báo
int ii;
bit bb;
bb = 1;
ii = 2;
• Kiểu cấu trúc
Records (structs): Có th ể tìm ra xung đột khi ch ạy
Typedef record{
short f1;
b yte f2;
}
8
- Bộ môn : Các vấn đề hiện đại công nghệ phần mềm.
Truy cập như C
Record rr;
rr.f1 = …
• Kiểu mảng
Một mảng có cấu trúc như sau:
int table[max]
Lưu ý rằng điều này tạo ra một m ảng max-1 số nguyên:
table[0], table[1], ... table[max-1]
• Kiểu liệt kê
Một bộ các h ằng số tượng trưng được khai báo như sau :
mtype = {LINE_CLEAR, TRAIN_ON_LINE, LINE_BLOCKED}
• Kênh (Chanel): Được sử d ụng để trao đổi dữ liệu giữa các tiến trình.
Cú pháp:
chan = [] of ,, ;
Cú pháp gửi tin nhắn trong mộ t kênh (!)
chan-name ! , ..... ;
Cú pháp nhận tin nhắn trong một kênh (?)
chan-name ? , .....;
Định danh, H ằng số và Biểu thức
2.3
• Định danh
Định danh có thể là một chữ cái, một ký tự.
• Hằng số
Hằng số là một chuỗ i ký tự đại diện cho một số nguyên thập phân.
Hằng số tượng trưng có thể được định nghĩa như sau:
#define MAX 999
• Biểu thức
9
- Bộ môn : Các vấn đề hiện đại công nghệ phần mềm.
Một biểu thức được xây dựng từ các biến, hằng số và sử dụng các toán
tử sau đây:
+, -, *, /, %, --, ++,
>, >=, ,
- Bộ môn : Các vấn đề hiện đại công nghệ phần mềm.
Tất cả các chương trình promela đều cần một tiến trình init nó
giống như hàm main() trong ngôn ngữ C. Việc thực thi một chương
trình promela được bắt đầu từ tiến trình init.
Một tiến trình init có dạng:
init { /* Các khai báo địa phương và các biểu thức. */ }
Đơn giản nhất có thể là chương trình promela có dạng:
init { skip }
Skip có nghĩa là không có biểu thức nào trong tiến trình init;
Mỗi tiến trình được định nghĩa bởi một proctype, nó được thực thi đồng
thời với tất cả các tiến trình khác, nó giao tiếp với các tiến trình khác thông qua
việc sử dụng các biến công cộng hoặc các kênh. Tiến trình thực thi sau khi thực
hiện hàm run.
Một số ví d ụ đơn giản về tiến trình
proctype hello(){ printf("Hello") }
proctype world(){ printf("World\n") }
init { run hello(); run world () }
Lệnh và cấu trúc lệnh Promela
2.5
Mỗi lệnh được ngăn cách với nhau mộ t dấu chấm phẩy (;).
Một số lệnh và cấu trúc tiêu biểu
• Skip: không thực hiện, chỉ thay đổi khi tiến trình gọi tới
• Printf: In ra màn hình.
• Assert(Exp) : Sử dụng kiểm tra nếu Exp là biểu thức hợp lệ
(Nếu giá trị Exp = 0 thì thực thi sẽ bị lỗ i).
Cấu trúc lặp (do)
Cú pháp:
if
11
- Bộ môn : Các vấn đề hiện đại công nghệ phần mềm.
:: choice1 -> stat1.1; stat1.2;
:: choice2 -> stat2.1; stat2.2;
:: ..........................................
:: choicen -> statn.1; statn.2;
fi;
Lựa chọn một trong các điều kiện thực thi
Cấu trúc so sánh (if)
do
:: choice1 -> stat1.1; stat1.2;
:: choice2 -> stat2.1; stat2.2;
:: ...........................................
:: choicen -> statn.1; statn.2;
od;
Lựa chọn được lặp đi lặp lại nhiều lần và có thể dừng nếu gặp break.
Cú pháp Active
Từ khóa Active có thể là tiền tố cho mọi thủ tục được khai báo trong
hàm.
Hiệu quả của từ khóa active là tạo ra liên kết Prototype trong hệ thống
ban đầu
Nhiều trường hợp của cùng một khai báo Prototype có thể được tạo ra
bằng cách sử dụng một m ảng các hậu tố tùy chọn. Ví dụ :
active [4] proctype hello(){ printf("Hello") }
active [7] proctype world(){ printf("World\n") }
Lưu ý : trường hợp này sẽ tạo ra 4 trường hợp của “Hello” và
7 trường hợp của “World”
12
- Bộ môn : Các vấn đề hiện đại công nghệ phần mềm.
Cú pháp Atomic
Có thể sử dụng tới một nhóm lệnh trong một thông báo atomic. Các
lệnh được thực hiện đơn lẻ và không xen kẽ với các lệnh trong tiến trình khác.
Tự động phá vỡ nếu lệnh bị khóa khi đó các lệnh trong tiến trình khác
có thể x en kẽ vào giữa.
Cú pháp:
atomic { statement1; ...; statementn }
Statement1 chạy đầu tiên, statementn chạy cuối cùng.
Cú pháp D -STEP
Nhiều phiên bản Atomic : Không chứa trạng thái trung gian được tạo ra
và lưu trữ.
Chỉ có thể chứa những bước xác đ ịnh.
Thời gian chạy sẽ bị lỗ i nếu Stat-I(I>1) bị chặn, khóa.
D-STEP cực kì hữu ích để thực hiện việc tính toán trong quá trình chuyển đổi
duy nhất.
Cú pháp:
d-step { statement1; ... ;statementn }
Cú pháp TIME-OUT
Lệnh sẽ được thực thi nếu không có một lệnh khác trong các tiến trình
khác đang thực thi.
Giố ng như thời gian chờ của Hệ thống Spin sử d ụng để giải quyết bế
tắc xung đột.
Nó không phải là một tính năng thời gian thực và có thể không được sử
dụng trong mô hình times-outs tham gia vàothiết kế hệ thống.
Sự khác biệt khi sử dụng 2 từ khóa Atomic, D-step trong bài toán cụ
2.6
thể
Mô hình
o K hi không sử dụng từ khóa trong chương trình
13
- Bộ môn : Các vấn đề hiện đại công nghệ phần mềm.
Hình 1: Khi không sử dụng từ khóa
Các trạng thái sinh ra khi không sử d ụng từ khóa sẽ được tăng lên theo công
bội. Trong trường hợp này tất cả các trạng thái có thể tạo được từ chương
trình đ ều có thể sinh ra. Do đó những trạng thái không cần thiết mà vẫn được
lưu trữ trong bộ nhớ sẽ làm lãng phí mộ t phần bộ nhớ và số lượng trạng nhiều
như vậy sẽ làm cho người thiết kế khó có thể kiểm soát được.
o K hi sử dụng từ khóa Atomic
14
- Bộ môn : Các vấn đề hiện đại công nghệ phần mềm.
Hình 2: khi sử dụng từ khóa Atomic
Mặc dù câu lệnh Atomic sẽ không được chạy xen kẽ nhau nhưng các trạng
thái trung gian vẫn sẽ được khởi tạo và lưu trữ trong stack. Do đó khi có một
trạng thái trung gian (trạng thái A) bị khóa , ngắt thì lời gọi Atomic sẽ bị m ất
và các trạng thái trung gian sẽ được đến thăm.
o K hi sử dụng từ khóa D-STEP
15
- Bộ môn : Các vấn đề hiện đại công nghệ phần mềm.
Hình 3: khi sử dụng từ khóa D-Step
Khác với từ khóa Atomic, từ khóa D-Step thực thi mộ t mã lênh nếu một bước
hay giao dịch nào bị khóa thì chương trình sẽ bị lỗi. Các trạng thái trung gian
sẽ không được khởi tạo.
Một chương trình đ ơn giản để kiểm tra chức năng khi sử dụng các từ
khóa
o Mã lệnh: Khi không sử dụng từ khóa nào.
16
- Bộ môn : Các vấn đề hiện đại công nghệ phần mềm.
int x=0
int y=0;int z=0
proctype A(){
printf("gia tri x1= %d \n", 1);
printf("gia tri y1= %d \n", 1);
printf("gia tri z1= %d\n", 1);
}
proctype B(){
printf("gia tri x2= %d \n", 2);
printf("gia tri y2= %d \n", 2);
printf("gia tri z2= %d\n", 2);
}
init {
run A();
run B();
}
Hình 4: Chương trình không sử dụng lệnh Atomic, D-step
Khi không sử dụng từ khóa nào thì số các trạng thái sinh ra trong ví dụ trên sẽ
là 9 trường hợp. Do các câu lệnh trong hai tiến trình sẽ chạy xen kẽ với nhau.
o Mã lệnh: Khi sử dụng từ khóa atomic hoặc D -step
Do chức năng của mã lệnh atomic và D-step là tương đối giống nhau chỉ
khác nhau đôi chút về trạng thái trung gian được khởi tạo.
Atomic : Khởi tạo trạng thái trung gian nhưng chỉ lưu vào stack.
Cho đến khi nào có mộ t trạng thái bên trong mã lệnh atomic bị
khóa, ngắt thì mới thực hiện các trạng thái trong Stack.
D -step: Không khởi tạo trạng thái trung gian nên khi có một trạng
thái nào bên trong mã lệnh D-step bị khóa thì chương trình thực thi
sẽ bị lỗi.
17
- Bộ môn : Các vấn đề hiện đại công nghệ phần mềm.
int x=0
int y=0;
int z=0
proctype A(){
atomic{
printf("gia tri x1= %d \n", 1);
printf("gia tri y1= %d \n", 1);
printf("gia tri z1= %d\n", 1);
}
}
proctype B(){
printf("gia tri x2= %d \n", 2);
printf("gia tri y2= %d \n", 2);
printf("gia tri z2= %d\n", 2);
}
init {
run A();
run B();
}
Hình 5: Khi sử dụ ng từ khóa Atomic, D-step
Trong trường hợp này thì số các trạng thái sinh ra sẽ giảm đi bởi vì khi
bắt đầu đ ến trạng thái x1 thì chương trình phải chạy hết đến trạng thái x3 rồi
mới xen kẽ tới các trạng thái khác được. Dựa vào đặc điểm này mà người
kiểm thử có thể loại bớt đi được khá nhiều các trạng thái không cần thiết.
18
- Bộ môn : Các vấn đề hiện đại công nghệ phần mềm.
CHƯƠNG 3
TRÌNH BÀY CÔNG CỤ SPIN, THAM SỐ , CÚ PHÁP LỆNH
Sơ lược về công c ụ spin
3.1
SPIN là công cụ mã nguồ n mở, phổ biến và được sử dụng bởi hàng
ngàn người trên toàn cầu.
SPIN được sử dụng cho việc xác minh thẩm định của các hệ thống
phân phối phần mềm.
Nó cung cấp một giả lập cho phép các nhà thiết kế đ ạt được kết quả
phản hồ i từ hệ thống mô hình của họ. Những kết quả p hản hồi đó đóng vai trò
quan trọng trong sự hiểu biết của các nhà thiết kế về hệ thố ng trước khi họ
đầu tư vào phân tích chính thức.
Lịch sử p hát triển công cụ SPIN
3.2
Từ năm 1980 Spin được phát triển tại Bell Labs của nhóm Unix Phần
mềm này phát triển rộng rãi từ năm 1991.
Tháng 4 năm 2002 Spin được trao giải thưởng phần mềm uy tín cho
năm 2001 của ACM.
Các version chính: năm 1991 là 1.0 (initial version) tới năm 2002 đ ã có
SPIN version 4.0 (automata extration from C code).
1.0 Jan 1991 Initial version (Holzmann 1991
2.0 Jan 1995 Partial order reduction
3.0 Apr 1997 Minimised automaton
representation
4.0 Late 2002 Ax: automata extraction from C
code
5.0 Oct 2007 Multi-core & swarm support
6.0 Dec 2010 Inline LTL formula parallel bfs
Một số yếu tố thành công của SPIN
3.3
Cú pháp thực hiện (bằng cách sử dụng tựa ngôn ngữ C).
Giao diện người dùng đồ họa đẹp Xspin.
19
- Bộ môn : Các vấn đề hiện đại công nghệ phần mềm.
Không chỉ là một công cụ nghiên cứu, mà còn là công cụ hỗ trợ.
Chứa nhiều hơn so với nhiều thập kỷ nghiên cứu kéo xác minh máy
tính tiên tiến AIDEC (nhiều thuật toán tối ưu hóa).
Kiến trúc SPIN – Cấp độ tổ chức Spin
3.4
Hình 6: Cấp độ tổ chức SPIN
Công cụ dòng lệnh.
3.4
3.4.1 Cú pháp Spin
Một số câu lênh trong SPIN.
Spin –a [-m] [-Pcpp] file
spin [-bglmprsv] [-J] [-qN] [-nN] [-Pcpp] file
spin -c [-t] [-Pcpp] file
spin -d [-Pcpp ] file
spin -f LTL
spin -F file
spin -i [-bglmprsv] [-J] [-qN] [-Pcpp] file
20
nguon tai.lieu . vn
