Xem mẫu

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

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:

Nguyễn Thị Minh Tuyền

2

Đặ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.

Nguyễn Thị Minh Tuyền

3

Đặ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.
Nguyễn Thị Minh Tuyền

4

Đặ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)

Nguyễn Thị Minh Tuyền

5

Đặc tả hình thức

nguon tai.lieu . vn