Công nghệ thông tin hiện nay là một trong những ngành phát triển mạnh mẽnói
chung, cùng với công nghệphần mềmnói riêng. Nhằm tạo ra những sản phẩm phần
mềm đảm bảo chất lượng và tính chính xác cao. Nên việc đặc tảvà kiểm chứng phần
mềm hết sức quan trọng trong nhiều lĩnh vực sửdụng phần mềm, đặc biệt là các ngành
công nghệcao đòi hỏi sựchính xác cao của phần mềm. Trong khuôn khổcủa một bài
luận văn tốt nghiệp em đi sâu vào phương pháp đặc tảvà kiểm chứng phần mềm sử
dụng ngôn ngữCafeOBJ và đặc biệt đã áp dụng phương pháp này cho một hệthống lò
vi sóng. Cùng với việc học tập và nghiên cứu trong khi làm khóa luận tốt nghiệp để
được tiếp cậnvới thực tếem đã thu được một sốkết quảnhất định. Thông qua đó,
cùng với kiến thức cơ sởkhi ngồi trên ghếnhà trường, em đã tìm hiểu thêm vềnhững
tiến bộtrong việc phát triển phần mềm trên thếgiới nói chung và Việt Nam nói riêng.
50 trang |
Chia sẻ: lvbuiluyen | Lượt xem: 2235 | Lượt tải: 3
Bạn đang xem trước 20 trang tài liệu Đặc tả và kiểm chứng phần mềm sử dụng cafeobj, để xem tài liệu hoàn chỉnh bạn click vào nút DOWNLOAD ở trên
ĐẠI HỌC QUỐC GIA HÀ NỘI
TRƯỜNG ĐẠI HỌC CÔNG NGHỆ
Phạm Ngọc Thắng
ĐẶC TẢ VÀ KIỂM CHỨNG PHẦN MỀM SỬ DỤNG
CafeOBJ
KHOÁ LUẬN TỐT NGHIỆP ĐẠI HỌC HỆ CHÍNH QUY
Ngành: Công nghệ thông tin
HÀ NỘI - 2010
ĐẠI HỌC QUỐC GIA HÀ NỘI
TRƯỜNG ĐẠI HỌC CÔNG NGHỆ
Phạm Ngọc Thắng
ĐẶC TẢ VÀ KIỂM CHỨNG PHẦN MỀM SỬ DỤNG
CafeOBJ
KHOÁ LUẬN TỐT NGHIỆP ĐẠI HỌC HỆ CHÍNH QUY
Ngành: Công nghệ thông tin
Cán bộ hướng dẫn: TS. Nguyễn Việt Hà
Cán bộ đồng hướng dẫn: ThS. Đặng Việt Dũng
HÀ NỘI - 2010
Đặc tả và kiểm chứng phần mềm sử dụng CafeOBJ Phạm Ngọc Thắng
i
Lời cảm ơn
Em xin bày tỏ lòng cảm ơn sâu sắc tới TS. Nguyễn Việt Hà và ThS. Đặng Việt
Dũng về sự hướng dẫn, chỉ bảo tận tình, cùng với những lời khuyên quý giá của thầy
trong quá trình em học tập cũng như thực hiện khóa luận.
Em xin gửi lời cảm ơn tới các thầy cô giảng dạy tại Đại học Công nghệ - Đại học
Quốc Gia Hà Nội đã trang bị cho em những kiến thức quý báu trong thời gian em học
tại trường. Đó cũng là tiền đề cơ sở để em có thể thực hiện được tốt khóa luận của
mình.
Em xin gửi lời cảm ơn tới các thầy các cô trong bộ môn Công nghệ phần mềm đã
tạo điều kiện cho em được làm việc ở trên bộ môn với đầy đủ trang thiết bị cho em học
tập và làm việc.
Cảm ơn bạn bè, người thân về sự động viên, giúp đỡ về mặt tinh thần cũng như
về mặt vật chất trong thời gian em thực hiện khóa luận này.
Hà nội, tháng 6 năm 2010
Sinh viên thực hiện
Phạm Ngọc Thắng
Đặc tả và kiểm chứng phần mềm sử dụng CafeOBJ Phạm Ngọc Thắng
ii
Tóm tắt
Công nghệ thông tin hiện nay là một trong những ngành phát triển mạnh mẽ nói
chung, cùng với công nghệ phần mềm nói riêng. Nhằm tạo ra những sản phẩm phần
mềm đảm bảo chất lượng và tính chính xác cao. Nên việc đặc tả và kiểm chứng phần
mềm hết sức quan trọng trong nhiều lĩnh vực sử dụng phần mềm, đặc biệt là các ngành
công nghệ cao đòi hỏi sự chính xác cao của phần mềm. Trong khuôn khổ của một bài
luận văn tốt nghiệp em đi sâu vào phương pháp đặc tả và kiểm chứng phần mềm sử
dụng ngôn ngữ CafeOBJ và đặc biệt đã áp dụng phương pháp này cho một hệ thống lò
vi sóng. Cùng với việc học tập và nghiên cứu trong khi làm khóa luận tốt nghiệp để
được tiếp cận với thực tế em đã thu được một số kết quả nhất định. Thông qua đó,
cùng với kiến thức cơ sở khi ngồi trên ghế nhà trường, em đã tìm hiểu thêm về những
tiến bộ trong việc phát triển phần mềm trên thế giới nói chung và Việt Nam nói riêng.
Đặc tả và kiểm chứng phần mềm sử dụng CafeOBJ Phạm Ngọc Thắng
iii
Mục lục
Chương 1. Giới thiệu ........................................................................................................1
1.1 Đặt vấn đề ...............................................................................................................1
1.2 Nội dung nghiên cứu của khóa luận.........................................................................1
1.3 Cấu trúc khóa luận...................................................................................................2
Chương 2. Phương pháp hình thức....................................................................................3
2.1 Phân loại .................................................................................................................3
2.2 Sử dụng...................................................................................................................4
2.2.1 Đặc tả hình thức................................................................................................4
2.2.2 Phát triển ..........................................................................................................5
2.2.3 Kiểm chứng ......................................................................................................5
2.2.3.1 Chứng minh của con người.........................................................................5
2.2.3.1 Chứng minh tự động...................................................................................6
Chương 3. Ngôn ngữ CafeOBJ .........................................................................................7
3.1 Giới thiệu ................................................................................................................7
3.2 Đặc tả và kiểm chứng trong CafeOBJ......................................................................9
3.2.1 Ví dụ.................................................................................................................9
3.2.2 Đặc tả số tự nhiên ...........................................................................................10
3.2.3 Đặc tả thuộc tính.............................................................................................10
3.2.4 Kiểm chứng thuộc tính....................................................................................10
Chương 4. Khái quát về OTS và bài toán QLOCK..........................................................13
4.1 Giới thiệu về OTS .................................................................................................13
4.2 OTS (Observation transition system).....................................................................14
4.3 Mô tả bài toán QLOCK .........................................................................................17
Đặc tả và kiểm chứng phần mềm sử dụng CafeOBJ Phạm Ngọc Thắng
iv
4.4 Đặc tả QLOCK với OTS .......................................................................................17
4.5 Đặc tả thuộc tính và kiểm chứng đặc tả .................................................................21
Chương 5. Đặc tả và kiểm chứng hệ thống lò vi sóng .....................................................24
5.1 Hệ thống lò vi sóng ...............................................................................................24
5.1.1 Mô tả hệ thống................................................................................................24
5.1.2 Mô tả các thuộc tính........................................................................................26
5.2 Mô hình hóa hệ thống trong OTS/CafeObj ............................................................26
5.2.1 Mô hình hóa và mô tả hệ thống trong OTS......................................................26
5.2.2 Đặc tả hình thức hệ thống trong CafeObj ........................................................28
5.2.3 Không gian trạng thái của hệ thống đặc tả hình thức .......................................29
5.2.4 Các thuộc tính được mô tả ..............................................................................29
5.3 Kiểm chứng bằng phương pháp quy nạp................................................................33
5.3.1 Các bước quy nạp ...........................................................................................33
5.3.2 Kiểm chứng bằng phương pháp quy nạp trong CafeOBJ.................................33
5.4. Kiểm chứng bằng phương pháp tìm kiếm trạng thái .............................................33
Chương 6. Kết luận.........................................................................................................36
Đặc tả và kiểm chứng phần mềm sử dụng CafeOBJ Phạm Ngọc Thắng
v
Danh mục hình vẽ
Hình 3.1: Mô đun EXAMPLE trong CafeOBJ. .................................................................8
Hình 3.2: Đặc tả của module PNAT cho ví dụ. .................................................................9
Hình 3.3: Đặc tả thuộc tính cho điều kiện (*)..................................................................10
Hình 3.4: Kiểm chứng quy nạp với module ISTEP. ........................................................11
Hình 3.5: Kiểm chứng quy nạp cho đặc tả.......................................................................11
Hình 4.1: Thuật toán của bài toán QLOCK. ....................................................................17
Hình 4.2: Kiểu biến tổng quát cho hàng đợi QUEUE. .....................................................18
Hình 4.3: Hàng đợi QUEUE cho bài toán QLOCK. ........................................................19
Hình 4.4: Đặc tả cho hệ thống QLOCK. .........................................................................20
Hình 4.5: Hành động try trong hệ thống QLOCK............................................................20
Hình 4.6: Mô đun INV và ISTEP dùng để kiểm chứng. ..................................................21
Hình 4.7: Kiểm chứng với trường hợp (1).......................................................................22
Hình 4.8: Kiểm chứng với trường hợp (2).......................................................................22
Hình 4.9: Kiểm chứng với bổ đề. ....................................................................................23
Hình 5.1: Cấu trúc Kripke của Lò vi sóng [1]. ................................................................25
Hình 5.2: Mô hình của lò vi sóng. ...................................................................................27
Hình 5.3: Đặc tả của lò vi sóng trong CafeOBJ...............................................................28
Hình 5.4: Mô đun LABEL trong CafeOBJ. .....................................................................29
Hình 5.5: Hình thức hóa không gian trạng thái của hệ thống. ..........................................29
Hình 5.6: Hình thức hóa các thuộc tính. ..........................................................................30
Hình 5.7: Đặc tả các thuộc tính trong CafeOBJ...............................................................31
Hình 5.8: Mô đun ISTEP trong CafeOBJ. .......................................................................32
Chương 1: Giới thiệu Phạm Ngọc Thắng
1
Chương 1
Giới thiệu
1.1 Đặt vấn đề
Đặc tả và kiểm chứng hình thức là một pha quan trọng nhằm nâng cao độ tin cậy
và chất lượng của phần mềm sử dụng phương pháp hình thức. Đối với các hệ thống
yêu cầu độ tin cậy cao như hệ thống điều khiển lò phản ứng hạt nhân hay điều khiển
tên lửa, … Các phương pháp đặc tả và kiểm chứng hình thức sẽ được áp dụng cho
những hệ thống này trước khi triển khai chúng. Trong khi việc kiểm thử phần mềm
(software testing) chỉ có thể chỉ ra các lỗi phát hiện được nhưng không thể chỉ ra được
phần mềm hoàn toàn không có lỗi, các phương pháp kiểm chứng có thể đảm bảo hệ
thống không có lỗi sau khi đã được kiểm chứng đúng đắn.
Hiện nay, đã có nhiều phương pháp và công cụ hỗ trợ cho việc đặc tả và kiểm
chứng phần mềm như OBJ [14], Maude [14], CafeOBJ [13], SPIN [15], SMV [17],
NuSMV [16], …. Mỗi phương pháp có những ưu và nhược điểm riêng và bị hạn chế
trong một số hệ thống nhất định.
Mục đích của khóa luận là tìm hiểu về phương pháp hình thức (formal method)
cũng như phương pháp đặc tả và kiểm chứng hình thức phần mềm trong CafeOBJ. Từ
mô tả của hệ thống cần kiểm chứng, chúng ta cần đặc tả hệ thống một cách hình thức
bằng ngôn ngữ CafeOBJ. Các thuộc tính cần kiểm chứng của hệ thống cũng được đặc
tả một cách tương tự. Sử dụng ngữ nghĩa cú pháp trong ngôn ngữ CafeOBJ để thể hiện
các đặc tả hệ thống cũng như các đặc tả thuộc tính của hệ thống cần kiểm chứng dưới
dạng hình thức từ các phát biểu của ngôn ngữ tự nhiên.
1.2 Nội dung nghiên cứu của khóa luận
Bài toán thực hiện trong khóa luận là bài toán đặc tả và kiểm chứng hệ thống lò
vi sóng sử dụng ngôn ngữ CafeOBJ. Đây là một trong hệ thống điển hình sẽ được trình
bày về quá trình mô hình hóa hệ thống giúp cho công việc viết đặc tả và kiểm chứng
các thuộc tính của chúng được đơn giản hơn. Nhằm kiểm chứng hệ thống một trong
những phương pháp chúng tôi quan tâm là viết đặc tả và kiểm chứng bằng CafeOBJ
Chương 1: Giới thiệu Phạm Ngọc Thắng
2
theo tư tưởng quy nạp toán học, với phương pháp này chúng ta có thể đặc tả và kiểm
chứng các hệ thống vô hạn trạng thái một cách chính xác (trong khi với kiểm chứng
mô hình (model checking) chỉ kiểm chứng hữu hạn trạng thái của hệ thống). Ngoài ra
CafeOBJ còn hộ trợ sự kiểm chứng bằng phương pháp tìm kiếm (searching) không
gian trạng thái dành cho hệ thống hữu hạn trạng thái. Đặc tả cho kiểm chứng cùng với
đặc tả hệ thống và đặc tả thuộc tính sẽ được sử dụng để kiểm chứng hệ thống. Kết quả
của quá trình kiểm chứng sẽ cho chúng ta biết được đặc tả thỏa mãn thuộc tính cần
kiểm chứng hay không.
1.3 Cấu trúc khóa luận
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 lý thuyết về phương pháp hình thức, bao gồm các khái niệm
cơ bản, các kỹ thuật cơ bản được sử dụng trong đặc tả và kiểm chứng phần mềm.
Chương 3 trình bày ngôn ngữ CafeOBJ, kỹ thuật đặc tả và kiểm chứng phần
mềm bằng phương pháp hình thức được sử dụng trong CafeOBJ.
Chương 4 trình bày phương pháp chuyển dịch hệ thống trực quan (Observation
transition system), một trong những phương pháp quan trọng nhằm đơn giản hóa việc
đặc tả và kiểm chứng phần mềm, kèm theo ví dụ về hệ thống QLOCK sử dung
OTS/CafeOBJ.
Chương 5 trình bày về “hệ thống Lò Vi Sóng” được đặc tả và kiểm chứng sử
dụng OTS/CafeOBJ, với hai phương pháp kiểm chứng khác nhau gồm quy nạp và tìm
kiếm (searching) các trạng thái.
Chương 6 tóm tắt 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.
Chương 2: Phương pháp hình thức Phạm Ngọc Thắng
3
Chương 2
Phương pháp hình thức
Trong ngành khoa học máy tính, phương pháp hình thức là các kỹ thuật toán học
cho việc đặc tả, phát triển và kiểm chứng các hệ thống phần mềm và phần cứng. Cách
tiếp cận này đặc biệt quan trọng đối với các hệ thống cần có tính toàn vẹn cao, chẳng
hạn hệ thống điều khiển lò phản ứng hạt nhân hay điều khiển tên lửa, khi an toàn hay
an ninh có vai trò quan trọng, để góp phần đảm bảo rằng quá trình phát triển hệ thống
sẽ không có lỗi. Các phương pháp hình thức đặc biệt hiệu quả tại giai đoạn đầu của
quá trình phát triển (tại các mức yêu cầu và đặc tả hệ thống), nhưng cũng có thể được
sử dụng cho một quá trình phát triển hoàn chỉnh của một hệ thống.
2.1 Phân loại
Các phương pháp hình thức có thể được sử dụng tại nhiều mức:
Mức 0: Đặc tả hình thức có thể được thực hiện và rồi một chương trình được
phát triển từ đặc tả này một cách không hình thức. Trong nhiều trường hợp, cách này
có thể là lựa chọn hiệu quả nhất về mặt chi phí.
Mức 1: Sử dụng phát triển và kiểm chứng hình thức để tạo ra một chương trình
theo một quy trình hình thức hơn. Ví dụ, có thể thực hiện các chứng minh về các tính
chất hoặc quá trình tinh chỉnh từ đặc tả hình thức tới một chương trình. Đây có thể là
lựa chọn phù hợp nhất đối với các hệ thống yêu cầu tính toàn vẹn cao với các tiêu chí
vè an toàn và an ninh.
Mức 2: Sử dụng các bộ chứng minh định lý (theorem prover) để thực hiện các
chứng minh hình thức hoàn toàn và được kiểm chứng bằn máy móc. Việc này có thể
đòi hỏi chi phí rất cao và chỉ đáng lựa chọn trong thực tiễn nếu phí tổn cho các lỗi sai
là cực kỳ cao.
Cùng với ngữ nghĩa hình thức của ngôn ngữ lập trình, các phương pháp hình thức
có thể được phân loại tương đối như sau:
Ngữ nghĩa ký hiệu (Denotational semantics), trong đó ý nghĩa của một hệ thống
được biểu diễn bằng lý thuyết toán học về miền xác định. Lợi điểm của những phương
pháp này phụ thuộc vào bản chất được hiểu rõ của các miền xác định để từ đó đem lại
Chương 2: Phương pháp hình thức Phạm Ngọc Thắng
4
ý nghĩa cho hệ thống; các phê phán chỉ ra rằng không phải hệ thống nào cũng có thể
được nhìn một cách tự nhiên hoặc trực quan dưới dạng một hàm số.
Ngữ nghĩa hoạt động (Operational semantics), trong đó, ý nghĩa của một hệ
thống được biểu diễn bằng một chuổi các hành động của một mô hình tính toán (giả
thiết là) đơn giản hơn. Lợi điểm của phương pháp này là tính đơn giản của các mô
hình tạo nên sự trong sáng của biểu diễn.
Ngữ nghĩa tiên đề (Axiomatic semantics), trong đó ý nghĩa của hệ thống được
biểu diễn theo các tiền điều kiện (precondition) và hậu điều kiện (postcondition), đây
lần lượt là các điều kiện phải được thỏa mãn tại các thời điểm trước và sau khi hệ
thống thực hiện một nhiệm vụ. Những người ủng hộ phương pháp này nói đến mối
quan hệ của nó với lôgic kinh điển; những người phê phán nói rằng những ngữ nghĩa
thuộc dạng này không thực sự mô tả xem hệ thống làm cái gì (chỉ là cái gì đúng trước
đó và sau đó).
2.2 Sử dụng
2.2.1 Đặc tả hình thức
Các phương pháp hình thức có thể được sử dụng để mô tả về hệ thống cần phát
triển, tại bất kỳ mức độ chi tiết nào mà ta muốn. Mô tả hình thức này có thể được sử
dụng để hướng dẫn các hoạt động phát triển tiếp theo; ngoài ra, nó có thể được sử
dụng để kiểm chứng xem các yêu cầu cho hệ thống đang được phát triển đã được đặc
tả một cách đầy đủ và chính xác hay chưa.
Nhu cầu về các hệ thống đặc tả hình thức đã được nói đến từ nhiều năm. Trong
báo cáo ALGOL 60, John Backus đã trình bày một hệ thống ký hiệu hình thức để mô
tả cú pháp ngôn ngữ lập trình (sau này được đặt tên là Backus normal form hay
Backus-Naur form (BNF) (Dạng chuẩn tắc Backus)).
Chương 2: Phương pháp hình thức Phạm Ngọc Thắng
5
2.2.2 Phát triển
Khi một đặc tả hình thức đã được phát triển xong, đặc tả đó có thể được sử dụng
làm một hướng dẫn trong quá trình hệ thống thực được phát triển (nghĩa là được hiện
thực hóa trong phần mềm và/hoặc phần cứng). Ví dụ:
Nếu đặc tả hình thức là một ngữ nghĩa hoạt động, hành vi được quan sát của hệ
thống thực sẽ có thể được so sánh với hành vi trong đặc tả (chính đặc tả cũng nên chạy
được hoặc giả lập được). Thêm vào đó, các lệnh hoạt động của đặc tả có thể thích hợp
cho việc dịch thẳng mã chạy được.
Nếu đặc tả hình thức là một ngữ nghĩa tiên đề, các tiền điều kiện và hậu điều kiện
của đặc tả có thể trở thành các khẳng định trong mã chạy được.
2.2.3 Kiểm chứng
Khi một đặc tả hình thức đã được phát triển, đặc tả này có thể được dùng làm cơ
sở cho việc chứng minh các tính chất của đặc tả.
2.2.3.1 Chứng minh của con người
Đôi khi, động cơ cho việc chứng minh tính đúng đắn của một hệ thống không
phải là nhu cầu đảm bảo tính đúng đắn của hệ thống mà là mong muốn hiểu rõ hơn về
hệ thống. Do đó, một số chứng minh được thực hiện dưới hình thức chứng minh toán
học: viết tay hoặc đánh máy nội dung bằng ngôn ngữ tự nhiên, với mức độ phi hình
thức như các chứng minh toán học thông thường mà con người vẫn thực hiện. Một
chứng minh tốt là một chứng minh mà những người khác có thể đọc được và hiểu
được. Các phê phán đối với cách tiếp cận này nói rằng tính đa nghĩa cố hữu trong ngôn
ngữ tự nhiên cho phép các lỗi sai trong các chứng minh đó có thể không bị phát hiện;
nhiều khi, những lỗi tinh vi có thể xuất hiện trong các chi tiết mức thấp mà thường
không được để ý đến bởi những chứng minh thuộc kiểu này. Ngoài ra, việc tạo ra các
chứng minh tốt đòi hỏi trình độ toán học cao.
Chương 2: Phương pháp hình thức Phạm Ngọc Thắng
6
2.2.3.1 Chứng minh tự động
Ngược lại, ngày càng có nhiều quan tâm đến các chứng minh về tính đúng đắn
của hệ thống bằng các phương tiện tự động. Các kỹ thuột tự động được phân thành hai
loại chính:
Chứng minh định lý tự động, trong đó, khi cho trước một mô tả về hệ thống,
một tập các tiên đề lôgic và một tập các quy tắc suy luận, một hệ thống sẽ cố gắng tự
xây dựng một chứng minh hình thức từ đầu.
Kiểm tra mô hình, trong đó, một hệ thống kiểm định các tính chất nhất định
bằng cách duyệt trong bộ tất cả các trạng thái mà trong thời gian chạy, hệ thống có thể
vào trạng thái đó.
Cả hai kỹ thuật trên đều hoạt động mà không cần đến sự hỗ trợ của con người.
Các bộ chứng minh định lý tự động thường yêu cầu định hướng xem các tính chất nào
là đáng quan tâm; các bộ kiểm tra mô hình có thể nhanh chóng sa lầy vào việc kiểm tra
hàng triệu trạng thái không đáng quan tâm nếu không được cho trước một mô hình đủ
trừu tượng.
Những người ủng hộ các hệ thống này cho rằng các kết quả của chúng có độ xác
t