LOGO
Đặc tả hình thức
Nguyễn Thị Minh Tuyền
Tổng quan
Nguyễn Thị Minh Tuyền 1
Đặc tả hình thức
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!
2
Nguyễn Thị Minh Tuyền
Đặ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.
3
Nguyễn Thị Minh Tuyền
Đặ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).
4
Nguyễn Thị Minh Tuyền
Đặ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 …
5
Nguyễn Thị Minh Tuyền