Bài giảng Đặc tả hình thức: Chương 0 - Nguyễn Thị Minh Tuyền

LOGO<br /> <br /> Đặc tả hình thức<br /> Tuần 1: Giới thiệu<br /> <br /> Nguyễn Thị Minh Tuyền<br /> <br /> Nguyễn Thị Minh Tuyền<br /> <br /> 1<br /> <br /> v Giảng viên lý thuyết:<br /> § <br /> § <br /> § <br /> § <br /> <br /> Nguyễn Thị Minh Tuyền<br /> FIT, trường ĐH Khoa học Tự nhiên tp Hồ Chí Minh<br /> Email: ntmtuyen@fit.hcmus.edu.vn<br /> Website: http://www.tuyennguyen.info/teaching.html<br /> •  Được cập nhật thường xuyên.<br /> <br /> v Giảng viên thực hành:<br /> <br /> Nguyễn Thị Minh Tuyền<br /> <br /> 2<br /> <br /> Đặc tả hình thức<br /> <br /> Thông tin về môn học và tài liệu<br /> v Không có giáo trình<br /> v Slide của môn này dựa vào slide của<br /> môn Formal Methods in Software<br /> Engineering của trường Đại học Iowa.<br /> v Sách tham khảo về kiến thức logic<br /> §  Logic in Computer Science. M. Huth and M. Ryan.<br /> Cambridge University Press, 2004 (2nd edition).<br /> §  Handbook of Practical Logic and Automated Reasoning.<br /> John Harrison. Intel Corporation, Portland, Oregon.<br /> <br /> Nguyễn Thị Minh Tuyền<br /> <br /> 3<br /> <br /> Đặc tả hình thức<br /> <br /> Mục tiêu của môn học<br /> v  Tập trung vào đặc tả hình thức.<br /> v  Giới thiệu thêm về phương pháp hình thức.<br /> v  Hiểu được phương pháp hình thức hỗ trợ cho việc tạo<br /> ra các phần mềm có chất lượng cao như thế nào.<br /> v  Học về mô hình hóa hình thức và các ngôn ngữ đặc<br /> tả.<br /> v  Viết và hiểu các đặc tả yêu cầu hình thức.<br /> v  Học về các phương pháp hình thức chính để kiểm<br /> định phần mềm.<br /> v  Biết được sử dụng phương pháp hình thức nào và khi<br /> nào.<br /> v  Sử dụng các công cụ tương tác và tự động để kiểm<br /> định mô hình và mã nguồn.<br /> Nguyễn Thị Minh Tuyền<br /> <br /> 4<br /> <br /> Đặc tả hình thức<br /> <br /> v Nội dung chính của môn này tập trung vào thiết<br /> kế ngữ nghĩa ở mức cao và các thuộc tính ở mức<br /> mã nguồn.<br /> v Nhấn mạnh và đặc tả dựa vào công cụ và các<br /> phương pháp thẩm định (validation methods)<br /> <br /> Nguyễn Thị Minh Tuyền<br /> <br /> 5<br /> <br /> Đặc tả hình thức<br /> <br />