Đặc tả hình thức - Tuần 1: Giới thiệu - Nguyễn Thị Minh Tuyền

LOGO Đặc tả hình thức Nguyễn Thị Minh Tuyền Tuần 1: Giới thiệu Nguyễn Thị Minh Tuyền 1 Đặc tả hình thức 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: 2 Nguyễn Thị Minh Tuyền Đặc tả hình thức 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. 3 Nguyễn Thị Minh Tuyền Đặc tả hình thức 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. 4 Nguyễn Thị Minh Tuyền Đặc tả hình thức 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) 5 Nguyễn Thị Minh Tuyền Đặc tả hình thức 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. 6 Nguyễn Thị Minh Tuyền Đặc tả hình thức 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) §  7 Nguyễn Thị Minh Tuyền Đặc tả hình thức 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. 8 Nguyễn Thị Minh Tuyền Đặc tả hình thức Đá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%). 9 Nguyễn Thị Minh Tuyền Đặc tả hình thức 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 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 LOGO