LUẬN VĂN: ĐẶC TẢ VÀ KIỂM CHỨNG PHẦN MỀM SỬ DỤNG CafeOBJ

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...
Nội dung trích xuất từ tài liệu:
LUẬN VĂN:ĐẶ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ắngLờ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ệtDũ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ầytrong 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ọcQuốc Gia Hà Nội đã trang bị cho em những kiến thức quý báu trong thời gian em họctạ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ủamì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ọctậ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 iĐặc tả và kiểm chứng phần mềm sử dụng CafeOBJ Phạm Ngọc ThắngTó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óichung, 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ầnmề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ầnmề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ànhcô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àiluậ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ữngtiế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. iiĐặc tả và kiểm chứng phần mềm sử dụng CafeOBJ Phạm Ngọc ThắngMục lụcChươ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................................................................................................... 2Chươ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 ................................................................................... 6Chươ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 ...... ...