Tài liệu Phương pháp hình thức đặc tả hệ thống, hướng đối tượng dựa trên mô hình rCOS

PHƯƠNG PHÁP HÌNH THỨC ĐẶC TẢ HỆ THỐNG
HƯỚNG ĐỐI TƯỢNG DỰA TRÊN MÔ HÌNH rCOS
Nguyễn Mạnh Đức (Trường ĐH Sư phạm - ĐH Thái Nguyên)-
Đặng Văn Đức (Viện Công nghệ thông tin - Viện KH&CN Việt Nam)-
Nguyễn Văn Vỵ (Trường ĐH Công nghệ- ĐH Quốc gia Hà Nội)
1. Đặt vấn đề
Thiết kế và phát triển hệ thống phần mềm với ngôn ngữ hướng đối tượng đã được thừa
nhận là rất phức tạp [1, 4]. Nhiều nhà nghiên cứu đã chỉ ra sự cần thiết phát triển công cụ hình
thức hoá làm cơ sở cho việc phát triển phần mềm hướng đối tượng. Bài báo này sẽ trình bày một
qui trình làm mịn mô hình UML dựa trên lý thuyết lập trình thống nhất của Hoare và He [2], sử
dụng vào việc xây dựng một cách đúng đắn các chương trình hướng đối tượng.
Trong tiến trình phát triển thống nhất RUP (rational unified process) dựa trên ngôn ngữ
UML (unified modeling language) [1, 4, 7], một số mô hình loại khác nhau của UML đã được
sử dụng để biểu diễn các mô hình nghiệp vụ, mô hình phân tích, mô hình thiết kế và mô hình
triển khai trong pha khác nhau để phát triển hệ thống. Thí dụ, biểu đồ ca sử dụng biểu diễn mô
hình nghiệp vụ (khung nhìn nghiệp vụ), biểu đồ lớp biểu diễn mô hình phân tích (khung nhìn
tĩnh), biểu đồ công tác và biểu đồ trạng thái biểu diễn hành vi (khung nhìn hành vi) RUP sử
dụng đồng thời nhiều khung nhìn trong việc mô hình hoá hệ thống cho phép người phát triển có
thể phân chia mô hình hệ thống thành một số khung nhìn khác nhau để làm trực quan và quản lý
chúng theo những cách riêng. Mỗi khung nhìn đơn sẽ tập trung vào một khía cạnh riêng biệt ở
một giai đoạn, để phân tích và hiểu rõ các đặc trưng khác nhau của mô hình hệ thống. Tuy
nhiên, mô hình hệ thống với nhiều khung nhìn phải đối mặt với các khó khăn về sự khác nhau
của nhiều khung nhìn ở những thời điểm khác nhau của tiến trình phát triển. Một số vấn đề đã
được đặt ra cần giải quyết [12]:
1) Tính nhất quán ngang của mô hình: Nhiều khung nhìn khác nhau của các hệ con khác
nhau trong một hệ thống đòi hỏi phải tương thích với nhau về cú pháp và ngữ nghĩa.
2) Tính nhất quán dọc của mô hình: Khi biến đổi và phát triển một mô hình qua các
bước làm mịn, đòi hỏi các mô hình nhận được ở mỗi bước phải nhất quán và có ngữ nghĩa phù
hợp với nhau;
3) Tính lần vết được của mô hình: Khi chuyển từ một mô hình của một khung nhìn này
sang mô hình theo một khung nhìn khác, hay từ bước làm mịn này sang bước sau phải được chỉ
dẫn cho phép lần ngược lại mô hình loại trước hay mô hình ở bước trước, cũng như có thể lần
xuôi đến các mô hình của bước sau, và đảm bảo sự phù hợp giữa các mô hình đó.
4) Tích hợp được các mô hình: Mô hình của các khung nhìn khác nhau cần phải tích