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 .
