TAILIEUCHUNG - Bài giảng Đặc tả hình thức: Chương 1 - Nguyễn Thị Minh Tuyền

Bài giảng Đặc tả hình thức: Chương 1 cung cấp cho người học các kiến thức: Phần mềm, thiệt hại về tiền của do lỗi phần mềm, lỗi phần mềm gây thiệt hại về tính mạng, lỗi hệ thống phần mềm, phương pháp hình thức,. | LOGO Đặc tả hình thức Tổng quan Nguyễn Thị Minh Tuyền Nguyễn Thị Minh Tuyền 1 Phần mềm v  Phần mềm ngày càng có ảnh hưởng lớn đến mọi mặt của cuộc sống §   Điều khiển quy trình (oil, gas, water, ) §   Giao thông vận tải (điều khiển không lưu, ) §   Chăm sóc y tế (quản lý bệnh nhân, điều khiển thiết bị, ) §   Tài chính (giao dịch tự động, bảo mật ngân hàng, ) §   Phòng thủ (điều khiển vũ khí, tên lửa, ) §   Sản xuất (lắp ráp, ) v  Lỗi phần mềm không những thiệt hại về tiền của mà còn thiệt hại về cả tính mạng con người! Nguyễn Thị Minh Tuyền 2 Đặc tả hình thức Thiệt hại về tiền của do lỗi phần mềm v  Hàng nghìn $ cho mỗi phút hệ thống sản xuất ngừng hoạt động. v  Mất một lượng lớn tiền của và trí tuệ đầu tư cho việc sửa lỗi §   Vụ nổ Ariane 5. v  Những thất bại về kinh doanh thương mại do lỗi phần mềm §   Ashton-Tate dBase. Nguyễn Thị Minh Tuyền 3 Đặc tả hình thức Lỗi phần mềm gây thiệt hại về tính mạng Những vấn đề tiềm tàng dễ thấy: v  Phần mềm được dùng để điều khiển nhà máy điện hạt nhân. v  Những hệ thống điều khiển không lưu. v  Điều khiển phóng tàu vũ trụ. v  Phần mềm nhúng trong xe hơi. v  Một số ví dụ nổi tiếng: §   Các lỗi trong máy bức xạ (radiation) Therac-25. §   Lỗi khi phóng tên lửa Patriot (1991). Nguyễn Thị Minh Tuyền 4 Đặc tả hình thức Lỗi hệ thống phần mềm Những lỗi nhỏ có thể gây nên thảm họa v  Vụ nổ Ariane 5 (1996) v   Lỗi phóng tên lửa chặn Patriot (1991) v  Mars Climate Orbiter (1999) v  London Ambulance Dispatch System v  Denver Airport Luggage Handling System v  Lỗi FDIV ở Intel Pentium (1994) v   Nguyễn Thị Minh Tuyền 5 Đặc tả hình .

• Kỹ thuật lập trình
• Bài giảng Đặc tả hình thức
• Đặc tả hình thức
• Hệ thống phần mềm
• Lỗi phần mềm
• Ngôn ngữ và hệ thống
• Các ngôn ngữ đặc tả
• Kiểm tra mô hình
• Đặc tả hàm
• Đặc tả đệ quy
• Đặc tả hàm tường minh
• Đặc tả hàm không tường minh
• Lập trình phần mềm
• Công nghệ phần mềm
• Đặc tả phần mềm
• Ngôn ngữ đặc tả hình thức
• Đặc tả yêu cầu phần mềm
• Bài giảng Đặc tả yêu cầu phần mềm
• Công nghệ phần mềm nâng cao
• Phân loại đặc tả yêu cầu phần mềm
• Đặc tả phi hình thức phần mềm
• Đặc tả hình thức phần mềm
• Mô hình Thế giới thực
• Quy trình công nghệ phần mềm
• Ngôn ngữ hình thức
• Thiết kế ở mức cao
• Đặc tả ở mức mã nguồn
• JML nâng cao
• Từ khóa chính trong JML
• Các tính năng nâng cao
• Đặc tả các ngoại lệ
• Thừa kế đặc tả
• Các trường model
• Đặc tả không hình thức
• Phép toán vị từ
• Cơ sở đặc tả hình thức
• Luật suy diễn
• Cơ sở toán học trong đặc tả hình thức
• Mô hình hóa dữ liệu
• Kiểu dữ liệu
• Đặc tả operation
• Dữ liệu kiểu mảng
• Kiểu đối tượng phức
• Kiểu tập hợp
• Design by contract
• Ngôn ngữ đặc tả
• Công cụ hỗ trợ
• Giới thiệu về ESC Java2
• Cách sử dụng và thuộc tính
• Cấu trúc của ESC
• Các file đặc tả
• Thủ thuật và cạm bẫy
• Đặc tả thừa kế
• Đặc tả sử dụng ánh xạ
• Kiểu ánh xạ
• Ngôn ngữ đặc tả Z
• Phép toán trên giản đồ