TAILIEUCHUNG - Báo cáo " Nghiên cứu về chứng minh tự động (Theorem Proving) trong CafeOBJ"

Đặ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. Có thể chia đặc tả phần mềm ra làm hai loại: đặc tả phi hình thức là đặc tả dựa trên ngôn ngữ tự nhiên và đặc tả hình thức là đặc tả dựa trên kiến trúc toán học. Đặc tả phi hình thức không được chặt chẽ bằng đặc tả hình thức nhưng được nhiều người biết và có thể dùng để trao đổi với nhau để làm chính xác hóa các điểm chưa rõ,. | Nghiên cứu về chứng minh tự động Theorem Proving trong CafeOBJ Tạ Thị Thu Hiền Trường Đại học Công nghệ Luận văn Thạc sĩ ngành Công nghệ phần mềm Mã số 60 48 10 Người hướng dẫn TS. Phạm Ngọc Hùng Năm bảo vệ 2010 Abstract Chương 1 Giới thiệu. Chương 2 Tổng quan về 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 3 Đặc tả hệ thống đa tác tử và các thuộc tính. Chương 4 Mổ tả về phương pháp kiểm chứng hệ thống đa tác tử bằng ngôn ngữ CafeOBJ với tư tưởng quy nạp có thể kiểm chứng với không gian trạng thái là vô tận. Chương 5 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 Keywords Ngôn ngữ lập trình Phần mềm Hệ thống đa tác tử Content GIỚI THIỆU Đặ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. Có thể chia đặc tả phần mềm ra làm hai loại đặc tả phi hình thức là đặc tả dựa trên ngôn ngữ tự nhiên và đặc tả hình thức là đặc tả dựa trên kiến trúc toán học. Đặc tả phi hình thức không được chặt chẽ bằng đặc tả hình thức nhưng được nhiều người biết và có thể dùng để trao đổi với nhau để làm chính xác hóa các điểm chưa rõ chưa thống nhất giữa các bên phát triển hệ thống. Đặc tả hình thức là đặc tả mà ở đó các từ ngữ cú pháp ngữ nghĩa được định nghĩa hình thức dựa vào toán học. Đặc tả hình thức có thể coi là một phần của hoạt động đặc tả phần mềm. Trong đặc tả hình thức các đặc tả yêu cầu được phân tích chi tiết các mô tả trừu tượng của các chức năng chương trình có thể được tạo ra để làm rõ yêu cầu. Đặc tả phần mềm hình thức là một đặc tả được trình bày trên một ngôn ngữ bao gồm từ vựng cú pháp và ngữ nghĩa được định nghĩa. Định nghĩa ngữ nghĩa đảm bảo ngôn ngữ đặc tả không phải là ngôn ngữ tự nhiên mà dựa trên toán học. Các chức năng nhận các đầu vào trả lại các kết quả. Các chức năng có thể định ra các điều kiện tiền tố và hậu tố. Điều kiện tiền tố là điều kiện cần thỏa mãn để có dữ liệu vào

• Báo cáo khoa học
• chứng minh tự động
• công nghệ phần mềm
• quy trình kiểm thử
• nghiên cứu khoa học
• điện toán đám mây
• kiểm thử phần mềm
• Kiểm chứng chương trình
• Sinh điều kiện kiểm chứng
• Chứng minh định lý
• Phương pháp hình thức
• Định lý tự động
• Đòn bẩy tài chính
• Dòng tiền tự do
• Cấu trúc vốn
• Công ty niêm yết
• Sở Giao dịch Chứng khoán thành phố Hồ Chí Minh
• Tỷ lệ nợ trên vốn chủ sở hữu
• Tỷ lệ nợ dài hạn
• thành phố Hồ Chí Minh
• hướng dẫn thủ tục
• Văn phòng công chứng
• Bổ trợ tư pháp
• hành chính Hồ Chí Minh
• ĐỒ ÁN TỐT NGHIỆP
• kinh tế chính trị
• LỤC LƯỢNG SẢN XUẤT
• CHỦ NGHĨA TƯ BẢN
• Cácmac
• TỰ ĐỘNG HÓA
• Du lịch sinh thái dựa vào cộng đồng
• Sinh kế bền vững
• Hoạt động sinh kế
• Nguồn tài nguyên du lịch tự nhiên
• Cộng đồng dân cư
• Đòn bẩy công nghệ
• Phương pháp tạo ý tưởng kinh doanh
• Đòn bẩy Doanh nghiệp
• Đòn bẩy Bất động sản
• Đòn bẩy Nợ
• Đòn bẩy chứng khoán
• Chi tiêu thông minh
• Kiểm thử phần mềm Chương 2
• Nhập môn kiểm thử phần mềm
• Lỗi phần mềm
• Quy trình kiểm thử phần mềm
• Vai trò của kiểm thử phần mềm
• Nguyên lý của kiểm thử phần mềm
• Bài giảng Kiểm thử phần mềm
• Công cụ kiểm thử phần mềm
• Thiết kế phần mềm
• Kiểm soát chất lượng phần mềm
• Nguyên tắc kiểm thử phần mềm
• Sơ đồ tổ chức đội kiểm thử
• Môi trường kiểm thử
• Dữ liệu kiểm thử
• Thiết kế ca kiểm thử
• Kiểm thử chức năng phần mềm
• Kiểm thử cấu trúc phần mềm
• Kiểm thử luồng điều khiển
• Kỹ thuật kiểm thử
• Gia công phần mềm
• Quản lý kiểm thử phần mềm
• Công cụ kiểm thử tự động
• Kế hoạch kiểm thử phần mềm
• Thực hiện quy trình kiểm thử phần mềm
• Thiết kế kiểm thử
• Bài giảng Công cụ kiểm thử phần mềm
• Qui trình kiểm thử phần mềm
• Cấp độ kiểm thử
• Các loại kiểm thử
• Vòng đời phát triển phần mềm
• Cấu trúc dữ liệu phần mềm
• Tiến trình làm phần mềm
• Đánh giá chất lượng phần mềm
• Kiểm thử hiệu năng
• Thành phần kiểm thử hiệu năng
• Phân loại kiểm thử hiệu năng
• Báo cáo kiểm thử phần mềm
• Test summary report
• Vòng đời lỗi phần mềm
• Mức độ kiểm thử phần mềm
• Qui trình phát triển phần mềm
• Chiến lược kiểm thử
• Kỹ thuật thiết kế kiểm thử phần mềm
• Phương pháp kiểm thử phần mềm
• Khái niệm kiểm thử phần mềm
• Công cụ kiểm thử
• Xây dựng tài liệu kiểm thử
• Quản lý kiểm thử
• Lập kế hoạch kiểm thử
• Công cụ hỗ trợ kiểm thử
• Kiểm soát quá trình kiểm thử
• Báo cáo đề tài khoa học và công nghệ
• Kỹ thuật hệ thống
• Phần mềm kiểm thử
• Quy tình kiểm thử
• Hoạt động kiểm thử phần mềm
• Kiểm chứng Phần mềm
• Bài giảng Kiểm chứng Phần mềm
• Software Testing
• Nguyên lý kiểm thử phần mềm
• Kỹ thuật kiểm thử phần mềm
• Bài giảng Công nghệ phần mềm
• Kiểm chứng phần mềm
• Thiết kế kiểm thử phần mềm
• Phân hoạch tương đương
• Phân tích giá trị biên
• Trường hợp kiểm thử phần mềm
• Đầu vào Test case
• Cấu trúc Test case
• Cấu trúc Test result