›
›

Bài giảng Đặc tả hình thức - Chương 1: Tổng quan - Nguyễn Trần Thi Văn

ppt 27 trang phuongnguyen 3870
Download
Bạn đang xem 20 trang mẫu của tài liệu "Bài giảng Đặc tả hình thức - Chương 1: Tổng quan - Nguyễn Trần Thi Văn", để tải tài liệu gốc về máy bạn click vào nút DOWNLOAD ở trên

Tài liệu đính kèm:

  • pptbai_giang_dac_ta_hinh_thuc_chuong_1_tong_quan_nguyen_tran_th.ppt

Nội dung text: Bài giảng Đặc tả hình thức - Chương 1: Tổng quan - Nguyễn Trần Thi Văn

  1. Đại học Sư phạm Kỹ thuật TP. HCM Khoa Công nghệ Thông tin o0o BÀI GIẢNG MÔN ĐẶC TẢ HÌNH THỨC Chương 1 Tổng quan CBGD: Nguyễn Trần Thi Văn
  2. Monday, June 14, 2021 Nội dung 1. Mục tiêu của chương 2. Giới thiệu chung 3. Một số khái niệm cơ bản 4. Lịch sử ra đời và phát triển 5. Đặc tả và quy trình CNPM 6. Tóm tắt Đặc tả hình thức Tổng quan 2
  3. Monday, June 14, 2021 Mục tiêu của chương Sau bài này, người học có thể: • Nêu được ý nghĩa của 1 số thuật ngữ cơ bản dùng trong môn học Đặc tả hình thức. • Trình bày được vai trò của các phương pháp hình thức trong các bước của quy trình phát triển phần mềm. • Nêu lịch sử ra đời và phát triển của các ngôn ngữ hình thức, cũng như tính chất chung của chúng. • Liệt kê được 1 số ngôn ngữ hình thức phổ biến hiện nay. Đặc tả hình thức Tổng quan 3
  4. Monday, June 14, 2021 Giới thiệu chung • Cung cấp các kiến thức liên quan đến hướng tiếp cận xây dựng phần mềm bằng phương pháp hình thức. • Tiếp cận các cơ sở liên quan đến đặc tả hình thức như (tập hợp, hàm, dãy, v.v ) • Cụ thể hóa việc đặc tả dùng các ngôn ngữ ĐTHT như Z và VDM Đặc tả hình thức Tổng quan 4
  5. Monday, June 14, 2021 Một số khái niệm cơ bản • Các phương pháp hình thức (formal methods) • Đặc tả (specification) • Đặc tả hình thức (formal specification) Đặc tả hình thức Tổng quan 5
  6. Monday, June 14, 2021 Formal methods • Thường bao gồm các công cụ như ngôn ngữ hình thức, đặc tả hình thức, v.v • Là thuật ngữ dùng để chỉ các kỹ thuật dựa trên cơ sở toán học dùng trong quá trình mô tả chi tiết (đặc tả), phát triển và kiểm chứng các hệ thống phần mềm cũng như phần cứng. Đặc tả hình thức Tổng quan 6
  7. Monday, June 14, 2021 Formal methods (2) • Thường áp dụng cho các hệ thống có kết cấu chặt chẽ, đòi hỏi độ tin cậy và tính an toàn cao. • Đặc biệt hiệu quả trong các giai đoạn đầu của quá trình xây dựng hệ thống (xác định yêu cầu và đặc tả hệ thống) Đặc tả hình thức Tổng quan 7
  8. Monday, June 14, 2021 Formal methods (3) Có thể được xếp loại theo 3 mức: – Mức 0: Đặc tả hình thức được sử dụng để đặc tả hệ thống trước khi phát triển nó. – Mức 1: Phát triển và kiểm chứng hình thức có thể được áp dụng để tạo ra một chương trình ( hay một hệ thống) một cách tự động, dựa trên các đặc tả hình thức đã có trước đó. – Mức 2: Chứng minh tự động. Đặc tả hình thức Tổng quan 8
  9. Monday, June 14, 2021 Specification • Đặc tả = Mô tả đặc tính / đặc điểm • Đặc tả là mô tả các cấu trúc, hoạt động của các sự vật hiện tượng, quá trình nào đó. • Sự mô tả này có thể đi từ khái quát đến cực kỳ chi tiết và chặt chẽ. Đặc tả hình thức Tổng quan 9
  10. Monday, June 14, 2021 Specification (2) Có nhiều ngôn ngữ cho phép đặc tả: • Ngôn ngữ tự nhiên • Ngôn ngữ toán • Ngôn ngữ lập trình • Ngôn ngữ hình thức Đặc tả hình thức Tổng quan 10
  11. Monday, June 14, 2021 Formal Specification • Đặc tả hình thức (ĐTHT) là đặc tả với các tính chất: – Chính xác và nhất quán ( precise and consistent). – Ngắn gọn nhưng đầy đủ (brief but complete). – Có thể xử lý bởi máy vi tính. Đặc tả hình thức Tổng quan 11
  12. Monday, June 14, 2021 Formal Specification (2) Các ứng dụng của ĐTHT: – Tạo ra các phác họa chi tiết, cụ thể và chặt chẽ về hệ thống sẽ được xây dựng. – Là công cụ định hướng để đảm bảo hệ thống được xây dựng một cách phù hợp và đầy đủ. – Là thước đo để kiểm chứng, khẳng định hệ thống được tạo ra có đúng đắn và tin cậy hay không. Đặc tả hình thức Tổng quan 12
  13. Monday, June 14, 2021 Formal Specification (3) Ví dụ: Đặc tả quy trình phát triển phần mềm theo mô hình thác nước (Waterfall). Đặc tả hình thức Tổng quan 13
  14. Monday, June 14, 2021 Formal Specification (4) Cách 1: Dùng ngôn ngữ tự nhiên • Quy trình xây dựng phần mềm được tiến hành tuần tự qua các bước: – Xác định yêu cầu – Phân tích – Thiết kế – Lập trình – Kiểm chứng – Bảo trì • Sau khi tiến hành xong 1 bước sẽ chuyển giao kết quả cho bước kế tiếp hoặc có thể chuyển ngược lại cho các bước trước đó nếu còn phát hiện lỗi và sau quá trình lại tiếp tục. Đặc tả hình thức Tổng quan 14
  15. Monday, June 14, 2021 Formal Specification (5) Cách 2: Dùng sơ đồ Xác định Phân tích Thiết kế Lập trình Kiểm chứng Bảo trì Giai đoạn Chuyển kết quả Đặc tả hình thức Tổng quan 15
  16. Monday, June 14, 2021 Lịch sử ra đời và phát triển • Các phương pháp hình thức đã ra đời và được sử dụng trong suốt hơn 30 năm qua (từ đầu thập kỷ 70). • Đa số các ngôn ngữ đặc tả đều dựa trên cơ sở toán học. • Được sử dụng cho nhiều mục đích khác nhau. Đặc tả hình thức Tổng quan 16
  17. Monday, June 14, 2021 Lịch sử ra đời và phát triển (2) • Các ngôn ngữ đặc tả được phân loại theo 3 tiêu chí chính: – Mức độ trừu tượng hóa – Phạm vi ứng dụng – Mục đích sử dụng Đặc tả hình thức Tổng quan 17
  18. Monday, June 14, 2021 Mức độ trừu tượng hóa • Có thể được sử dụng để đặc tả các hệ thống với quy mô khác nhau, từ nhỏ đến lớn, từ đơn giản đến phức tạp. • Mức độ trừu tượng càng cao → càng cồng kềnh • Mức độ trừu tượng càng thấp → đơn giản và không có nhiều ứng dụng. Đặc tả hình thức Tổng quan 18
  19. Monday, June 14, 2021 Phạm vi ứng dụng • Các ngôn ngữ đặc tả thường chỉ được thiết kế để phục vụ cho 1 hay 1 số ít lĩnh vực cụ thể. • VD: – VDM dùng trong thiết kế mạch số. – Logic mệnh đề dùng trong suy diễn và chứng minh tự động. – UNITY dùng trong kiểm chứng hệ thống song song. – v.v Đặc tả hình thức Tổng quan 19
  20. Monday, June 14, 2021 Mục đích sử dụng • Ngôn ngữ đặc tả phục vụ cho 2 đối tượng chính: con người và máy tính! • Vấn đề đặt ra là phải dung hòa: – Gần với ngôn ngữ tự nhiên con người → khó xử lý. – Gần với ngôn ngữ máy → khó học và sử dụng. Đặc tả hình thức Tổng quan 20
  21. Monday, June 14, 2021 Lịch sử ra đời và phát triển (3) Các ngôn ngữ đặc tả không hình thức: • Thế hệ thứ nhất: Booch, Rumbaugh • Thế hệ thứ hai: UML • Thế hệ thứ ba: OOCL – Object-oriented Change and Learning (dùng trong khoa học nhận dạng và trí tuệ nhân tạo – biểu diễn tri thức). Các ngôn ngữ đặc tả hình thức: • OCL, Predicate Calculus, CDM, UNITY • VDM, Z • Object-Z (Z++), VDM++ Đặc tả hình thức Tổng quan 21
  22. Monday, June 14, 2021 Đặc tả và quy trình CNPM Thế giới thực Mô hình TG thực Phân tích Xác định yêu cầu Thiết kế Người Mô hình phần mềm Lập trình Kiểm chứng Phần mềm Phần mềm với độ tin cậy Đặc tả hình thức Tổng quan 22
  23. Monday, June 14, 2021 Phân tích • Lập các mô hình thế giới thực – Mô hình dữ liệu – Các ràng buộc – Mô hình xử lý – Mô hình trạng thái – Mô hình thời gian – Mô hình không gian • Dùng đặc tả : – Các sơ đồ – Các phát biểu về ràng buộc – Các quy định về công thức tính toán – Thiết kế dữ liệu – Các hàm kiểm tra ràng buộc Đặc tả hình thức Tổng quan 23
  24. Monday, June 14, 2021 Thiết kế • Lập mô hình phần mềm – Hệ thống dữ liệu – Hệ thống giao diện – Hệ thống xử lý • Dùng đặc tả – Các sơ đồ – Các thao tác trên màn hình – Các hàm xử lý – Các hàm Đặc tả hình thức Tổng quan 24
  25. Monday, June 14, 2021 Kiểm chứng • Kiểm tra tính đúng đắn – Dữ liệu – Hàm – Giao diện • Dùng đặc tả – Kiểm tra tính đúng đắn của hàm Đặc tả hình thức Tổng quan 25
  26. Monday, June 14, 2021 Tóm tắt chương – Đặc tả hình thức là công việc mô tả cấu trúc, hoạt động của SV-HT 1 cách chặt chẽ, chính xác để có thể xử lý trên máy tính. – Đặc tả hình thức thường sử dụng các ngôn ngữ hình thức, đa số dựa trên cơ sở toán học. – Đặc tả hình thức đã và đang được ứng dụng trong nhiều công đoạn khác nhau của quy trình CNPM. – Có nhiều ngôn ngữ hình thức khác nhau, trong đó tiêu biểu là Z và VDM Đặc tả hình thức Tổng quan 26
  27. Monday, June 14, 2021 HẾT CHƯƠNG 1 (còn tiếp ) Đặc tả hình thức Tổng quan 27