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

Thể loại Tài liệu miễn phí Kỹ thuật lập trình

Số trang 40

Ngày tạo 8/30/2018 5:43:37 AM +00:00

Loại tệp PDF

Kích thước

Tên tệp

Tải Bài giảng Đặc tả hình thức: Chương 1 - Nguyễn Thị ... (.pdf)

Xem mẫu

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

nguon tai.lieu . vn

Tin học văn phòng Đồ họa - Thiết kế - Flash Quản trị Web Cơ sở dữ liệu Quản trị mạng Kỹ thuật lập trình Hệ điều hành Phần cứng An ninh - Bảo mật Chứng chỉ quốc tế Thủ thuật máy tính Điện - Điện tử Kinh tế học Hoá học Xã hội học Môi trường