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

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