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: http://www.tuyennguyen.info/teaching.html
• Đượ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