đặc tả và kiểm chứng phần mềm sử dụng cafeobj

ĐẠ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