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

T¹p chÝ Khoa häc & C«ng nghÖ - Sè 1(45) Tập 2/N¨m 2008 
 95
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 hợp 
đảm bảo sự nhất quán và đồng bộ toàn hệ thống trước khi có sản phNm phần mềm cuối cùng... 
Nhiều nghiên cứu về tính chất và hình thức thể hiện của các mô hình UML [10, 12] đã 
được tiến hành trong những năm gần đây. Tuy nhiên, phần lớn các nghiên cứu chỉ liên quan tới 
hình thức của từng loại biểu đồ riêng rẽ và tính nhất quán của các mô hình loại 1 hoặc loại 2. 
T¹p chÝ Khoa häc & C«ng nghÖ - Sè 1(45) Tập 2/N¨m 2008 
 96 
Nhìn lại tiến trình phát triển hệ thống phần mềm theo hướng đối tượng theo RUP ta thấy, 
bắt đầu của tiến trình phát triển với khung nhìn nghiệp vụ, có chứa mô hình lớp khái niệm, và 
cho đến khi kết thúc tiến trình trước khi chuyển sang mã nguồn, chúng ta lại nhận được biểu đồ 
lớp thiết kế của hệ thống phần mềm. Nếu ta chỉ sử dụng một khung nhìn duy nhất được biểu 
diễn bằng các biểu đồ lớp, ta sẽ khắc phục được tính đa khung nhìn của tiến trình phát triển ở 
trên. Vấn đề duy nhất còn cần phải giải quyết ở đây là: làm sao xây dựng được các phép biến 
đổi và các quy tắc kiểm tra sự đúng đắn của chúng, khi đó bằng một loạt các phép biến đổi đúng 
đắn, ta có thể chuyển biểu đồ lớp khái niệm ban đầu thành biểu đồ lớp thiết kế cuối cùng của 
phần mềm hệ thống (hình vẽ dưới đây) [16, 17]. 
Lúc này, các khung nhìn khác của tiến trình RUP sẽ được sử dụng như các công cụ trợ giúp 
cho việc xác định các phép biến đổi cụ thể để tận dụng được thế mạnh của các khung nhìn này. Vấn 
đề cuối cùng đặt ra được giải quyết bằng công cụ hình thực hóa dựa trên các quan hệ đại số. 
Nhìn trến sơ đồ ta thấy, để đạt đến biểu đồ lớp thiết kê cuối cùng, chúng ta cần đến các 
phép biến đổi sau: thêm lớp (có thể kế thừa), thêm thuộc tính, thêm phương thức, thay đổi đặc 
trưng của thuộc tính, của phương thức, thay đổi liên kết giữa các lớp và các biến đổi tương ứng 
trong mỗi phương thức. 
2. Cơ sở của các phép biến đổi 
Một biểu diễn của chương trình lệnh được coi như một thiết kế (design) xác định bởi 
cặp (α, P) [2, 3], ở đây α biểu thị tập các biến đã biết trong thiết kế, được gọi là bảng ký 
kiệu của thiết kế; P là các toán tử xác định quan hệ giữa các giá trị ban đầu của các biến và 
các giá trị kết quả của nó, ta ký hiệu quá trình biến đổi như sau: p(x) ├ R(x, x’), cụ thể hơn 
như sau: 
p(x) ├ R(x, x’) def
 ok ∧ p(x) ⇒ ok’∧ R(x, x’) 
Trong đó: p(x) được gọi là tiền điều kiện và phải có giá trị true – tức là đúng đắn trước 
khi chương trình bắt đầu. R(x, x’) gọi là hậu điều kiện nhận được sau khi chương trình thực 
hiện. x và x’ biểu diễn giá trị khởi đầu và kết thúc của biến x trong chương trình. ok và ok’ là 
các biến logic mô tả trạng thái hành vi ban đầu và cuối của chương trình: nếu chương trình được 
kích hoạt hợp thức ok là true, nếu việc thực hiện chương trình cuối cùng thành công ok’ là true, 
ngược lại chúng là false. 
biểu đồ lớp 
khái niệm 
miền lĩnh 
vực 
biểu đồ lớp 
thiết kế phần 
mềm hệ 
thống 
phép 
BĐ1 
biểu đồ 
lớp được 
làm mịn 1 
phép 
BĐ2 
phép 
BĐn 
mô hình 
nghiệp vụ 
khung 
nhìn 1 
mô hình 
phân tích 
khung 
nhìn 2 
mô hình 
thiết kế 
khung 
nhìn k 
Ý tưởng cho phương pháp giải quyết vấn đề 
Tiến 
trình 
RUP 
Phương 
pháp 
mới 
T¹p chÝ Khoa häc & C«ng nghÖ - Sè 1(45) Tập 2/N¨m 2008 
 97
2.1. Mô tả hệ thống hướng đối tượng 
Một hệ thống hoặc chương trình hướng đối tượng S có dạng cdecls ● P , ở đây: cdecls là 
phần khai báo một số hữu hạn các lớp; P được gọi là phương thức chính và có dạng (glb, c), 
trong đó glb là tập hữu hạn các biến chung và kiểu dữ liệu của chúng, còn c là các lệnh. P có thể 
dược hiểu như là phương thức chính nếu S được tạo bởi ngôn ngữ giống như Java. Phần khai 
báo lớp cdecls là thứ tự của các khai báo lớp cdecl1; ...; cdeclk,. Ở đây mỗi khai báo lớp cdecli 
có dạng như sau: 
[private] class N [extends M] { 
pri : T1 t1 = a1 ..., Tm tm = am; 
pro : U1 u1 = b1 ..., Un un = bn; 
pub : V1 v1 = d1 ..., Vk vk = dk; 
meth : m1 (T11 x11, T12 y12, T13 z13) { c1 }; 
 ... ; 
 mℓ (Tℓ1 xℓ1, Tℓ2 yℓ2, Tℓ3 zℓ3) { cℓ } 
} 
trong đó: 
1. Mỗi lớp có thể được khai báo private hoặc là public, ngầm định là public. Chỉ các lớp có 
kiểu public hoặc kiểu cơ sở mới được sử dụng trong các khai báo biến chung glb. 
2. N và M là các tên lớp khác nhau và M được gọi là lớp cha của N. 
3. Phần pri khai báo các thuộc tính private của lớp, bao gồm kiểu và các giá trị khởi tạo. 
Tương tự, các phần pro và pub khai báo các thuộc tính protected và public của lớp. 
4. Phần method khai báo các phương thức của lớp N, trong đó m1, m2, ..., mℓ là các phương 
thức, ở đây (Ti1 xi1), (Ti2 yi2), (Ti3 zi3) và ci biểu diễn các tham biến giá trị, các tham biến kết 
quả, các tham biến giá trị kết quả và phần thân của phương thức mi. Phương thức có thể được 
chỉ ra bởi biểu diễn m(paras){c}, trong đó paras là các tham biến và c là thân lệnh của m. 
Khi viết các luật làm mịn, ký pháp sau được sử dụng để chỉ sự khai báo lớp N: N [M, pri, 
pro, pub, op]. Trong đó, M là tên lớp cha của N; pri, pro và pub là các tập thuộc tính private, 
protected và public của N; còn op là tập các phương thức của N. Ta có thể chỉ đưa ra các tham 
số liên quan cần thiết chẳng hạn như: nếu sử dụng N[op] để chỉ lớp N với tập các phương thức 
op, N[pro, op] chỉ lớp N với các thuộc tính protected là pro và tập các phương thức là op. 
2.2. Mô tả biểu thức 
Biểu thức trong ngôn ngữ hướng đối tượng có thể xuất hiện vế bên phải của các lệnh 
gán, xác định theo các qui tắc như sau [2, 5]: 
e ::= x | null | self | e.a | e is C | C(e) | f(e) 
Trong đó x là biến đơn, null là kiểu đối tượng đặc biệt, lớp đặc biệt NULL là lớp con 
của mọi lớp và null là duy nhất, self được sử dụng để chỉ đối tượng hoạt động trong phạm vi 
hiện tại, e.a là thuộc tính a của e, e is C là kiểu kiểm thử (test), C(e) là biểu thức có kiểu theo 
khuôn mẫu, f(e) là phép toán gắn liền với các kiểu nguyên thuỷ. 
2.3. Mô tả các lệnh 
Phần này xét các lệnh hỗ trợ việc xây dựng chương trình hướng đối tượng tiêu biểu [2, 5]. 
T¹p chÝ Khoa häc & C«ng nghÖ - Sè 1(45) Tập 2/N¨m 2008 
 98 
c ::= skip | chaos | var T x = e | end x bỏ qua| không xác định khai báo | kết thúc khai báo 
 c; c | c
bc | c ⊓ c | b*c tuần tự| chọn theo điều kiện| không tiền định| lặp 
 le.m(e, v, u) | le:=e | C.new(x) gọi phương thức | gán| tạo đối tượng mới. 
Ở đây b là biểu thức logic, c là lệnh, e là một biểu thức, le có thể xuất hiện ở vế trái của 
phép gán và có dạng le ::= x|le.a với x là biến đơn còn a là thuộc tính của đối tượng. Đa số các 
lệnh có ý nghĩa tương tự như trong các ngôn ngữ lệnh (có thể xem chi tiết trong [2, 5]). Sau đây 
là các giải thích một số lệnh đặc trưng cho chương trình hướng đối tượng. 
Lệnh gán le := e được xác định đúng khi le và e đã được xác định đúng và kiểu của e là 
kiểu con của kiểu đã được khai báo le. Trong trường hợp lệnh gán đơn x := e, khi lệnh gán được 
xác định đúng nó chỉ thay đổi x bởi gán x bằng giá trị của e. Trong trường hợp sự thay đổi thuộc 
tính của đối tượng, le.a := e thay thuộc tính a của đối tượng le bằng giá trị e. 
 Phương thức gọi le.m(e, v, vr) xác định đúng nếu le là đối tượng không rỗng và m(x, y, 
z) là phương thức đã được khai báo trong kiểu le. Khi nó đã được xác định đúng, việc thực hiện 
các lệnh gán các giá trị của các tham số thực v và vr cho các tham số hình thức x và z của m 
của các đối tượng hoạt động le tham chiếu tới, rồi thực hiện thân của phương thức trong môi 
trường của lớp đối tượng hoạt động. Sau khi thực hiện các thân cuối cùng, giá trị của tham biến 
kết quả và tham biến giá trị kết quả y và z được trả lại hợp qui cách với các tham số thực r và vr. 
Lệnh tạo đối tượng mới C.new(x) được xác định đúng nếu C là lớp đã được khai báo. Sự 
thực hiện lệnh này sẽ tạo ra một đối tượng mới của lớp C với biến tham chiếu là x và gắn giá trị 
khởi đầu của các thuộc tính trong lớp C với giá trị các thuộc tính của x. 
3. Các phép biến đổi làm mịn mô hình hệ thống đối tượng 
3.1. Các khái niệm 
Sau đây ta xem xét một số khái niệm liên quan tới quá trình làm mịn mô hình hệ thống 
[3, 9, 11, 13, 14]: 
Định nghĩa 1 (làm mịn thiết kế): Thiết kế D2 = (α, P2) là làm mịn của thiết kế D1=(α, 
P1) được ký hiệu là: D1 ⊑ D2, nếu P2 dẫn tới P1, nghĩa là: ∀x, x’, ..., z, z’, ok, ok’: (P2 ⇒ P1). 
Ở đây x, ..., z là các biến chứa trong α.. D1≡ D2 nếu và chỉ nếu D1⊑ D2 và D2 ⊑ D1. 
Định nghĩa 2 (làm mịn dữ liệu): Cho ρ là ánh xạ α2 tới α1. Thiết kế D2 = (α2, P2) là 
làm mịn của thiết kế D1 = (α1, P1) dưới ρ, được ký hiệu là D1⊑ρ D2, nếu (ρ; P1)⊑ (ρ;P2). 
Trong trường hợp này ρ được gọi là ánh xạ làm mịn. 
Định nghĩa 3 (làm mịn hệ thống): Cho S1 và S2 là các đối tượng chương trình có cùng 
một tập các biến chung glb. S2 là làm mịn của S1, được chỉ ra bởi S1 ⊑sys S2, nếu hành vi của 
nó có thể kiểm soát và dự đoán nhiều hơn trong S1, tức là: ∀ x, x’, ok, ok’: (S2⇒ S1) 
 Ở đây x là các biến trong glb.Ý nghĩa này là hành vi mở rộng của S1, đó là các cặp tiền 
điều kiện và hậu điều kiện của các biến chung là tập con của S2. Để phạm vi của S1 và S2 được 
làm mịn là khác nhau, ta yêu cầu chúng phải có cùng tập các biến chung và tồn tại ánh xạ làm 
mịn từ các biến của S1 tới S2 trên tập các biến chung đó. 
Định nghĩa 4 (làm mịn lớp): Cho cdecls1 và cdecls2 là hai khai báo. cdecls2 là làm 
mịn của cdecls1, đượcký hiệu lài cdecls2 ⊒class cdecls1 nếu như phần trước có thể thay thế 
T¹p chÝ Khoa häc & C«ng nghÖ - Sè 1(45) Tập 2/N¨m 2008 
 99
phần sau trong bất kỳ hệ thống đối tượng: cdecls2 ⊒class cdecls1 def ∀P . (cdecls2• P ⊒sys 
cdecls1• P). Ở đây P đóng vai trò cho phương thức chính (glb, c). 
Phương thức chính tương ứng với chương trình ứng dụng đang sử dụng các dịch vụ Do 
đó, ở đây ta chỉ quan tâm làm mịn giữa các phần khai báo. 
3.2. Xây dựng qui trình làm mịn mô hình 
Quá trình làm mịn được thực hiện theo các luật làm mịn đã được đã được xác định [3, 10, 11]. 
3.2.1. Xây dựng hệ thống khởi tạo ban đầu 
Mô hình hệ thống khởi tạo ban đầu còn gọi là mô hình khái niệm thô, đó chính là mô 
hình lĩnh vực miềm, mô tả các khái niệm quan trọng của hệ thống qua các đối tượng của lĩnh 
vực nghiệp vụ và các liên kết giữa chúng với nhau. 
Thuật toán bổ sung các lớp vào mô hình khởi tạo: 
Công việc đầu tiên là tạo mô hình khởi tạo của hệ thống, cụ thể là bổ sung tên các lớp Ni 
đặc trưng cho các đối tượng miền lĩnh vực vào biểu đồ lớp của mô hình hệ thống có dạng: 
APP0 = N1[]; N2[]; ...; Nk[] 
và xác định những quan hệ giữa các Ni. Phép biến đổi này được thực hiện bằng thuật toán 
addClassName như sau: 
// Thuật toán addClassName- bổ sung các lớp vào mô hình 
Input: Một tên xâu cho định danh cho lớp Ni. 
Output: Lớp Ni trống (chưa có các thuộc tính hoặc phương thức). 
Format: addClassName () 
Method: 
var stop: Boolean, s: String; 
stop := false; 
while ¬ stop do { 
 read(s); 
 if {(s ””) → AdditionClassName(s)} fi; 
 read(stop); 
} 
end stop, s; 
End. 
Ở đây, cấu trúc if {(bi → Pi) | 1 ≤ i ≤ n} fi là sự thực hiện liên tiếp có điều kiện. Trong 
đó, mỗi Pi được chọn để thực hiện nếu bi là true. Khi mọi bi là false thì kết quả là chaos [2]. 
Phep bổ sung lớp này sẽ được dùng cho việc bổ sung tiếp tục các lớp sau này vào hệ thống. 
3.2.2. Xây dựng các biến đổi làm mịn mô hình khái niệm hệ thống [14, 16, 17] 
Thuật toán bổ sung các thuộc tính cho lớp: 
Khi đã có một lớp, ta cần xác định và bổ sung các thuộc tính private và định dạng các 
kiểu cho nó. (khi không giả thiết gì, thuộc tính trong lớp mặc định là private). Việc thêm một 
thuộc tính thành phần vào một lớp có thể được thực hiện theo luật bổ sung sau: 
 Ni[]; cdecls ⊑ Ni[pri ]; cdecls 
T¹p chÝ Khoa häc & C«ng nghÖ - Sè 1(45) Tập 2/N¨m 2008 
 100
Trong đó T là một kiểu dữ liệu của thuộc tính attributeName và d là giá trị khởi đầu 
nếu cần. Với mỗi lớp, thực hiện nhiều lần luật này để bổ sung đầy đủ các thuộc tính cho nó. Quá 
trình này có thể được mô tả bẳng thuật toán hình thức như sau: 
// Thuật toán addAttributeName- bổ sung các thuộc tính vào lớp 
Input: Một lớp Ni của hệ thống, . 
Output: Lớp Ni bao gồm các thuộc tính kiểu private cần thiết. 
Format: addAttributeName () 
Method: 
var stop: Boolean, s: String; 
 stop := false; 
while ¬ stop do { 
read(s); 
if {(s ””) → 
AdditionAttributeName(s)} fi; 
read(stop); 
} 
end stop, s; 
End. 
Thực hiện k lần thuật toán này để bổ sung các thuộc tính cho k lớp của hệ thống. 
Thuật toán chuyên đổi kiểu thuộc tính: 
Tiếp theo là chuyển các thuộc tính kiểu private cần thiết sang kiểu protected để được hỗ 
trợ các dịch vụ nhiều hơn. Muốn vậy, ta sẽ áp dụng luật chuyển đổi kiểu thuộc tính sau: 
Ni[pri ]; cdecls ⊑ Ni[pro ]; cdecls 
Việc chuyển thuộc tính kiểu private trong một lớp sang kiểu protected theo thuật toán sau: 
// Thuật toán priAttToproAtt, chuyển kiểu thuộc tính private thành protected 
Input: Một lớp khái niệm Ni của hệ thống ứng dụng. 
Output: Lớp Ni bao gồm các thuộc tính kiểu protected cần thiết. 
Format: priAttiToproAtt () 
Method: 
var stop: Boolean, ok: Boolean; 
stop := false; ok := false; 
while ¬ stop do { 
if {(type(Ni.AttributeName) = private) → 
{ Question (ok); 
 if {ok=true → 
 priTopro(Ni.AttributeName)}fi; 
} fi; 
 read(stop); 
} 
end stop, ok; 
End. 
T¹p chÝ Khoa häc & C«ng nghÖ - Sè 1(45) Tập 2/N¨m 2008 
 101
Bằng cách tương tự, ta cũng có thể xây dựng các thuật toán chuyển kiểu thuộc tính protected 
sang kiểu public. Sau mỗi bước thực hiện các công việc làm mịn trên sẽ thu được một mô hình 
thống mới và ta có: Mô hình khái niệm thô ⊑ Mô hình khái niệm mịn ban đầu. 
3.2.3. Xây dựng mô hình thiết kế ban đầu cho hệ thống 
Thuật toán bổ sung các phương thức cho lớp: 
Mô hình thiết kế là mô hình gồm các lớp có chứa đầy đủ thuộc tính và phương thức. Bằng 
cách bổ sung các phương thức cho các lớp của mô hình khái niệm ta được mô hình thiết kế. Có 
thể áp dụng các luật bổ sung phương thức như sau: 
N[op]; cdecls ⊑ N[op ∪ m(paras) {c}]; cdecls 
Thuật toán bổ sung các phương thức vào một lớp có thể viết như sau: 
// Thuật toán addMethodName- bổ sung các phương thức vào lớp 
Input: Một lớp Ni của hệ thống ứng dụng. 
Output: Lớp Ni bao gồm các phương thức cần thiết. 
Format: addMethodName () 
Method: 
var stop: Boolean, s: String, paras: String; 
stop := false; 
while ¬ stop do { 
read(s, paras); 
if {(s ””) → 
 AdditionMethodName(s, paras)} fi; 
read(stop); 
} 
end stop, s, paras; 
End. 
Sau phép biến đổi này ta có: Mô hình khái niệm mịn ⊑ Mô hình thiết kế ban đầu. 
3.2.4. Làm mịn mô hình thiết kế hệ thống 
Các công việc trong phần này tuỳ thuộc nhiều vào bài toán nghiệp vụ cụ thể đặt ra. Trong 
bước này chúng ta có thể áp dụng nhiều luật làm mịn khác nhau để làm mịn dần hệ thống từ mô 
hình thô về dạng sát với mã trình có thể thực hiện được, tạo điều kiện thuận lợi cho quá trình dịch 
xuôi từ mô hình UML sang một ngôn ngữ hướng đối tượng mà nó hỗ trợ. Ở đây cần thực hiện các 
luật khác nhau để làm mịn dần cho hệ thống với các thao tác biến đổi sau đây [3, 11]: 
- Làm mịn các phần thân phương thức m(){c} trong các lớp: Áp dụng luật Extract 
Method, Move Method, Add Parameter  
- Chuyển thuộc tính từ một lớp tới lớp khác: Ápdụng luật Move Field [11], để chuyển 
thuộc tính từ một lớp sang lớp khác như sau: 
cdecl; M[b: N, a: T, op]; N[] ⊒ cdecls; M[b: N, op]; N[a: T] 
- Xây dựng các thừa kế cho các lớp: Áp dụng các luật tạo quan hệ giữa các lớp, chế tác lại 
định hướng mẫu, như Decorator, Strategy, luật thay thế điều kiện bằng tính đa hình ... 
T¹p chÝ Khoa häc & C«ng nghÖ - Sè 1(45) Tập 2/N¨m 2008 
 102
Với mỗi hệ thống ứng dụng cụ thể, ta có thể linh hoạt áp dụng các luật làm mịn khác 
nhau đã trình bày ở trên để biến đổi dần hệ thống cho bài toán đặt ra. Khi kết thúc các phép 
biến đổi, ta sẽ có một hệ thống bao gồm các lớp thiết kế với đầy đủ thuộc tính và phương 
thức. Do quá trình biến đổi thực hiện đảm bảo tính đúng đắng, nhất quán và phù hợp, nên hệ 
thống nhận được ở dạng hình thức hóa đặc tả đúng đắn những gì ta mong muốn về hệ thống 
cần xây dựng. 
4. Kết luận 
Bài báo đã trình bầy một tiến qui trình phát triển hệ thống phần mềm hướng đối tượng 
trên cơ sở các luật và các thuật toán biến đổi làm mịn, chúng được xây dựng dựa trên tính đúng 
của luật làm mịn và tính đúng của đặc tả hình thức đã xét. Để thực hiện các biến đổi làm mịn, 
các thuật toán làm mịn tương ứng được xây dựng phục vụ cho việc phát triển các mô hình hệ 
thống từ khái niệm đến thiết kế để được mô hình thiết kế cuối cùng đặc tả hệ thống cần xây 
dựng. Chúng tôi đã xây dựng các thuật toán: addClassName, addAttributeName, MoveAtt, 
priAttToproAtt, proAttTopubAtt, MoveMethod, addMethodName, RelationShip, Inheritance1, 
Inheritance2, Polymorphism để phục vụ cho đặc tả quá trình làm mịn và tinh chế các hệ thống 
hướng đối tượng [15, 16, 17]. 
Qua quá trình làm mịn cho ta mô hình thiết kế cuối cùng có biểu diễn tương đối gần 
với chương trình ở dạng ngôn ngữ lập trình có thể thực hiện được. Điều đó làm dễ dàng cho 
việc cài đặt hệ thống bằng bất kỳ ngôn ngữ lập trình hướng đối tượng, chẳng hạn như 
C#.Net hay Java. 
Để áp dụng được các bước làm mịn cụ thể đối với mỗi bài toán, việc sử dụng các khung 
nhìn của tiến trình RUP là rất cần thiết. Nó là những những mô hình trực quan, cho ta những gợi 
ý cho việc lựa chọn các phép biến đổi cần thiết ở mỗi bước. Khi thực hiện các phép biến đổi 
này, ở đây mới nêu ra được các việc cần làm để được hệ thống cuối cùng. Tuy nhiên, mô hình 
thiết kế tối ưu hay không chưa được đề cập. Ngoài ra, thực sự chúng tôi mới đưa ra nhưng phép 
biến đổi cơ bản. Còn có nhiều phép biến đổi liên quan đến những trường hợp tinh tế cũng chưa 
đề cập đến. Đó chính là những vấn đề đặt ra cần được tiếp tục nghiên cứu để có được một sự 
hoàn thiện và khả năng triển khai hiệu quả cao 
 
Tóm tắt 
 Trong bài báo này trình bày những nghiên cứu bước đầu về một tiến trình hình thức để 
đặc tả quá trình phát triển một hệ thống hướng đối tượng. Xuất phát từ biểu đồ miền lĩnh vực 
nghiệp vụ, quá trình phát triển hệ thống dựa trên tiến trình RUP nhưng được thực hiện bằng 
các biến đổi hình thức trên cơ sở các quan hệ đại số và các luật để đảm bảo tính đúng đắn của 
kết quả nhận được. Các phép biến đổi bao gồm thêm lớp, thêm thuộc tính, các phương thức 
cho lớp, phát triển các lớp kế thừa, chuyển đổi đặc trưng các thuộc tính của lớp, chuyển thuộc 
tính và toán tử từ một lớp sang một lớp khác, các phép toán đặc tả một phương thức của một 
lớp... Kết quả nhận được sẽ là một đặc tả hình thức của hệ thống với các lớp với các thành 
phần của nó. Do sự đặc tả trực quan gần với mô hình UML và ngôn ngữ lệnh nên có chuyển 
kết quả cuối cùng sang biểu đồ thiết kế với các lớp bằng UML, từ đó sử dụng Rational Rose 
để chuyển thành mã lệnh. 
Key words: UML, RUP, Rational Rose, Object–Oriented, refinement, process, class, 
attribute, operation 
T¹p chÝ Khoa häc & C«ng nghÖ - Sè 1(45) Tập 2/N¨m 2008 
 103
Summary 
The formal method specsification Object-Oriented System base on relation model 
This paper presents a algebric relations – based formal refinement process for the object-
oriented software system development. Starting at the conceptual class model of one applied 
domain (in conjunction with RUP), the refinement process trasforms this model to the final 
design class model by sequent applying number of algebric relations-based formal 
transformations and relevant rules. Theses transformations include these adding classes to the 
exsiting system model, adding and changing attrributes, operations in the clasess of this model, 
and also instructions in the operations of one class... The final design class model is a design 
specificaton of the expected software system. The repesentation of this final model is closed to 
one of the object-oriented programming languages. 
Tài liệu tham khảo 
[1] Booch, G., Rumbaugh, J. and Jacobson, I., The Unified Modeling Language User Guide, Addison-
Wesley, 1999. 
[2] C.A.R. Hoare and He Jifeng, Unifying Theories of Programming, Prentice Hall, 1998. 
[3] He Jifeng, Li Xiaohan and Zhiming Liu, rCOS: Refinement Calculus for Object Systems, Technical 
report UNU/IIST No.322, UNU/IIST: International Institute for software technology, the United 
Nations University, Macau, May 2005. 
[4] Ivar Jacopson, Gray Booch and James Rumbaugh, The Unified Software Development Process, 
Addision-Wesley, 2000. 
[5] J. He, Z. Liu, X. Li and S.Qin, A relational model for object-oriented designs. In Pro APLA’2004 
LNCS 3302, Taiwan, 2004, Springer. 
[6] Joshua Kerievsky, Refactoring to patterns, Addison-Wesley, 2004 
[7] Kuchten P., The Rational Unified Process – An Introduction, Addison-Wesley, 2000. 
[8] Larman, Applying UML and patterns, Prentice-Hall International, 2001. 
[9] Martin Fowler, Refactoring, improving the design of existing code, Addison-Wesley, 2000. 
[10] R.J.R. Back, L. Petre and I.P. Paltor, Formalizing UML use cases in the refinement calculus. In 
Proc. UML’99. Springer-Verlag, 1999. 
[11] Quan Long, He Jifeng, Zhiming Liu, Refactoring and pattern-directed refactoring: A formal 
perspective, Technical report UNU/IIST No.318, UNU/IIST: International Institute for software 
technology, the United Nations University, Macau, January 2005. 
[12] P. Andre, A. Romanczuk, J.C. Royer and A. Vasconcelos, Checking the consistency of UML class 
diagrams using Larch Prove. In Proc. ROOM’2000, York, UK, 2000. 
[13] Nguyễn Mạnh Đức, Nguyễn Văn Vỵ, Đặng Văn Đức (2005), “Mô hình đại số quan hệ của hệ 
thống hướng đối tượng”, Tạp chí Tin học và điều khiển học, Viện Khoa học và Công nghệ Việt 
Nam, 21 (3) tr.261-270. 
[14] Nguyễn Mạnh Đức, Đặng Văn Đức (2006), “Về một cách tinh chế mô hình lớp UML”, Tạp chí Tin 
học và điều khiển học, Viện Khoa học và Công nghệ Việt Nam, 22 (1) tr. 63-74. 
[15] Nguyễn Mạnh Đức, Đặng Văn Đức (2006), “Ứng dụng phương pháp hướng đối tượng và ngôn ngữ 
UML mô hình hoá hệ thống E-Learning”, Tạp chí Khoa học và Công nghệ, Viện Khoa học và 
Công nghệ Việt Nam, 44 (3) tr. 33-42. 
[16] Nguyễn Mạnh Đức (2007), Thiết kế hướng đối tượng và xây dựng hệ thống thông tin phức tạp, 
Luận án Tiến sĩ Toán học, Viện Công nghệ Thông tin - Viện KH&CN Việt Nam. 
[17] Đặng Văn Đức, Nguyễn Văn Vỵ, Nguyễn Mạnh Đức (2007), “Một số thuật toán tinh chế cấu trúc hệ 
thống hướng đối tượng dựa trên các luật làm mịn của rCOS”, Kỷ yếu 30 năm thành lập Viện Công 
nghệ Thông tin, Viện Công nghệ Thông tin - Viện KH&CN Việt Nam.