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<br /> <br /> PHƯƠNG PHÁP HÌNH THỨC ĐẶC TẢ HỆ THỐNG<br /> HƯỚNG ĐỐI TƯỢNG DỰA TRÊN MÔ HÌNH rCOS<br /> 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)<br /> <br /> 1. Đặt vấn đề<br /> 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<br /> 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<br /> 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<br /> 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ử<br /> 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.<br /> Trong tiến trình phát triển thống nhất RUP (rational unified process) dựa trên ngôn ngữ<br /> UML (unified modeling language) [1, 4, 7], một số mô hình loại khác nhau của UML đã được<br /> 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<br /> 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ô<br /> 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<br /> 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ử<br /> 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ó<br /> 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ý<br /> 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 ở<br /> 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<br /> 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<br /> 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 đề đã<br /> được đặt ra cần giải quyết [12]:<br /> 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<br /> 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.<br /> 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<br /> 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ù<br /> hợp với nhau;<br /> 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<br /> 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ỉ<br /> 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<br /> 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 đó.<br /> 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<br /> đả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...<br /> 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] đã<br /> đượ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<br /> 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.<br /> 95<br /> <br /> T¹p chÝ Khoa häc & C«ng nghÖ - Sè 1(45) Tập 2/N¨m 2008<br /> <br /> 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,<br /> 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à<br /> 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 đồ<br /> 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<br /> 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 ở<br /> 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<br /> đổ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<br /> đắ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<br /> phần mềm hệ thống (hình vẽ dưới đây) [16, 17].<br /> Phương<br /> pháp<br /> mới<br /> <br /> Tiến<br /> trình<br /> RUP<br /> <br /> biểu đồ lớp<br /> khái niệm<br /> miền lĩnh<br /> vực<br /> mô hình<br /> nghiệp vụ<br /> khung<br /> nhìn 1<br /> <br /> phép<br /> BĐ1<br /> <br /> biểu đồ<br /> lớp được<br /> làm mịn 1<br /> <br /> mô hình<br /> phân tích<br /> khung<br /> nhìn 2<br /> <br /> phép<br /> BĐ2<br /> <br /> …<br /> <br /> phép<br /> BĐn<br /> <br /> …<br /> <br /> biểu đồ lớp<br /> thiết kế phần<br /> mềm hệ<br /> thống<br /> mô hình<br /> thiết kế<br /> khung<br /> nhìn k<br /> <br /> Ý tưởng cho phương pháp giải quyết vấn đề<br /> 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<br /> 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<br /> đề 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ố.<br /> 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<br /> 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<br /> 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<br /> trong mỗi phương thức.<br /> 2. Cơ sở của các phép biến đổi<br /> 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<br /> 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ý<br /> 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à<br /> 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<br /> như sau:<br /> p(x) ├ R(x, x’) def ok ∧ p(x) ⇒ ok’∧<br /> ∧ R(x, x’)<br /> 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<br /> 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<br /> 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à<br /> 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<br /> 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,<br /> ngược lại chúng là false.<br /> 96<br /> <br /> T¹p chÝ Khoa häc & C«ng nghÖ - Sè 1(45) Tập 2/N¨m 2008<br /> <br /> 2.1. Mô tả hệ thống hướng đối tượng<br /> 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à<br /> 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),<br /> 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ể<br /> 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<br /> 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<br /> có dạng như sau:<br /> [private] class N [extends M] {<br /> pri : T1 t1 = a1 ..., Tm tm = am;<br /> pro : U1 u1 = b1 ..., Un un = bn;<br /> pub : V1 v1 = d1 ..., Vk vk = dk;<br /> meth : m1 (T11 x11, T12 y12, T13 z13) { c1 };<br /> ... ;<br /> mℓ (Tℓ1 xℓ1, Tℓ2 yℓ2, Tℓ3 zℓ3) { cℓ }<br /> }<br /> <br /> trong đó:<br /> 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ó<br /> 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.<br /> 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.<br /> 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.<br /> 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.<br /> 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<br /> 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<br /> 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<br /> 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.<br /> 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,<br /> 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,<br /> 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<br /> 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<br /> 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.<br /> 2.2. Mô tả biểu thức<br /> 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<br /> gán, xác định theo các qui tắc như sau [2, 5]:<br /> e ::= x | null | self | e.a | e is C | C(e) | f(e)<br /> 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<br /> 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<br /> 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<br /> khuôn mẫu, f(e) là phép toán gắn liền với các kiểu nguyên thuỷ.<br /> 2.3. Mô tả các lệnh<br /> 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].<br /> 97<br /> <br /> T¹p chÝ Khoa häc & C«ng nghÖ - Sè 1(45) Tập 2/N¨m 2008<br /> <br /> 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<br />
b<br /> c | c ⊓ c | b*c<br /> tuần tự| chọn theo điều kiện| không tiền định| lặp<br /> c; c | c
<br /> le.m(e, v, u) | le:=e | C.new(x)<br /> gọi phương thức | gán| tạo đối tượng mới.<br /> Ở đâ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<br /> 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<br /> 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<br /> 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.<br /> 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à<br /> 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<br /> 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<br /> 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.<br /> 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,<br /> 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<br /> 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<br /> 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<br /> 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<br /> 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.<br /> 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ự<br /> 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ị<br /> 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.<br /> 3. Các phép biến đổi làm mịn mô hình hệ thống đối tượng<br /> 3.1. Các khái niệm<br /> 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<br /> [3, 9, 11, 13, 14]:<br /> Đị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=(α,<br /> 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).<br /> Ở đây x, ..., z là các biến chứa trong α.. D1≡ D2 nếu và chỉ nếu D1⊑ D2 và D2 ⊑ D1.<br /> Đị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à<br /> 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).<br /> Trong trường hợp này ρ được gọi là ánh xạ làm mịn.<br /> Đị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<br /> 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<br /> 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)<br /> Ở đâ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<br /> đ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<br /> 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<br /> mịn từ các biến của S1 tới S2 trên tập các biến chung đó.<br /> Định nghĩa 4 (làm mịn lớp): Cho cdecls1 và cdecls2 là hai khai báo. cdecls2 là làm<br /> mịn của cdecls1, đượcký hiệu lài cdecls2 ⊒class cdecls1 nếu như phần trước có thể thay thế<br /> 98<br /> <br /> T¹p chÝ Khoa häc & C«ng nghÖ - Sè 1(45) Tập 2/N¨m 2008<br /> <br /> phần sau trong bất kỳ hệ thống đối tượng: cdecls2 ⊒class cdecls1 def ∀P . (cdecls2• P ⊒sys<br /> cdecls1• P). Ở đây P đóng vai trò cho phương thức chính (glb, c).<br /> 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<br /> đó, ở đây ta chỉ quan tâm làm mịn giữa các phần khai báo.<br /> 3.2. Xây dựng qui trình làm mịn mô hình<br /> 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].<br /> 3.2.1. Xây dựng hệ thống khởi tạo ban đầu<br /> 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ô<br /> 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<br /> vực nghiệp vụ và các liên kết giữa chúng với nhau.<br /> Thuật toán bổ sung các lớp vào mô hình khởi tạo:<br /> 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<br /> đặ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:<br /> APP0 = N1[]; N2[]; ...; Nk[]<br /> 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<br /> addClassName như sau:<br /> // Thuật toán addClassName- bổ sung các lớp vào mô hình<br /> Input: Một tên xâu cho định danh cho lớp Ni.<br /> Output: Lớp Ni trống (chưa có các thuộc tính hoặc phương thức).<br /> Format: addClassName ()<br /> Method:<br /> var stop: Boolean, s: String;<br /> stop := false;<br /> while ¬ stop do {<br /> read(s);<br /> if {(s ””) → AdditionClassName(s)} fi;<br /> read(stop);<br /> }<br /> end stop, s;<br /> End.<br /> <br /> Ở đâ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<br /> đó, 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].<br /> 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.<br /> 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]<br /> Thuật toán bổ sung các thuộc tính cho lớp:<br /> 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<br /> 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<br /> 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:<br /> Ni[]; cdecls ⊑ Ni[pri ]; cdecls<br /> 99<br /> <br />