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

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