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,...
Nội dung trích xuất từ tài liệu:
Bài giảng Đặc tả hình thức: Chương 1 - Nguyễn Thị Minh Tuyền 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 thức