Chương 3: Kiểm chứng mô hình Aspect-UML

Chương 3: Kiểm chứng mô hình Aspect-UML

1. Giới thiệu về Alloy

   1. Alloy[4] là gì?

1. Tính chất của ngôn ngữ alloy

• 
  Đối các mô hình hữu hạn alloy có thể hữu hạn phạm vi kiểm tra: phân tích được đầy đủ các đối tượng đặc tả
  
• 
  Alloy cho phép kiểm tra vô hạn các mô hình vì kiểm tra hữu hạn không nhận được phản ánh đúng từ mô hình cần đặc tả
  
• 
  Alloy có khả năng đặt quan hệ logic giữa các đối tượng trong mô hình
  
• 
  Tự động phân tích và kiểm tra tính đứng đắn của các mô hình
  
• 
  Về cấu trúc dữ liệu:
  
  • 
    Xử lý vụng về
    
  • 
    Chức năng đệ quy khó diễn tả
    

3. Cấu trúc một chương trình Alloy

sig A{…}

assert a { …}

check a scope

pred P () {…}

run P

Ý nghĩa:

– fact F: nghĩa là giả sử ràng buộc F vững chắc

–assert a: tin tưởng rằng A sau F

–check a : tìm một ví dụ không đáp ứng A và F

– pred: định nghĩa sự ràng buộc P

– run: tìm ra 1 instance thỏa mãn P và F

4. Khai báo trong alloy

• 
  Sig Object{} định nghĩa một lớp đối tượng
  
• 
  Trừu tượng sig Object ()là trừu tượng sig không có các thành phần ngoại trừ những phần mở rộng của nó
  
• 
  SigFile extends Object ()-sự thiêt lập này có thể được giới thiệu là một tập hợp con của tập khác
  

1. Các ký hiệu

• 
  Sig A{}
  
• 
  sig B extends A {} (nghĩa là B trong A)
  
• 
  sig C extends A {}(C trong A)
  

2. Khai báo các liên kết

sigObject{}

sigDir extends Object {

entries: set Object,

parent: lone Dir

}

1. Các trường

• 
  Sig A{f: set X}
  
• 
  Sig B extends A{g:set Y}
  

f: A-> X

1. Các dạng thiết lập

• 
  Lone: chỉ không hoặc một
  
• 
  All: bất kì số nào
  
• 
  One: chỉ duy nhất một
  
• 
  Some: một hoặc nhiều hơn
  

1. Facts và Assertions

• 
  Fact
  
  • 
    Hạn chế được những giả đình luôn luôn giữ(ví dụ như sử dụng các không gian hạn chế của các bộ đếm)
    
  • 
    Một mô hình có thể có bất kỳ các con số của fact
    

fact { all z: A | F }

• 
  Assert: sự liên kết có ý đi theo các fact của mô hình có thể kiểm tra bằng cách sử dụng các lệnh kiểm tra
  

6. Các hằng số và các toán tử

• 
  Hằng:
  
  • 
    None = tập rỗng.
    
  • 
    Univ = tập phổ biến
    
  • 
    Iden = đồng nhất.
    
• 
  Các toán tử(Operators):
  
  • 
    Set operators:
    
    • 
      +: hợp nhất
      

• 
  &: giao nhau
  

• 
  -: hiệu số
  

• 
  in : tập con
  

sister in sibling

• 
  =: bằng nhau
  
• 
  Relational operators:
  
  • 
    . : dot (phép nối)
    
  • 
    ->: mũi tên (product)
    
  • 
    ^ : transitive closure
    
  • 
    *: reflexive- transitive closure
    
  • 
    ~: đảo vế
    
  • 
    [] : box (join)
    
  • 
    <: : domain restriction
    
  • 
    :> : range restriction
    
  • 
    ++ : override
    
• 
  Toán tử logic
  
  • 
    ! : negation
    
  • 
    && : conjunction (and)
    
  • 
    || : disjunction (OR)
    
  • 
    => : implication
    
  • 
    else : alternative
    
  • 
    <=> : bi-implication (IFF)
    
• 
  Logic Cardinalities
  
  • 
    = equals
    
  • 
    < less than
    
  • 
    > greater than
    
  • 
    =< less than or equal to
    
  • 
    >= greater than or equal to
    
  • 
    #r number of tuples in r
    
  • 
    0,1,... integer literal
    
  • 
    + plus
    
  • 
    - minus
    

1. Predicates

• 
  Một pred là tên của một ràng buộc
  
• 
  Không hoặc nhiều hơn sự khai báo cho những lí luận
  
• 
  Có thể sử dụng để đại diện cho một quá trình thực thi
  
• 
  Chỉ được dùng khi được gọi (không như fact)
  

2. Đặc tả mô hình Aspect-UML trong Alloy

   1. Mô hình Aspect UML

Mô hình Aspect-UML có thể được kiểm tra từ các xung đột tương tác aspect. Một cách để tự động quá trình kiểm chứng là chuyển đổi mô hình Aspect- UML sang ngôn ngữ đặc tả Alloy. Alloy cung cấp một ngôn ngữ đặc tả mô hình đơn giản dựa trên logic đầu tiên như phân tích mô hình và công cụ mô phỏng[]. Một mô hình Alloy được soạn thảo từ một tập hợp các signature xác đinh tập hợp đối tượng và các mối quan hệ giữa chúng. Mô hình này có thể được thêm các rang buộc bởi predicates và assertions. Một mô hình là trừu tượng cái mà thực sự xác định một tập hợp có thể vô hạn của một mô hình hữu hạn. Alloy thực thi đặc tả mô hình bằng cách tìm kiếm mô hình cá biệt đáp ứng một số đặc điểm của đặc tả. Một mô hình có thể được kiểm tra là có giá trị hay là thỏa mãn bên trong các ràng buộc một mô hình cá biệt. Thật vậy, các phân tích Alloy giới hạn việc tìm kiếm các mô hình cá biệt cái mà kích cỡ(về các đối tượng) là thấp hơn cho một số ràng buộc cố đinh bời người sử dụng. Alloy khẳng định hướng tiếp cận đặc tả của nó bằng việc đề xuất giả thuyết phạm vi nhỏ mà theo đó các counterexample phế bỏ một mô hình có khuynh hướng xảy ra trong các ví dụ mô hình nhỏ.

2. Mô hình viễn thông

• 
  Tính năng thời gian được liên quan tới thời gian kết nối và giữ thời gian kết nối tổng số cho mỗi khách hàng. Nó xảy ra ở trong khoảng đầu đến cuối của mỗi kết nối.
  
• 
  Tính năng thanh toán có liên quan tới việc tính phí khách hàng cho các cuộc gọi của họ. Một tính phí cho mõi kết nối được tính toán và khi chấm dứt kết nôi nó được bổ sung vào hóa đơn của khách hàng phù hợp
  
• 
  Tính năng ngắt được sử dụng để xử lý các đường truyền bận bằng cách ngắt cuộc gọi. Nó can thiệp vào lúc bắt dầu kết nối bằng cách kiểm tra nếu đích là bận , trong trường hợp này cuộc gọi bị gián đoạn.
  

Hình 6: Mô hình class cho hệ thống viễn thông

Hình trên thể hiện bằng cách nào viêc tính giờ, thanh toán và các yêu cầu ngắt cuộc gọi được tích hợp vào trong biểu đồ lớp UML, sử dụng Aspect UML thích hợp. Những yêu cầu crosscutting được bắt tương ứng bằng aspect Timing, Billing và Interrupting cái mà được mô tả như các lớp trong UML được mô tả với stereotype <>. Những aspect này cắt ngang ứng dụng cơ bản thông qua 2 point cut được mô hình như một interface đặc biệt có tên là OpComplete và OpDrop. Một quan hệ phụ thuộc <> thì thường được sử dụng để liên kết mỗi join point mà nó biểu hiện. Interface của pointcut OpComplete chứa một biểu thức trừu tượng được đặt tên là opComplete(c:Connection) được thực thi khi một trong những joinpoint của nó đạt được. Tương tự interface của OpDrop chức một biểu thức trừu tượng opDrop(c:Connection). Hãy xem xét về ví dụ aspect Timing( aspect Billing và aspect Interrupting cũng tương tự). Nó thực thi cả interface ponitcut OpComplete và OpDrop và do đó cung cấp 1 số advice tương ứng để thực hiện mỗi cái trong chúng.

3. Đặc tả mô hình Aspect UML bằng Alloy­

Bảng 2: Chuyển đổi thành phần cấu trúc mô hình Aspect UML sang Alloy.

Các class và aspect được chuyển thành các khai báo signature trong Alloy. Các thuộc tính của một lớp hoặc của 1 aspect thì được chuyển thành các mối quan hệ trong các signature tương đồng. Tương tự các liên kết giữa những class và hoặc aspect thì được dịch thành các mối quan hệ. Đối với kiểu người dùng tự định nghĩa kiểu dữ liệu tập hợp , cái mà là tập hợp các giá trị không được có mặt trong UML( ví dụ như kết nối hay ngắt kết nối trong trường hợp chúng tôi nghiên cứu), các enumeration con được chuyển đổi thành các signature kế thừa từ signature được định nghĩa bởi cái kiểu enumeration. Ví dụ, đoạn code Alloy sau đặc tả lớp Connection xuất hiện ở trong mô hình lớp của ứng dụng viễn thông (hình 5).

Sig Connection{

status: Status,

origin, destination: Device

}

abstract sig Status{}

Đối với aspect Timing, nó được xác định bời đoạn code Alloy sau:

sig Timing{

effectiveConnections: set Connection,

getTimer: effectiveConnections → some Timer

}

sig Timer{

c : Connection

}

Chuyển đổi ngữ pháp của chú thích Aspect UML sang Alloy

Để giải quyết ngữ nghĩa của các tương tác aspect tại join point, mô hình UML đã được mở rộng với các chú thích xác định những giao ước riêng lẻ mà mỗi phương thức / biểu thức advice (thực thi tại join point) phải được lưu ý. Những giao ước đó được khai báo ở các điều kiện trước và sau (post/pre condition). May mắn thay Alloy cũng cho chúng ta đặc tả những ràng buộc mà biểu thức(phương thức và advice tại join point) phải thỏa mãn thông qua việc sử dụng các predicate. Ví dụ: xét 1 phương thức op() với tham số s thuộc kiểu T có hành vi được xác định bởi điều kiện trước là s>0 và điều kiện sau khi thực thi là s<100, Alloy mô tả ràng buộc này predicate sau:

pred op(s, s′:T) {

// precondition

s>0

// postcondition

Trong một mô hình Aspect UML chính xác, các tương tác aspect tại join point không bao giờ là nguyên nhân sự vi phạm của các điều kiện riêng lẻ trước và sau của hàm, bất kể bối cảnh thực thi có được lưu tâm. Trong mô hình Alloy, điều này có nghĩa là việc kết hợp các aspect sẽ yêu cầu các thành phần của các ràng buộc của advice với những với ràng buộc join point có liên quan. Nếu không có xung đột, tất cả các trường hợp của mô hình có thể đáp ứng các ràng buộc, mà gây ra bởi việc kết hợp các aspect. Nếu không có xung đột, tất cả các trường hợp của mô hình có thể đáp ứng các ràng buộc, mà gây ra bởi việc kết hợp các aspect.

Để minh họa điều này, chúng ta hãy xem xét các predicate của Alloy mà chúng tôi định nghĩa để hạn chế các thực thi kết hợp các phương thức và advice tại join point Drop trong ứng dụng viễn thông. Trong các bước sau đây, chúng tôi sẽ giải thích làm thế nào để xác định (1) những ràng buộc của phương thức drop(), (2) ràng buộc của advice opDropTiming và opDropBilling,(3) những ràng buộc áp đặt bởi các thành phần advice, và cuối cùng (4) các ràng buộc tạo ra bời việc kết hợp các advice tại join point drop().

(1) Các hành vi của phương thức drop() phải thỏa mãn các ràng buộc áp đặt bởi những điều kiện trước và sau của nó. Điều kiện trước phải được thoải mãn bởi mô hình mà mỗi phương thức được thực thi và phương thức thực thi phải rời khỏi mô hình trong trang thái thỏa mãn những điều kiện sau. Trong trường hợp này, trạng thái kết nối được thiết lập để kết nôi khi drop() được gọi, trong khi việc thức thi của nó sau này phải bị hủy để ngắt kết nối. Trạng thái trước và sau việc kết nối tương ứng được nắm bắt bởi các biến c và c’. Những ràng buộc này có thể được đặc tả trong Alloy sử dụng các định nghĩa predicate như bên dưới :

pred drop(c, c′: Connection) {

c.status= connected &&

c′.status=disconnected &&

c′.origin.d_status=idle &&

c′.destination.d_status=idle

}

(2) Hành vi của advice opDrop trong aspect Timing được xác định một cách tương tự .Các điều kiện trước của nó ràng buộc giờ liên quan tới việc kết nối (đang bị ngắt) không có một đăng kí nào về thời gian kết nối. Ngược lại, điều kiện sau tác động mạnh mẽ lên thời gian có đăng kí kết nối giá trị thời gian phải lớn hơn hoặc bằng 0. Những ràng buộc này buộc bộ đếm giờ phải thay đổi trạng thái, cái mà hậu quả ảnh hưởng lớn đến aspect Timing cũng để thay đổi trạng thái nó phải cập nhật các trường bao gồm danh sách các bộ tính giờ. Tham số t và t’ được sử dụng để biểu thị trạng thái của aspect Timing trước và sau khi thức thi advice opDrop. Đối với việc kết nối, cá trạng thái của nó (mô hình bởi tham số c )vẫn giữ nguyên. Predicate Alloy sau được sử dụng để xác định ràng buộc áp đặt bởi advice opDrop:

t.useTimer[c].connectionTime=Null &&

t′.useTimer[c].connectionTime≥ 0 }

Một predicate Alloy phải được định nghĩa để xác định các ràng buộc áp đặt bởi các điều kiện trước vào sau của mỗi advice và join point phương thức được xuất hiện trong mô hình Aspect UML. Trong trường hợp advice opDrop của Billing, các điều khiện trước và sau có tác động mạnh mẽ lên tổng số hóa đơn của người gọi để tăng thêm nếu bộ đếm thời gian đã được ghi lại một thời gian kết nối lớn hơn hoặc bằng 0. Do vậy chỉ có hóa đơn thay đổi trạng thái. Trạng thái này có thể được quan sát nhờ tham số b và b’ trong predicate opDropBilling bên dưới. Predicate này xác định một ràng buộc bắt buộc bởi thực thi advice opDrop của Billing.

pred OpDropBilling(b,b′:Billing, t:Timing,c:Connection) {

(t.useTimer[c].connectionTime >= 0) &&

(b.useBill[c.origin.owner].charge ≤

b′.useBill[c.origin.owner].charge)

}

Hầu hết ta có thể thấy được aspect Billing ngầm đòi hỏi các dịch vụ của aspect Timing. Cách xây dựng này không được khuyến cáo, các aspect nên được định nghĩa độc lập với nhau.Tuy nhiên nếu aspect Timing được thu lại, phân tích của chung tôi có thể phát hiện lỗi của aspect Billing tại join point drop.

Ví dụ Timing và Billing không là các aspect đồng thời tương tác tại join point drop. Advice onDrop tương ứng của chúng cần được biên soạn trong một trật tự khó mà xác định được. Để tác động đến Alloy đi qua tất cả các advice được yêu cầu, chúng ta định nghĩa một predicate được gọi là executeOpDrop cái mà cho phép Alloy có sự lựa chọn thoải mái để cho phép điều kiện sau của predicate opDropBilling tiếp theo điều kiện trước của predicateOpDropTiming hoặc ngược lại. Vậy khi kiểm tra tính hợp lệ của assertion, bộ phân tích alloy sẽ đi qua tất cả các thực thi các predicate, vì thế cố gắng tất cả các yêu cầu của hai advice pre và post constraint.

pred executeOpDrop(t,t′:Timing, b,b′:Billing,c:Connection){

OpDropTiming(t,t′,c) && OpDropBilling(b,b′,t′,c)

||

OpDropBilling(b,b′,t,c) && OpDropTiming(t,t′,c) }

pred weaveAtOpDrop(t,t′: Timing, b,b′:Billing, c,c′: Connection)

{ drop(c,c′) &&

executeOpDrop(t,t′,b,b′,c′) &&

(c′.status=disconnected)

}

4. Kiểm chứng mô hình Aspect UML sử dụng Alloy

• 
  Sự vi phạm của thuộc tính cục bộ
  
• 
  Sự vi phạm của thuộc tính toàn cục
  

1. Kiểm chứng sự vi phạm của thuộc tính cục bộ

assert testWeaveAtOpDrop {

all c: Connection, t:Timing, b: Billing |

some c′: Connection, t′:Timing, b′: Billing |

(c!=c′)&&(t!=t′)&&(b!=b′) => weaveAtOpDrop(t,t′, b,b′, c,c′)

}

Nếu khẳng định không hợp lệ thì sẽ xuất hiện counterexample được sinh ra bởi công cụ phân tích Alloy.

2. Kiểm chứng sự vi phạm của các thuộc tính toàn cục

• 
  Với mỗi trạng thái của hệ thống số lượng các kết nối luôn nhỏ hơn hoặc bằng 50.
  
• 
  Trạng thái của tất cả các thiết bị ( nguồn hoặc đích ) tham gia vào các kết nối thì không nhàn rỗi.
  

pred limitedConnectedConnections {

#{allc:Connection | c.status=connected}≤ 50 }

pred deviceIdle {

alld:Device,somec:Connection |

(dinc.(origin+destination))&&(c.status=connected)

=> (d.d−status!=idle)

}.

4. Chương 4 : Kết luận

[1] http://www.cs.bham.ac.uk/~bxb/UML2Alloy/

[3] Farida Mostefaoui DIRO,Julie Vachon , University of Monreal Quebec, Canada Verification of Aspect –UML models using alloy, 2007

[4] Daniel Jackson , Solfware Abstraction: Logic, Language, and Analysis,

[5] J.VachonandF.Mostefaoui.Achieving supplementary equirements using aspect-oriented development.In ICEIS, pages584–587, 2004