Luận án Kiểm thử dựa trên mô hình với cách tiếp cận mô hình hóa chuyên biệt miền

được định nghĩa hợp lệ: 1 self.uslnode ->forAll(n:USLNode| 2 if (n.oclIsTypeOf(InitialNode))then 3 self.flowedge ->select(b:FlowEdge |(b.source.oclIsTypeOf(USL:: InitialNode))and(b.oclIsTypeOf(USL:: BasicFlowEdge)))->size() =1 4 else 5 if(self.flowedge ->selectByType(BasicFlowEdge)->select(b: BasicFlowEdge|b.target=n))->size() >=1 then 6 if (n.oclIsTypeOf(DecisionNode))then 7 self.flowedge ->selectByType(BasicFlowEdge)->select (b: BasicFlowEdge|b.source=n)->size()=1 8 else 9 if(n.oclIsTypeOf(ForkNode)) then 10 self.flowedge ->select(f:FlowEdge|f.source=n)->forAll(b :FlowEdge|b.oclIsTypeOf(BasicFlowEdge)) 11 else 12 if(n.oclIsTypeOf(JoinNode)) then 13 (self.flowedge ->select(f:FlowEdge|f.source=n)-> forAll(b:FlowEdge|b.oclIsTypeOf(BasicFlowEdge)))and(self. flowedge ->select(f:FlowEdge|f.target=n)->forAll(b:FlowEdge|b. oclIsTypeOf(BasicFlowEdge))) 14 else 15 if(n.oclIsKindOf(FlowStep)) then 16 self.flowedge ->select(f:FlowEdge |(f.source=n)and(f .oclIsTypeOf(BasicFlowEdge)))->size()= 1 17 else true 18 endif 19 endif 20 endif 21 endif 22 else ((self.flowedge ->selectByType(BasicFlowEdge)->select(b: BasicFlowEdge|b.source=n))->size()=0) and if(n.oclIsTypeOf( FinalNode))then 23 true else self.flowedge ->selectByType (AlternateFlowEdge) ->exists (f:AlternateFlowEdge|f.label=self.flowedge -> selectByType(AlternateFlowEdge)->select(a:AlternateFlowEdge|a .target=n)->first ().label)endif) endif endif) Luật 11. Thuộc tính number của mỗi FlowStep trong Basic flow là duy nhất: Chương 3. Đặc tả ca sử dụng theo hướng mô hình hóa chuyên biệt miền 65 1 self.uslnode ->selectByKind(FlowStep)->select(n:FlowStep|self. flowedge ->selectByType(BasicFlowEdge)->exists(t:BasicFlowEdge |(t.source=n)or(t.target=n)))->forAll(n1:FlowStep , n2: FlowStep|n1.number=n2.number implies n1=n2). Luật 12. Thuộc tính number của mỗi FlowStep trong một Alternate flow là duy nhất: 1 self.uslnode ->selectByKind(FlowStep)->select (n:FlowStep|self. flowedge ->selectByType(AlternateFlowEdge)->exists(t: AlternateFlowEdge |(t.source=n)or(t.target=n)))->forAll(n1: FlowStep ,n2:FlowStep |(n1.number=n2.number)and(self.flowedge -> selectByType(AlternateFlowEdge)->select(t1:AlternateFlowEdge| t1.target=n1)->first().label=self.flowedge ->selectByType( AlternateFlowEdge)->select(t2:AlternateFlowEdge|t2.target=n2) ->first().label) implies n1=n2). Ví dụ 3.4.2.1. Khi chúng ta thực hiện một số thay đổi trên mô hình USL hiển thị trong Hình 3.5 như sau: - Nếu chúng ta loại bỏ c0 hoặc thêm một InitialNode mới vào mô hình này thì nó sẽ vi phạm Luật 1. - Nếu chúng ta loại bỏ cả c7, c8 khỏi mô hình thì nó sẽ vi phạm Luật 2. - Nếu mô hình chỉ có các ControlNode thì nó sẽ vi phạm Luật 3. - Nếu FlowEdge b1 không phải là một BasicFlowEdge mà là một AlternateFlowEdge thì mô hình sẽ vi phạm Luật 4. - Nếu chúng ta nối b17 với c8 và bỏ c7 thì mô hình sẽ vi phạm Luật 5. - Nếu chúng ta thêm một AlternateFlowEdge nối giữa s4 và c6 thì mô hình sẽ vi phạm Luật 6 và 9. - Nếu chúng ta bỏ b14, s11, b16, p3 thì mô hình sẽ vi phạm Luật 7 và 8. - Nếu FlowEdge b6 không phải là BasicFlowEdgemà là AlternateFlowEdge hoặc giá trị của thuộc tính label của AlternateFlowEdge al 1 không phải là “4a” thì mô hình sẽ vi phạm Luật 10. - Nếu giá trị thuộc tính number của s2 không phải là 2 mà là 1 thì mô hình vi phạm Luật 11. - Nếu giá trị của thuộc tính number của s14 không phải là 2 mà là 1 thì mô hình vi phạm Luật 12. Chương 3. Đặc tả ca sử dụng theo hướng mô hình hóa chuyên biệt miền 66 3.4.3 Cú pháp cụ thể của USL Để giúp người dùng có thể tạo được các mô hình USL một cách trực quan và dễ dàng, luận án đề xuất xây dựng cú pháp cụ thể cho USL với các ký hiệu (notation) đồ họa như trong Bảng 3.2. Hình 3.5 là mô hình USL của ca sử dụng Lend book trong cú pháp cụ thể. Luận án đã triển khai cú Bảng 3.2: Các ký hiệu đồ họa của các khái niệm trong mô hình USL Khái niệm Trình bày Ký hiệu DescriptionInfor Một hộp văn bản không có đường viền, các thuộc tính được trình bày ứng với một danh sách trong hộp InitialNode Một hình tròn rỗng FinalNode Một hình tròn gạch tréo ở giữa DecisionNode Một hình thoi nền đen nhỏ có một cạnh đivào và ít nhất hai cạnh đi ra ForkNode Một đoạn thẳng tô đậm có một cạnh đi vàovà ít nhất hai cạnh đi ra JoinNode Một đoạn tô đậm có ít nhất hai cạnh đi vàovà một cạnh đi ra BasicFlowEdge Một đường mũi tên đậm AlternateFlowEdge Một đường mũi tên mảnh được gán nhãn làtên của luồng thay thế ActorStep Hình chữ nhật gồm hai phần. Phần đầu chứa nhãn và các thuộc tính numberStep và description của ActorStep. Phần hai là danh sách các thông tin của các ActorAction của ActorStep SystemStep Hình chữ nhật gồm hai phần. Phần đầu chứa nhãn và hai thuộc tính numberStep và description của SystemStep. Phần hai là danh sách các thông tin của các SystemAction của SystemStep Action Thông tin của một Action được trình bày bằng một chuỗi văn bản trong phần hai của một FlowStep Chương 3. Đặc tả ca sử dụng theo hướng mô hình hóa chuyên biệt miền 67 pháp cụ thể này cho công cụ soạn thảo USL. Giải thích chi tiết về công cụ này được giải thích trong Chương 5. Sau khi xây dựng cú pháp cho ngôn ngữ, luận án sẽ trình bày về ngữ nghĩa cho ngôn ngữ. Theo Kleppe [35], ngữ nghĩa của một ngôn ngữ mô hình mô tả những gì xảy ra trong máy tính khi một mô hình của ngôn ngữ được thực thi. Trong lý thuyết ngôn ngữ có bốn cách khác nhau để mô tả ngữ nghĩa cho một ngôn ngữ: (i) Ký hiệu (Denotational) là việc cấu trúc các đối tượng toán học. Các đối tượng toán học này đại diện cho ý nghĩa của các mô hình; (ii) Sự hoạt động (Operational) là việc mô tả cách một mô hình được biên dịch như một chuỗi của các bước tính toán. Thường thì ngữ nghĩa hoạt động được đưa ra dưới dạng một hệ thống chuyển trạng thái; (iii) Phép chuyển (Translational) là việc chuyển các mô hình vào trong một ngôn ngữ khác đã được hiểu tốt; (iv) Thực dụng (Pragmatic) là cung cấp một công cụ thực thi mô hình. Để mô tả ngữ nghĩa của USL, luận án sẽ cung cấp một ngữ nghĩa thực thi cho USL bằng cách sử dụng một hệ thống chuyển trạng thái được gán nhãn và xây dựng một số các phép chuyển. Việc cung cấp một ngữ nghĩa thực thi cho ngôn ngữ USL là hình thức hóa hoạt động của một mô hình USL để luận án sử dụng cho mục đích sinh các ca kiểm thử như nghiên cứu [46] hình thức hóa biểu đồ hoạt động cho mục đích sinh các ca kiểm thử. Ngoài ra, các phép chuyển được xây dựng để cung cấp các bộ sinh tự động từ các mô hình USL. Các mục tiếp theo, luận án sẽ trình bày lần lượt hai cách mô tả ngữ nghĩa của ngôn ngữ USL. Chương 3. Đặc tả ca sử dụng theo hướng mô hình hóa chuyên biệt miền 68 Hình 3.5: Đặc tả ca sử dụng Lend Book bằng một mô hình USL. Chương 3. Đặc tả ca sử dụng theo hướng mô hình hóa chuyên biệt miền 69 3.5 Ngữ nghĩa hình thức của mô hình USL Phần này, luận án cung cấp ngữ nghĩa hình thức cho các mô hình USL. Mục đích là để cung cấp một ngữ nghĩa thực thi cho các mô hình USL bằng cách sử dụng một hệ thống chuyển trạng thái được gán nhãn. Ngữ nghĩa thực thi của các mô hình USL sẽ là cơ sở lý thuyết để luận án xây dựng các thuật toán sinh các ca kiểm thử tự động từ mô hình USL. Luận án định nghĩa hình thức một mô hình USL thông qua các định nghĩa được trình bày trong phần này. Ở đây, luận án xem một mô hình USL như một đồ thị gồm có các nút và các cạnh. Một nút đại diện cho một bước hoặc một hành động điều khiển được thực hiện bởi hệ thống. Ngoài ra, các khái niệm miền của hệ thống được mô hình trong biểu đồ lớp UML cũng được tham chiếu. Định nghĩa 3.1 (Mô hình USL) Một mô hình USL của một ca sử dụng là một bộ D = 〈DC ,A,E ,C ,Act ,Fe ,Fc ,Ff 〉 với: - DC là một biểu đồ lớp trình diễn các khái niệm miền của hệ thống; - A = AcNode ∪Af là tập của các nút (USLNode); - E = Eb ∪ Ea là tập của các cạnh (FlowEdge); - C = G ∪ {cpreUC } ∪ CpostUC ∪ CpreA ∪ CpostA là tập các ràng buộc (Constraint); - Act = Acta ∪Acts là tập của hành động (Action); - Fe ⊆ {A×G × E ×A} là mối quan hệ giữa các nút, điều kiện gác G, và các cạnh; - Fc ⊆ {CpreA×Act ×CpostA} là các quan hệ giữa các hành động với các tiền và hậu điều kiện của các hành động; - Ff ⊆ {Nf ×CpostUC } là mối quan hệ giữa các nút kết thúc (FinalNode) và hậu điều kiện của ca sử dụng. Trong đó: - AcNode = NI ∪Nf ∪Nd ∪Nj ∪Nk , với: + NI = {cit} là tập các nút bắt đầu (InitialNode), + Nf = {cf 1, . . . , cfn} là tập các nút kết thúc (FinalNode), + Nd = {cd1, . . . , cdn} là tập các nút quyết định (DecisionNode), Chương 3. Đặc tả ca sử dụng theo hướng mô hình hóa chuyên biệt miền 70 + Nj = {cj1, . . . , cjn} là tập các nút nối (JoinNode), + Nk = {ck1, . . . , ckn} là tập các nút chia (ForkNode); - Af = Aa ∪As là tập các bước (FlowStep), khi đó: + Aa = {sa1, . . . , san}(∀ sa ∈ Aa , sa = (sd ,Aca)) là tập các bước của tác nhân (ActorStep), + As = {ss1, . . . , ssn}(∀ ss ∈ As , ss = (sd ,Acs)) là tập các bước của hệ thống (SystemStep), trong đó: • sd ∈ String là mô tả của bước sa và ss , • Aca = (Aca ⊂ Acta) là tập các hành động của tác nhân (ActorAction) có thứ tự trong sa , • Acs = (Acs ⊂ Acts) là tập các hành động của hệ thống (SystemAction) có thứ tự trong ss , • actions(sa) = Aca và actions(ss) = Acs là một ánh xạ từ sa và ss tới Aca và Acs , • firstAct(sa) = aa1, firstAct(ss) = as1, lastAct(sa) = aan , và lastAct(ss) = asn là bốn ánh xạ từ sa và ss tới aa1, as1, aan , và asn , • Actions(D) = ⋃s∈Af actions(s) ≡ Act . + ∀ si , sj ∈ Af , actions(si ) ∩ actions(sj ) = ∅. - Eb = {eb1, . . . , ebn} là tập các cạnh BasicFlowEdge, - Ea = {ea1, . . . , ean} là tập các cạnh AlternateFlowEdge. - G = {gc1, . . . , gcn} là tập các điều kiện gác trên các cạnh; - cpreUC là tiền điều kiện của ca sử dụng; - CpostUC = {pu1 . . . pun} là hậu điều kiện của ca sử dụng; - CpreA = {pe1, . . . , pen} là tập các tiền điều kiện của các hành động; - CpostA = {po1, . . . , pon} là tập các hậu điều kiện của các hành động; - Acta = Actai ∪Actar là tập các hành động của tác nhân, với: + Actai là tập các hành động ActorInput, + Actar là tập các hành động ActorRequest; - Acts = Actsd ∪ Actsp ∪ Actss ∪ Actso ∪ Actsr ∪ Actsi ∪ Actse là tập các hành động của hệ thống, với: + Actsd là tập các hành động SystemDisplay, + Actsp là tập các hành động SystemOperation, Chương 3. Đặc tả ca sử dụng theo hướng mô hình hóa chuyên biệt miền 71 + Actss là tập các hành động SystemState, + Actso là tập các hành động SystemOutput, + Actsr là tập các hành động SystemRequest, + Actsi là tập các hành động SystemInclude, + Actse là tập các hành động SystemExtend. Trên mô hình D, luận án định nghĩa một số hàm như trong Bảng 3.3. Ví dụ 3.4.1.5. Mô hình USL như trong Hình 3.5 chứa các thành phần như sau: NI = {c0}; NF = {c7, c8}; AcNode = {c0, . . . , c8}; Aa = {s1, s3, s5, s7, s13}; As = {s2, s4, s6, s8, . . . , s12, s14, s15, s16}; Eb = {b1, . . . , b17}; Ea = {al 1, . . . , al 10}; G = {g1, . . . , g6}; CpreUC = ∅; CpostUC = ∅; CpreA = ∅; và CpostA = {p1, . . . , p6}; Act = {a1, . . . , a18}. DC tương ứng với mô hình khái niệm trong phần (b) của Hình 3.1. Mô hình này có mười sáu ràng buộc là điều kiện gác và hậu điều kiện. Ví dụ, hậu điều kiện p1 của Action a11 được trình bày bằng OCL như sau: BookLoan.allInstances()->exists(b:BookLoan| (b.bcid = bcid) and (b.bid = bid) and (b.payed=0)). Luận án sử dụng một LTS [34] để định nghĩa hình thức ngữ nghĩa hoạt động cho các mô hình USL. Sự thực thi của một mô hình USL được mô hình hóa bởi một LTS. Trong đó, các chuyển được gây ra bởi việc thực hiện của các hành động và các trạng thái xác định bởi các phép gán biến khi thực thi. Luận án định nghĩa một LTS của một mô hình USL đệ quy từ các khái niệm USL cơ bản. Ngữ nghĩa của của các khái niệm này được định nghĩa tóm tắt như trong Bảng 3.4. Trong định nghĩa 2, luận án sẽ hình thức các khái niệm của một LTS được ánh xạ từ một mô hình USL. Định nghĩa 3.2 (Thực thi mô hình USL) Cho một mô hình USL D = 〈DC ,A,E ,C ,Act ,Fe ,Fc ,Ff 〉, một LTS mô tả thực thi của D là một bộ năm 〈Σ(V),P(G ×A× P), T , αinit ,F〉 trong đó: - V là một tập hữu hạn của các biến mà kiểu của nó là các kiểu cơ bản và các lớp của DC ; - Σ(V) là tập của các trạng thái (α), mỗi trạng thái là một tập của các gán giá trị tới tập con của các biến trong V; - P ⊆ CpostA ∪CpostUC là tập của các ràng buộc hậu điều kiện của D ; - A = AcNode ∪Act là tập của các hành động; - G ⊆ G ∪CpreUC ∪CpreA là tập các điều kiện gác của các chuyển; Chương 3. Đặc tả ca sử dụng theo hướng mô hình hóa chuyên biệt miền 72 - αinit ∈ Σ(V) là trạng thái bắt đầu; - F ⊂ Σ(V) là tập các trạng thái kết thúc; - T ⊆ Σ(V)×P(G×A×P)×Σ(V) là mối quan hệ chuyển được định nghĩa như sau: Một chuyển t = (α, (g , a, p), α′) ∈ T , hoặc ký hiệu là α g |a|p−→ α′, Bảng 3.3: Danh sách các hàm được định nghĩa trong D Hàm Điều kiện Mô tả firstAct(c) = c c ∈ AcNode Trả về hành động đầu tiên chứa trong một ControlNode. lastAct(c) = c c ∈ AcNode Trả về hành động cuối cùng chứa trong một ControlNode. source(e) = ns e ∈ E ,ns ∈ A, nt ∈ A, g ∈ G , (ns , g , e,nt) ∈ Fe Trả về một USLNode nguồn của một FlowEdge. target(e) = nt Trả về một USLNode đích của một FlowEdge. guardE(e) = g Trả về điều kiện gác của một FlowEdge. guardE(ns, nt) = g Trả về điều kiện gác của cạnh có nút nguồn và nút đích truyền vào. preA(a) = pe a ∈ Actions(D), (pe , a, po) ∈ Fc Trả về tiền điều kiện của một hành động. postA(a) = po Trả về hậu điều kiện của một hành động. preA(c) = True c ∈ (AcNode \NI ) Trả về tiền điều kiện của một ControlNode không phải là InitialNode postA(c) = True c ∈ (AcNode \Nf ) Trả về hậu điều kiện của một ControlNode không phải là FinalNode. postA(c) = True c ∈ (AcNode \Nf ) Trả về hậu điều kiện của một ControlNode không phải là FinalNode postC(c) = pu c ∈ Nf , (c, pu) ∈ Ff Trả về hậu điều kiện của một FinalNode preC(D) = cpreUC Trả về tiền điều kiện của một mô hình USL. isCompleted(e) = True e ∈ E , lastAct(target(e)) đã hoàn thành thực thi Trả về trạng thái hoàn thành của một cạnh. isCompleted(e) = False e ∈ E , lastAct(target(e)) chưa hoàn thành thực thi Chương 3. Đặc tả ca sử dụng theo hướng mô hình hóa chuyên biệt miền 73 với: + a ∈ A là hành động để xảy ra chuyển t , + α, α′ ∈ Σ(V) là các trạng thái đầu và cuối của chuyển t mà α′ thỏa mãn p, + p ∈ P là hậu điều kiện sau khi thực hiện hành động a, g = defGuard(a) ∈ G là điều kiện gác để thực thi hành động a, Khi đó: defGuard(a) được định nghĩa như sau (được tổng hợp trong Bảng 3.4): =  preC(D), if a ∈ NI . guardE(e)(e ∈ D .E , target(e) = a), if a ∈ AcNode \Nj .∧ (e∈D .E ,target(e)=a) isCompleted(e) ∧ guardE(e), if a ∈ Nj . preC(DI ) ∧ preA(a) ∧ guardE(e)(e ∈ D .E , target(e) = a), if a ∈ Actsi . preC(DX ) ∧ preA(a) ∧ guardE(e)(e ∈ D .E , target(e) = a), if a ∈ Actse . preA(a) ∧ guardE(e)(s ∈ Af , target(e) = s), if ((a ∈ Aact) ∧ (a = firstAct(s)). preA(a)(s ∈ Af , a ∈ actions(s)), if otherwise Ví dụ 3.5.1. Hình 3.1 hiển thị mô hình ca sử dụng đơn giản của hệ thống Library và mô hình lớp của các khái niệm. Luận án giả định rằng một snapshot được hiển thị trong Hình 3.6 được nắm bắt khi mô hình ca sử dụng trong Hình 3.5 được thực thi tại bước a8 . Chúng ta có các phép gán giá trị như sau: (bid , “b 01”) ≡ bid = “b 01”, (bid , “b01”) ≡ bid = “b01”, (bcid , “bc 01”) ≡ bcid = “bc 01”, (lid , “l 01”) ≡ lid = “l 01”, ldate, “24/11/18”) ≡ ldate = “24/11/18”, (lbid , “lb 1”) ≡ lbid = “lb 1”. Các đối tượng của snapshot này là như sau: Borrower :“b 01”, Borrower :“b 02”, Book:“b01”, Book:“b02”, BookCopy:“bc 01”, BookCopy:“bc 02”, BookCopy:“bc 03”, Librarian:“l 01”, Librarian:“l 02”, Librarian:“l 03”, BookLoan:“lb 1”. Khi đó, trạng thái αa8 = {(bid , “b 02”), (bcid , “b 01”), (iid , “l 01”), (ldate = “24/11/18′′), Borrower :“b 01”, Borrower :“b 02”, Book :“b01”, Book :“b02”, BookCopy :“bc 01”, BookCopy :“bc 02”, BookCopy :“bc 03”, Librarian:“l 01”, Librarian:“l 02”, Librarian:“l 03”, BookLoan:“lb 1”}. Trong các hành động có thể có một số hành động được thực hiện đồng thời, những hành động này gây nên các chuyển đồng thời giữa các trạng thái. Hai định nghĩa tiếp theo định nghĩa hình thức các chuyển đồng thời. Chương 3. Đặc tả ca sử dụng theo hướng mô hình hóa chuyên biệt miền 74 Bảng 3.4: Ngữ nghĩa dựa trên LTS của các khái niệm USL cơ bản Các khái niệm USL Ký hiệu Ngữ nghĩa dựa trên LTS Step a1 ... an α α1 ... αn g1 | a1 | p1 gn | an | pn where gi = preA(ai ), pi = postA(ai ) (∀ i = 2, . . . ,n). Flow edge n1 n2 α α1 α2 g1 | a1 | p1 g2 | a2 | p2 where a2 = firstAct(n2), g2 = guardE(n1,n2) ∧ preA(a2), p2 = postA(a2). Decision node c nd n1 ... nm α αd αc α′ gd | ad | pd gc | c | true ga | a | pa where ad = lastAct(nd ); gc = guardE(nd , c), a = firstAct(n), ga = guardE(c,n) ∧ preA(a) s.t n ∈ {n1, . . . ,nm}. Fork node nf n1 ... nmc α αf αc α′1 ... α′m gf | af | pf gc | c | trueg1 | a1 | p1 gm | am | pm where af = lastAct(nf ); gc = guardE(nf , c), ai = firstAct(ni ), gi = preA(ai ), pi = postA(ai ) (∀ i = 1, . . . ,m). Join node n1 ... nm nj c α1 ... αm αc αj α g1 | a1 | p1 gm | am | pm gw | c | true gj | aj | pj where ai = lastAct(ni ), (∀ i = 1, . . . ,m); gw = ( ∧ (e∈D.E,target(e)=c) isCompleted(e)∧guardE(e)); aj = firstAct(nj ), gj = guardE(c,nj ) ∧ preA(aj ), pj = postA(aj ). Initial node c n α αi α′ gu | c | true g | a | p where α = αinit , gu = preC(D); a = firstAct(n), g = guardE(c,n) ∧ preA(a), p = postA(a). Flow final node n c α αf α′ g | a | p gc | c | pf where α′ ∈ F , pf = postC(D , c), gc = guardE(n, c); a = lastAct(n), USL model with include action n1 n n2 DI ≡ n1 nI1 ... nIm n2 where n ∈ As , | actions(n) |= 1, a ∈ Actsi (a ∈ actions(n)), t = (α, (ga | a | pa ), α′); nI1 , . . . ,nIm ∈ DI .A, ga = guardE(n1,n) ∧ preA(a) ∧ preC(DI ), pa = postC(nf ) | nf ∈ DI .Nf USL model with extend action n1 n n2 DX ≡ n1 nX1 ... nXm n2 where n ∈ As , | actions(n) |= 1, a ∈ Actse(a ∈ actions(n)), t = (α, (ga | a | pa ), α′); nX1 , . . . ,nXm ∈ DX .A, ga = preA(a) ∧ preC(DX ), ga = guardE(n1,n) ∧ preA(a) ∧ preC(DX ), pa = postC(nf ) | nf ∈ DX .Nf Legend a a action in a step; s a step; Du use case; α a state Định nghĩa 3.3 (Các hàm trong LTS) Cho một LTS L của một mô hình USL D , một trạng thái hiện thời của L là α, và một chuyển t = α g |a|p−→ α′ ∈ L.T . Luận án định nghĩa các thuật ngữ như sau: - preT(t) = α, postT(t) = α′, guard(t) = g , postC(t) = p, và act(t) = a. Chương 3. Đặc tả ca sử dụng theo hướng mô hình hóa chuyên biệt miền 75 Hình 3.6: Một snapshot của ca sử dụng Lend Book. - eval(g) là giá trị của ràng buộc g . - reachable(α) = {t | preT(t) = α} là tập của các chuyển bắt đầu từ α. - firable(α) = {t ∈ reachable(α), eval(guard(t)) = true} là tập của các chuyển có thể được kích hoạt (fired) từ α. Ví dụ 3.5.2. Khi mô hình trong Hình 3.5 thực hiện tại hành động a11, chúng ta có: Khi đó, trạng thái αa11 = {(bid , “b 02”), (bcid , “b 01”), (lid , “l 01”), (ldate = “24/11/18”), (bLoan(“lb 2”, “b 01”, “b 02”, “l 01”, “24/11/18”, 0) Borrower :“b 01”, Borrower :“b 02”, Book :“b01”, Book :“b02”, BookCopy :“bc 01”, BookCopy :“bc 02”, BookCopy :“bc 03”, Librarian:“l 01”, Librarian:“l 02”, Librarian:“l 03”, BookLoan:“lb 1”, BookLoan:“lb 2”}. Chuyển ta11,c4 = αa11 true|c4|true−→ αc4. reachable(αa11) = {ta11,c4} và firable(αa11)= {ta11,c4}. Định nghĩa 3.4 (Chuyển đồng thời) Cho một LTS L của một mô hình USL D và trạng thái hiện tại α của. Một chuyển trạng thái đồng thời τ ∈ L.T là một tập của các chuyển t1, t2, . . . , tn ∈ firable(α). Ví dụ 3.5.3. Khi mô hình USL trong Hình 3.5 thực hiện tại bước c4, chúng ta có hai chuyển là tc4,a12 = αc4 true|a12|p2−→ αa12 và tc4,a13 = αc4 true|a13|p3−→ αa13, reachable(αc4) = {tc4,a12, tc4,a13} và firable(αc4) = {tc4,a12, tc4,a13}. Do đó, {tc4,12, tc4,13} là một chuyển đồng thời và αa12, αa13 tương ứng thỏa mãn p2, p3. Chương 3. Đặc tả ca sử dụng theo hướng mô hình hóa chuyên biệt miền 76 Bên trong cách tiếp cận của luận án, một LTS của một mô hình USL có thể chứa cả hai chuyển đồng thời và chuyển không đồng thời. Tiếp theo, luận án định nghĩa ngữ nghĩa của một kịch bản ca sử dụng. Định nghĩa 3.5 (Thực thi kịch bản ca sử dụng) Cho một kịch bản ca sử dụng của một mô hình USL D bao gồm một chuỗi các hành động (a0, . . . , an−1). Sự thực thi của kịch bản này là một đường trong LTS L của D : p = α0 t0→ α1 t1→ . . . tn−1→ αn , khi đó ti = αi gi |ai |pi−→ αi+1 (∀ i = 0, . . .,n − 1), α0 = L.αinit , αn ∈ L.F , và ti ∈ L.T . Ví dụ 3.5.4. Khi mô hình USL trong Hình 3.5 thực hiện ở bước αa11 như đã đề cập ở trên và eval(g1), eval(g3), và eval(g5) là true, thì kịch bản ca sử dụng là như sau: p = αinit true|a1|true−→ αa1 true|a2|true−→ αa2 true|a3|true−→ αa3 true|a4|true−→ αa4 true|a5|true−→ αa5 true|a6|true−→ αa6 true|c1|true−→ αc1 g1|a7|true−→ αa7 true|a8|true−→ αa8 true|c2|true−→ αc2 g3|a9|true−→ αa9 true|a10|true−→ αa10 g5|a11|true−→ αa11 true|c4|true−→ αc4 {true|a12|p2,true|a13|p3}−→ αa12−a13 true|c5|true−→ αc5 true|c7|true−→ αc7 (αc7 ∈ F). 3.6 Chuyển đổi mô hình USL Phần này thảo luận về cách các mô hình USL có thể được chuyển tới các chế tác phần mềm khác bao gồm các ca kiểm thử, các mô hình cấu trúc, các mô hình hành vi, và các mô tả ca sử dụng dựa trên mẫu văn bản (textual Template-based Use case Descriptions - TUCD). Trong phần này, luận án tập trung vào chuyển đổi từ mô hình USL tới một TUCD. Mục đích là để minh họa khả năng chuyển đổi mô hình của USL. 3.6.1 Sinh các ca kiểm thử Theo cách tiếp cận kiểm thử hướng ca sử dụng [26], một kịch bản ca sử dụng xác định một kịch bản kiểm thử. Các ràng buộc của một kịch bản ca sử dụng giúp xác địch các dữ liệu kiểm thử tương ứng của kịch bản. Phương pháp kiểm thử dựa trên mô hình [71] trình bày một kỹ thuật cho sinh tự động các ca kiểm thử từ một mô hình ca sử dụng. Cụ thể, các luồng điều khiển của một mô hình ca sử dụng được sử dụng để sinh các kịch bản ca sử dụng. Ví dụ, Linzhang [41] trình bày một kỹ thuật để diễn tả các Chương 3. Đặc tả ca sử dụng theo hướng mô hình hóa chuyên biệt miền 77 luồng điều khiển sử dụng biểu đồ hoạt động UML. Tác giả sau đó đề xuất một thuật toán để thăm tất cả các đường cơ bản (basic paths) có thể của biểu đồ hoạt động để sinh các kịch bản kiểm thử. Hai công việc khác [2, 3, 73] tập trung vào vấn đề sinh dữ liệu kiểm thử tự động từ các ràng buộc của kịch bản kiểm thử được viết trong OCL. Họ phát triển các bộ giải ràng buộc OCL cho công việc này. Do USL đặc tả rõ ràng được các khía cạnh thông tin khác nhau được mô tả trong ca sử dụng trong đó bao gồm các luồng điều khiển và các ràng buộc khác nhau trong ca sử dụng. Vì vậy, chúng tôi tin rằng các mô hình USL cũng có thể được sử dụng như là một đầu vào để sinh các ca kiểm thử. Cụ thể, USL có các siêu khái niệm để diễn tả các loại nút điều khiển khác nhau như biểu đồ hoạt động trong UML. Hơn nữa, khái niệm Constraint của USL đặc tả được các loại ràng buộc cần thiết để sinh dữ liệu khác nhau. Trong chương tiếp theo, luận án sẽ đề xuất phương pháp để sinh các ca kiểm thử từ các ca sử dụng được đặc tả trong các mô hình USL. 3.6.2 Sinh các mô hình cấu trúc và mô hình hành vi Trong hoạt động phân tích yêu cầu, các hành vi được mô tả trong một mô tả ca sử dụng được phân tích để tạo các mô hình cấu trúc và hành vi khác. Các mô hình đích thường được diễn tả bằng sử dụng các biểu đồ của UML, bao gồm biểu đồ hoạt động, biểu đồ lớp, biểu đồ cộng tác, và biểu đồ tuần tự. Savic´ [59], Silva [14], Smialek [63] đề xuất các DSL để đặc tả ca sử dụng. Cụ thể, ba nghiên cứu sử dụng các kiểu hành động khác nhau để mô hình các hành vi ca sử dụng. Sau đó, họ trình bày kỹ thuật chuyển mô hình để chuyển tự động các hành vi và các yếu tố mô hình liên quan vào trong một biểu đồ lớp. Ví dụ, các yếu tố mô hình được thảo luận trong [71] bao gồm đối tượng gửi, đối tượng nhận, thông điệp, và các tham số. USL được phát triển theo ý tưởng của các công việc ở trên. Đặc biệt, luận án sử dụng siêu khái niệm Action để diễn tả các hành vi ca sử dụng và các thông tin liên quan như thảo luận ở trên. Hơn nữa, USL còn diễn tả được luồng điều khiển trong ca sử dụng thông qua sử dụng các cấu trúc điều khiển như trong biểu đồ hoạt động. Vì vậy, mô hình USL có thể được Chương 3. Đặc tả ca sử dụng theo hướng mô hình hóa chuyên biệt miền 78 sử dụng như là đầu vào để sinh các mô hình cấu trúc và mô hình hành vi. Ví dụ, một kỹ thuật cho việc sinh biểu đồ tuần tự được trình bày trong [40, 66]. Một kỹ thuật trình bày cho việc sinh biểu đồ lớp từ đặc tả ca sử dụng được trình bày trong [42]. 3.6.3 Sinh TUCDs Theo[17, 36, 57], mô tả ca sử dụng dựa trên mẫu dạng văn bản TUCDs [13, 28, 68] cho phép khách hàng tham gia tích cực vào phân tích yêu cầu để xác