Giáo trình Đặc tả hình thức - Chương 0: Giới thiệu - Nguyễn Thị Minh Tuyền

Nội dung text: Giáo trình Đặc tả hình thức - Chương 0: Giới thiệu - Nguyễn Thị Minh Tuyền

1. LOGO Đặc tả hình thức Tuần 1: Giới thiệu Nguyễn Thị Minh Tuyền Nguyễn Thị Minh Tuyền 1
2. v Giảng viên lý thuyết: § Nguyễn Thị Minh Tuyền § FIT, trường ĐH Khoa học Tự nhiên tp Hồ Chí Minh § Email: ntmtuyen@fit.hcmus.edu.vn § Website: • Được cập nhật thường xuyên. v Giảng viên thực hành: Nguyễn Thị Minh Tuyền 2 Đặc tả hình thức
3. Thông tin về môn học và tài liệu v Không có giáo trình v Slide của môn này dựa vào slide của môn Formal Methods in Software Engineering của trường Đại học Iowa. v Sách tham khảo về kiến thức logic § Logic in Computer Science. M. Huth and M. Ryan. Cambridge University Press, 2004 (2nd edition). § Handbook of Practical Logic and Automated Reasoning. John Harrison. Intel Corporation, Portland, Oregon. Nguyễn Thị Minh Tuyền 3 Đặc tả hình thức
4. Mục tiêu của môn học v Tập trung vào đặc tả hình thức. v Giới thiệu thêm về phương pháp hình thức. v Hiểu được phương pháp hình thức hỗ trợ cho việc tạo ra các phần mềm có chất lượng cao như thế nào. v Học về mô hình hóa hình thức và các ngôn ngữ đặc tả. v Viết và hiểu các đặc tả yêu cầu hình thức. v Học về các phương pháp hình thức chính để kiểm định phần mềm. v Biết được sử dụng phương pháp hình thức nào và khi nào. v Sử dụng các công cụ tương tác và tự động để kiểm định mô hình và mã nguồn. Nguyễn Thị Minh Tuyền 4 Đặc tả hình thức
5. v Nội dung chính của môn này tập trung vào thiết kế ngữ nghĩa ở mức cao và các thuộc tính ở mức mã nguồn. v Nhấn mạnh và đặc tả dựa vào công cụ và các phương pháp thẩm định (validation methods) Nguyễn Thị Minh Tuyền 5 Đặc tả hình thức
6. Phần I: Thiết kế ở mức cao v Kiến thức chung về logic v Ngôn ngữ Alloy § Là ngôn ngữ mô hình hóa đơn giản cho thiết kế phần mềm. § Dễ dàng phân tích tự động một cách hoàn chỉnh § Nhắm vào việc diễn đạt các hành vi và ràng buộc cấu trúc phức tạp trong một hệ thống phần mềm. § Công cụ mô hình hóa trực quan sử dụng logic bậc nhất (first-order logic). § Phân tích tự động dùng SAT solving. v Sau khi học xong, SV sẽ biết § Thiết kế và mô hình hóa các hệ thống sử dụng ngôn ngữ Alloy § Kiểm tra mô hình và các thuộc tính của nó bằng Alloy Analyzer § Hiểu cái gì có thể và không thể diễn đạt được bằng Alloy. Nguyễn Thị Minh Tuyền 6 Đặc tả hình thức
7. Phần II: Đặc tả ở mức mã nguồn v Một số ngôn ngữ đặc tả ở mức mã nguồn: § JML (Java Modeling Language) (Java) § Dafny (C#) § Krakatoa (Java/C) § ACSL (ANSI/ISO C Specification Language)(C) § Nguyễn Thị Minh Tuyền 7 Đặc tả hình thức
8. Phần II: Đặc tả ở mức mã nguồn v Ngôn ngữ : JML (Java) § Dựa vào mô hình thiết kế dựa vào ràng buộc (design by contract). § Đặc tả được “nhúng” trong mã nguồn. § Nhiều công cụ kiểm thử có sẵn. v Sau khi học xong SV sẽ biết § Viết các ràng buộc và đặc tả hình thức dùng JML. § Hiểu mã nguồn và đặc tả được biểu diễn bằng logic như thế nào. § Kiểm thử các thuộc tính hàm của chương trình bằng các công cụ tự động. Nguyễn Thị Minh Tuyền 8 Đặc tả hình thức
9. Đánh giá môn học v Thực hành (30%). v Thi giữa kỳ (15%). v Thi cuối kỳ (60%). v Chuyên cần và tham gia xây dựng bài giảng (10%). Nguyễn Thị Minh Tuyền 9 Đặc tả hình thức
10. Quy định chung v Tuân thủ nghiêm túc các nội quy và quy định của Khoa và Trường. v Không được vắng quá 3 buổi trên tổng số các buổi học lý thuyết. v Không gian lận trong quá trình làm bài tập và trong thi cử. v Nộp bài tập đúng thời hạn quy định § Trừ 15% bài tập cho mỗi ngày nộp trễ. § Nộp trễ trên 4 ngày => 0 điểm. 10 Đặc tả hình thức
11. Quy định của môn học v Tắt điện thoại hoặc để điện thoại ở chế độ im lặng. v Không sử dụng điện thoại trong giờ học. v Không sử dụng máy tính bảng, máy tính xách tay và các thiết bị điện tử khác trong giờ học. v Không ăn vặt trong lớp. 11 Đặc tả hình thức