intTypePromotion=1
ADSENSE

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

Chia sẻ: Thi Thi | Ngày: | Loại File: PDF | Số trang:9

36
lượt xem
1
download
 
  Download Vui lòng tải xuống để xem tài liệu đầy đủ

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.

Chủ đề:
Lưu

Nội dung Text: 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 />
ADSENSE

CÓ THỂ BẠN MUỐN DOWNLOAD

 

Đồng bộ tài khoản
2=>2