tailieunhanh - 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 .