[Bài Giảng] Chương 1-Tổng Quan

Nội dung

1. Mục tiêu của chương
2. Giới thiệu chung
3. Một số khái niệm cơ bản
4. Lịch sử ra đời và phát triển
5. Đặc tả và quy trình CNPM
6. Tóm tắt

Mục tiêu của chương
                                   

• Sau bài này, người học có thể:
• Nêu được ý nghĩa của 1 số thuật ngữ cơ bản dùng trong môn học Đặc tả hình thức.
• Trình bày được vai trò của các phương pháp hình thức trong các bước của quy trình phát triển phần mềm.
• Nêu lịch sử ra đời và phát triển của các ngôn ngữ hình thức, cũng như tính chất chung của chúng.
• Liệt kê được 1 số ngôn ngữ hình thức phổ biến hiện nay.

Giới thiệu chung

• Cung cấp các kiến thức liên quan đến hướng tiếp cận xây dựng phần mềm bằng phương pháp hình thức.
• Tiếp cận các cơ sở liên quan đến đặc tả hình thức như (tập hợp, hàm, dãy, v.v…)
• Cụ thể hóa việc đặc tả dùng các ngôn ngữ ĐTHT như Z và VDM

Một số khái niệm cơ bản

• Các phương pháp hình thức (formal methods)
• Đặc tả (specification)
• Đặc tả hình thức (formal specification)

Formal methods

• Thường bao gồm các công cụ như ngôn ngữ hình thức, đặc tả hình thức, v.v…
• Là thuật ngữ dùng để chỉ các kỹ thuật dựa trên cơ sở toán học dùng trong quá trình mô tả chi tiết (đặc tả), phát triển và kiểm chứng các hệ thống phần mềm cũng như phần cứng. 
• Thường áp dụng cho các hệ thống có kết cấu chặt chẽ, đòi hỏi độ tin cậy và tính an toàn cao.
• Đặc biệt hiệu quả trong các giai đoạn đầu của quá trình xây dựng hệ thống (xác định yêu cầu và đặc tả hệ thống) 
• Có thể được xếp loại theo 3 mức:
• Mức 0: Đặc tả hình thức được sử dụng để đặc tả hệ thống trước khi phát triển nó.
• Mức 1: Phát triển và kiểm chứng hình thức có thể được áp dụng để tạo ra một chương trình ( hay một hệ thống) một cách tự động, dựa trên các đặc tả hình thức đã có trước đó.
• Mức 2: Chứng minh tự động. 

Specification

• Đặc tả = Mô tả đặc tính / đặc điểm
• Đặc tả là mô tả các cấu trúc, hoạt động của các sự vật hiện tượng, quá trình nào đó.
• Sự mô tả này có thể đi từ khái quát đến cực kỳ chi tiết và chặt chẽ.
• Có nhiều ngôn ngữ cho phép đặc tả:
• Ngôn ngữ tự nhiên
• Ngôn ngữ toán
• Ngôn ngữ lập trình 
• Ngôn ngữ hình thức 

Formal Specification

• Đặc tả hình thức (ĐTHT) là đặc tả với các tính chất:
• Chính xác và nhất quán ( precise and consistent).
• Ngắn gọn nhưng đầy đủ (brief but complete).
• Có thể xử lý bởi máy vi tính. 

• Các ứng dụng của ĐTHT:
• Tạo ra các phác họa chi tiết, cụ thể và chặt chẽ về hệ thống sẽ được xây dựng.
• Là công cụ định hướng để đảm bảo hệ thống được xây dựng một cách phù hợp và đầy đủ.
• Là thước đo để kiểm chứng, khẳng định hệ thống được tạo ra có đúng đắn và tin cậy hay không. 

• Ví dụ: Đặc tả quy trình phát triển phần mềm theo mô hình thác nước (Waterfall).

• Cách 1: Dùng ngôn ngữ tự nhiên

1. Quy trình xây dựng phần mềm được tiến hành tuần tự qua các bước:
2. Xác định yêu cầu
3. Phân tích
4. Thiết kế
5. Lập trình
6. Kiểm chứng
7. Bảo trì
8. Sau khi tiến hành xong 1 bước sẽ chuyển giao kết quả cho bước kế tiếp hoặc có thể chuyển ngược lại cho các bước trước đó nếu còn phát hiện lỗi và sau quá trình lại tiếp tục. 

• Cách 2: Dùng sơ đồ

Lịch sử ra đời và phát triển

• Các phương pháp hình thức đã ra đời và được sử dụng trong suốt hơn 30 năm qua (từ đầu thập kỷ 70).
• Đa số các ngôn ngữ đặc tả đều dựa trên cơ sở toán học.
• Được sử dụng cho nhiều mục đích khác nhau.

• Các ngôn ngữ đặc tả được phân loại theo 3 tiêu chí chính:

1. Mức độ trừu tượng hóa
2. Phạm vi ứng dụng
3. Mục đích sử dụng
4. Mức độ trừu tượng hóa
5. Có thể được sử dụng để đặc tả các hệ thống với quy mô khác nhau, từ nhỏ đến lớn, từ đơn giản đến phức tạp.
6. Mức độ trừu tượng càng cao  càng cồng kềnh
7. Mức độ trừu tượng càng thấp  đơn giản và không có nhiều ứng dụng.

Phạm vi ứng dụng

• Các ngôn ngữ đặc tả thường chỉ được thiết kế để phục vụ cho 1 hay 1 số ít lĩnh vực cụ thể.
• VD:
• VDM dùng trong thiết kế mạch số.
• Logic mệnh đề dùng trong suy diễn và chứng minh tự động.
• UNITY dùng trong kiểm chứng hệ thống song song.
• v.v…

Mục đích sử dụng

• Ngôn ngữ đặc tả phục vụ cho 2 đối tượng chính: con người và máy tính!
• Vấn đề đặt ra là phải dung hòa:
• Gần với ngôn ngữ tự nhiên con người  khó xử lý.
• Gần với ngôn ngữ máy  khó học và sử dụng.

• Các ngôn ngữ đặc tả không hình thức:
• Thế hệ thứ nhất: Booch, Rumbaugh
• Thế hệ thứ hai: UML
• Thế hệ thứ ba: OOCL – Object-oriented Change and Learning (dùng trong khoa học nhận dạng và trí tuệ nhân tạo – biểu diễn tri thức).

Các ngôn ngữ đặc tả hình thức: 

• OCL, Predicate Calculus, CDM, UNITY
• VDM, Z
• Object-Z (Z++), VDM++
• Đặc tả và quy trình CNPM
• Phân tích
• Lập các mô hình thế giới thực
• Mô hình dữ liệu
• Các ràng buộc
• Mô hình xử lý
• Mô hình trạng thái
• Mô hình thời gian
• Mô hình không gian

Dùng đặc tả :

• Các sơ đồ
• Các phát biểu về ràng buộc
• Các quy định về công thức tính toán
• Thiết kế dữ liệu
• Các hàm kiểm tra ràng buộc 

Thiết kế

• Lập mô hình phần mềm

1. Hệ thống dữ liệu
2. Hệ thống giao diện
3. Hệ thống xử lý

• Dùng đặc tả 

1. Các sơ đồ
2. Các thao tác trên màn hình
3. Các hàm xử lý
4. Các hàm 

Kiểm chứng

• Kiểm tra tính đúng đắn

1. Dữ liệu
2. Hàm
3. Giao diện

• Dùng đặc tả 

1. Kiểm tra tính đúng đắn của hàm

Tóm tắt chương

1. Đặc tả hình thức là công việc mô tả cấu trúc, hoạt động của SV-HT 1 cách chặt chẽ, chính xác để có thể xử lý trên máy tính.
2. Đặc tả hình thức thường sử dụng các ngôn ngữ hình thức, đa số dựa trên cơ sở toán học.
3. Đặc tả hình thức đã và đang được ứng dụng trong nhiều công đoạn khác nhau của quy trình CNPM.
4. Có nhiều ngôn ngữ hình thức khác nhau, trong đó tiêu biểu là Z và VDM 

HẾT CHƯƠNG 1
(còn tiếp…)