Bài giảng Đặc tả hình thức: Chương 7

LOGO

Đặc tả hình thức

Mô hình động trong Alloy

Nguyễn Thị Minh Tuyền

Nguyễn Thị Minh Tuyền 1

Các mô hình tĩnh

v Trong các buổi học trước

§  định nghĩa các mô hình dựa vào tập hợp và quan hệ

v Một instance của mô hình là một tập các giá trị thỏa mãn các ràng buộc được định nghĩa bởi multiplicity, fact,..

2 Nguyễn Thị Minh Tuyền Đặc tả hình thức

Các mô hình tĩnh

Person = {Matt, Sue} Man = {Matt} Woman = {Sue} Married = {} spouse = {} children = {} siblings = {}

Person = {Matt, Sue} Man = {Matt} Woman = {Sue} Married = {Matt, Sue} spouse = {(Matt,Sue), (Sue,Matt)} children = {} siblings = {}

Person = {Matt, Sue, Sean} Man = {Matt} Woman = {Sue} Married = {Matt, Sue} spouse = {(Matt,Sue), (Sue,Matt)} children = {(Matt,Sean), (Sue,Sean)} siblings = {}

3 Nguyễn Thị Minh Tuyền Đặc tả hình thức

Mô hình động

v Các mô hình tĩnh cho phép mô tả trạng

thái hợp lệ của một hệ thống động.

v Ta cũng có thể mô tả các chuyển đổi hợp

lệ giữa các trạng thái.

v Ví dụ:

§  Một người được sinh ra trước khi họ cưới §  Một người kết hôn trước khi có con §  Một người là con cho đến khi họ chết

4 Nguyễn Thị Minh Tuyền Đặc tả hình thức

Ví dụ

abstract sig Person {

children: set Person, siblings: set Person

} sig Man, Woman extends Person {} sig Married in Person {

spouse: one Married

}

5 Nguyễn Thị Minh Tuyền Đặc tả hình thức

Chuyển đổi

v Hai người cưới nhau:

§  Tại thời điểm t, spouse = {} §  Tại thời điểm t’, spouse = {(Matt, Sue), (Sue,Matt)}

v ⇒ Ta thêm khái niệm về thời gian vào

trong quan hệ spouse

6 Nguyễn Thị Minh Tuyền Đặc tả hình thức

Mô hình hóa chuyển đổi trạng thái

v Alloy không có khái niệm về chuyển đổi

trạng thái.

v Một phương pháp tổng quát và khá đơn

giản để mô hình hóa khía cạnh động của một hệ thống: §  thêm signature Time để biểu diễn thời gian §  thêm thành phần thời gian vào mỗi quan hệ mà nó sẽ

thay đổi theo thời gian.

7 Nguyễn Thị Minh Tuyền Đặc tả hình thức

Ví dụ

abstract sig Person {

children: set Person, siblings: set Person

} sig Man, Woman extends Person {} sig Married in Person {

spouse: one Married

}

8 Nguyễn Thị Minh Tuyền Đặc tả hình thức

sig Time{} abstract sig Person {

children: Person set -> Time, siblings: Person set -> Time

} sig Man, Woman extends Person {} sig Married in Person {

spouse: Married one -> Time

}

9 Nguyễn Thị Minh Tuyền Đặc tả hình thức

Các chuyển đổi

v Hai người cưới nhau

§  Tại thời điểm t, Married = {} §  Tại thời điểm t’, Married = {Matt, Sue}

v Thực tế, ta không thể có một signature

phụ thuộc thời gian, vì signature độc lập về thời gian. §  Ví dụ: quan hệ Married

Person = {Matt,Sue} Man = {Matt} Woman = {Sue} Married = {} spouse = {} children = {} siblings = {}

Person = {Matt, Sue} Man = {Matt} Woman = {Sue} Married = {Matt, Sue} spouse = {(Matt,Sue), (Sue,Matt)} children = {} siblings = {}

thời điểm t

thời điểm t’

10 Nguyễn Thị Minh Tuyền Đặc tả hình thức

Các chuyển đổi

v Một người được sinh ra §  Tại thời điểm t, Person = {} §  Tại thời điểm t’, Person = {Sue}

v Ta không thể thêm khái niệm được sinh ra vào signature Person vì signature độc lập về thời gian.

Person = {} Man = {} Woman = {} spouse = {} children = {} siblings = {}

Person = {Sue} Man = {} Woman = {Sue} spouse = {} children = {} siblings = {}

thời điểm t

thời điểm t’

11 Nguyễn Thị Minh Tuyền Đặc tả hình thức

Signature mang tính chất tĩnh

abstract sig Person {

children: Person set -> Time, siblings: Person set -> Time, spouse: Person lone -> Time

} sig Man, Woman extends Person {} sig Married in Person {

spouse: Married one -> Time

}

12 Nguyễn Thị Minh Tuyền Đặc tả hình thức

abstract sig Person {

children: Person set -> Time, siblings: Person set -> Time, spouse: Person lone -> Time

} sig Man, Woman extends Person {}

Ta cần thêm quan hệ sau, nhưng thêm vào đâu? alive: Person set -> Time

13 Nguyễn Thị Minh Tuyền Đặc tả hình thức

abstract sig Person {

children: Person set -> Time, siblings: Person set -> Time, spouse: Person lone -> Time alive: Person set -> Time

} sig Man, Woman extends Person {}

14 Nguyễn Thị Minh Tuyền Đặc tả hình thức

Ôn lại các ràng buộc

abstract sig Person {

children: Person set -> Time, siblings: Person set -> Time, spouse: Person lone -> Time, alive: set Time parents: Person set -> Time

} sig Man, Woman extends Person {} fun parents[] : Person->Person {~children} fact parentsDef {

all t: Time | parents.t = ~(children.t)

}

15 Nguyễn Thị Minh Tuyền Đặc tả hình thức

fact parentsDef {

all t: Time | parents.t = ~(children.t)

} -- Hai người có quan hệ huyết thống -- nếu họ có chung tổ tiên pred BloodRelatives [p, q: Person, t: Time]{

some p.*(parents.t) & q.*(parents.t)

}

16 Nguyễn Thị Minh Tuyền Đặc tả hình thức

fact static {

p in p.^(parents.t)

-- Một người không thể là tổ tiên của chính họ all t: Time | no p: Person | -- Không ai có nhiều hơn một bố -- và nhiều hơn một mẹ all t: Time | all p: Person |

lone (p.parents.t & Man) and lone (p.parents.t & Woman)

...

17 Nguyễn Thị Minh Tuyền Đặc tả hình thức

-- Anh chị em của một người p là những người -- khác p và có cùng bố mẹ với p all t: Time | all p: Person |

p.siblings.t = ({q: Person | p.parents.t = q.parents.t} – p )

-- Mỗi người có đàn ông/phụ nữ có gia đình thì có -- một vợ/chồng all t: Time | all p: Person |

let s = p.spouse.t |

(p in Man implies s in Woman) and (p in Woman implies s in Man)

...

18 Nguyễn Thị Minh Tuyền Đặc tả hình thức

... -- Hai người không thể vừa là vợ chồng -- vừa là anh em của nhau được all t: Time | no p: Person | some p.spouse.t and p.spouse.t in p.siblings.t -- Người ta không thể cưới người có -- quan hệ huyết thống all t: Time | no p: Person |

let s = p.spouse.t |

some s and BloodRelatives [p, p.spouse.t, t]

...

19 Nguyễn Thị Minh Tuyền Đặc tả hình thức

… -- một người không thể có con -- với người có quan hệ huyết thống với mình all t: Time | all p, q: Person |

(some (p.children.t & q.children.t) and p != q) implies not BloodRelatives [p, q, t]

-- quan hệ spouse là đối xứng all t: Time |

spouse.t = ~(spouse.t)

}

20 Nguyễn Thị Minh Tuyền Đặc tả hình thức

Chuyển đổi

v Một người được sinh ra §  Thêm vào quan hệ alive.

v Chú ý: ở đây không có yêu cầu một người

phải có bố mẹ.

Person = {Matt, Sue, Sean} Man = {Matt, Sean} Woman = {Sue} spouse = {} children = {} siblings = {} alive = {Sue}

Person = {Matt, Sue, Sean} Man = {Matt, Sean} Woman = {Sue} spouse = {} children = {} siblings = {} alive = {}

thời điểm t

thời điểm t’

21 Nguyễn Thị Minh Tuyền Đặc tả hình thức

v Một người được sinh ra §  Thêm vào quan hệ alive

Person = {Matt, Sue, Sean} Man = {Matt, Sean} Woman = {Sue} spouse = {(Matt,Sue), (Sue,Matt)} children = {(Matt,Sean), (Sue,Sean)} siblings = {} alive = {Matt, Sue, Sean}

Person = {Matt, Sue, Sean} Man = {Matt, Sean} Woman = {Sue} spouse = {(Matt,Sue), (Sue,Matt)} children = {} siblings = {} alive = {Matt, Sue}

22 Nguyễn Thị Minh Tuyền Đặc tả hình thức

Các chuỗi trạng thái

Person = {Matt, Sue, Sean} Man = {Matt, Sean} Woman = {Sue} spouse = {} children = {} siblings = {} alive = {Sue}

Person = {Matt, Sue, Sean} Man = {Matt, Sean} Woman = {Sue} spouse = {(Matt,Sue), (Sue,Matt)} children = {} siblings = {} alive = {Sue, Matt}

Person = {Matt, Sue, Sean} Man = {Matt, Sean} Woman = {Sue} spouse = {} children = {} siblings = {} alive = {}

Person = {Matt, Sue, Sean} Man = {Matt, Sean} Woman = {Sue} spouse = {(Matt,Sue), (Sue,Matt)} children = {(Matt,Sean), (Sue,Sean)} siblings = {} alive = {Sue, Matt, Sean}

23 Nguyễn Thị Minh Tuyền Đặc tả hình thức

Biểu diễn một chuyển đổi

v Một chuyển đổi có thể được mô hình hóa

như một vị từ giữa hai trạng thái: §  Trạng thái ngay trước khi chuyển đổi và §  Trạng thái ngay sau khi chuyển đổi.

v Ta định nghĩa nó như một vị từ với (ít

nhất) hai tham số hình thức: t, t’: Time v Các ràng buộc trên thời gian t (t’) mô hình

hóa trạng thái ngay trước (ngay sau) chuyển đổi.

24 Nguyễn Thị Minh Tuyền Đặc tả hình thức

Biểu diễn một chuyển đổi

v Ràng buộc điều kiện trước

§  Mô tả các trạng thái mà chuyển đổi áp dụng

v Ràng buộc điều kiện sau

§  Mô tả hiệu ứng của chuyển đổi khi sinh ra trạng thái

v Ràng buộc frame condition

§  Mô tả cái gì không thay đổi giữa trạng thái trước và

trạng thái sau khi chuyển đổi.

25 Nguyễn Thị Minh Tuyền Đặc tả hình thức

Ví dụ

pred marriage [m: Man, w: Woman, t,t': Time, ] { -- điều kiện trước

-- m và w phải sống trước khi cưới m+w in alive.t -- m và w chưa có gia đình no (m+w).spouse.t -- m và w không có quan hệ huyết thống với nhau not BloodRelatives [m, w, t]

-- điều kiện sau

-- sau khi cưới w là vợ của m m.spouse.t' = w -- sau khi cưới m là chồng của w -- (dư thừa)

-- frame condition ?? }

26 Nguyễn Thị Minh Tuyền Đặc tả hình thức

Frame condition

v Những quan hệ nào không bị ảnh hưởng bởi quan

hệ hôn nhân? v Có 5 quan hệ:

§  children, parents, siblings §  spouse §  alive

v Quan hệ parents và siblings được định nghĩa dựa vào quan hệ children. Vì vậy frame condition chỉ xem xét các quan hệ children, spouse và alive.

27 Nguyễn Thị Minh Tuyền Đặc tả hình thức

Các vị từ frame condition

pred noChildrenChangeExcept [ps: set Person

t,t': Time] {

all p: Person - ps |

p.children.t' = p.children.t

} pred noSpouseChangeExcept [ ps: set Person

t,t': Time] {

all p: Person - ps |

p.spouse.t' = p.spouse.t

} pred noAliveChange [t,t': Time] {

alive.t’ = alive.t

}

28 Nguyễn Thị Minh Tuyền Đặc tả hình thức

Ví dụ: marriage

pred marriage [m: Man, w: Woman, t,t': Time]{

-- điều kiện trước m+w in alive.t no (m+w).spouse.t not BloodRelatives [m, w, t] -- điều kiện sau m.spouse.t' = w -- frame condition noChildrenChangeExcept [none, t, t’] noSpouseChangeExcept [m+w, t, t’] noAliveChange [t, t’]

}

29 Nguyễn Thị Minh Tuyền Đặc tả hình thức

Instance của marriage

open ordering [Time] as T … pred marriageInstance { some t: Time | some m: Man | some w: Woman |

let t' = T/next [t] |

marriage [m, w, t, t’]

} run {marriageInstance }

30 Nguyễn Thị Minh Tuyền Đặc tả hình thức

pred birth [t, t': Time]{

-- điều kiện trước và điều kiện sau one p: Person | p !in alive.t and alive.t’ = alive.t + p -- frame condition noChildrenChangeExcept [none, t, t'] noSpouseChangeExcept [none, t, t']

}

31 Nguyễn Thị Minh Tuyền Đặc tả hình thức

pred birthFromParents [m, w: Person, t,t': Time]{

-- điều kiện trước p !in alive.t -- điều kiện sau

-- điều kiện trước về m, w m+w in alive.t m.spouse.t = w -- điều kiện trước và điều kiện sau về một đứa con p nào đó one p: Person | { alive.t’ = alive.t + p m.children.t’ = m.children.t + p w.children.t’ = w.children.t + p } -- frame condition noChildrenChangeExcept [m+w, t, t’] noSpouseChangeExcept [none, t, t’]

}

32 Nguyễn Thị Minh Tuyền Đặc tả hình thức

pred birthInstance { some t: Time | let t' = T/next [t] | birth [t, t']

} pred birthFromParentsInstance {

some t: Time | some m, w: Person | let t' = T/next [t] | birthFromParents [m, w, t, t’]

}

33 Nguyễn Thị Minh Tuyền Đặc tả hình thức

Đặc tả hệ thống chuyển đổi

v Một hệ thống chuyển đổi là một tập các trace: các chuỗi tuần tự các bước liên quan đến thời gian được phát sinh ra từ các phép toán. v Với mỗi trace:

§  Bước thời gian đầu tiên thỏa mãn điều kiện đầu. §  Mỗi cặp các bước kế tiếp nhau liên quan đến nhau

bởi:

•  một toán tử birth, hoặc •  một toán tử marriage, hoặc •  một toán từ birthFromParents

34 Nguyễn Thị Minh Tuyền Đặc tả hình thức

Đặc tả bước đầu tiên

pred init [t: Time] { no children.t no spouse.t no alive.t

}

35 Nguyễn Thị Minh Tuyền Đặc tả hình thức

Đặc tả của một trace

fact Trace {

init [T/first] all t: Time - T/last | let t’ = T/next [t] | birth [t, t’] or one m: Man | one w: Woman | marriage [m, w, t, t’] or birthFromParents [m, w, t, t’]

} run {Trace and some Man and some Woman}

36 Nguyễn Thị Minh Tuyền Đặc tả hình thức

Ràng buộc trên quan hệ alive

fact staticAlive {

all t: Time | all p: Person | let mainRels = children + spouse |

p !in alive.t implies ( no p.mainRels.t and no q: Person | p in q.mainRels.t )

}

37 Nguyễn Thị Minh Tuyền Đặc tả hình thức

Bài giảng Đặc tả hình thức: Chương 7 - Nguyễn Thị Minh Tuyền

LOGO

Đặc tả hình thức

Mô hình động trong Alloy

Các mô hình tĩnh

v Trong các buổi học trước

v Một instance của mô hình là một tập các giá trị thỏa mãn các ràng buộc được định nghĩa bởi multiplicity, fact,..

Các mô hình tĩnh

Mô hình động

v Các mô hình tĩnh cho phép mô tả trạng

thái hợp lệ của một hệ thống động.

v Ta cũng có thể mô tả các chuyển đổi hợp

lệ giữa các trạng thái.

v Ví dụ:

Ví dụ

abstract sig Person {

children: set Person, siblings: set Person

} sig Man, Woman extends Person {} sig Married in Person {

spouse: one Married

}

Chuyển đổi

v Hai người cưới nhau:

v ⇒ Ta thêm khái niệm về thời gian vào

trong quan hệ spouse

Mô hình hóa chuyển đổi trạng thái

v Alloy không có khái niệm về chuyển đổi

trạng thái.

v Một phương pháp tổng quát và khá đơn

giản để mô hình hóa khía cạnh động của một hệ thống: § thêm signature Time để biểu diễn thời gian § thêm thành phần thời gian vào mỗi quan hệ mà nó sẽ

Ví dụ

abstract sig Person {

children: set Person, siblings: set Person

} sig Man, Woman extends Person {} sig Married in Person {

spouse: one Married

}

sig Time{} abstract sig Person {

children: Person set -> Time, siblings: Person set -> Time

} sig Man, Woman extends Person {} sig Married in Person {

spouse: Married one -> Time

}

Các chuyển đổi

v Hai người cưới nhau

v Thực tế, ta không thể có một signature

phụ thuộc thời gian, vì signature độc lập về thời gian. § Ví dụ: quan hệ Married

Các chuyển đổi

v Một người được sinh ra § Tại thời điểm t, Person = {} § Tại thời điểm t’, Person = {Sue}

v Ta không thể thêm khái niệm được sinh ra vào signature Person vì signature độc lập về thời gian.

Signature mang tính chất tĩnh

abstract sig Person {

children: Person set -> Time, siblings: Person set -> Time, spouse: Person lone -> Time

} sig Man, Woman extends Person {} sig Married in Person {

spouse: Married one -> Time

}

abstract sig Person {

children: Person set -> Time, siblings: Person set -> Time, spouse: Person lone -> Time

} sig Man, Woman extends Person {}

Ta cần thêm quan hệ sau, nhưng thêm vào đâu? alive: Person set -> Time

abstract sig Person {

children: Person set -> Time, siblings: Person set -> Time, spouse: Person lone -> Time alive: Person set -> Time

} sig Man, Woman extends Person {}

Ôn lại các ràng buộc

abstract sig Person {

} sig Man, Woman extends Person {} fun parents[] : Person->Person {~children} fact parentsDef {

fact parentsDef {

} -- Hai người có quan hệ huyết thống -- nếu họ có chung tổ tiên pred BloodRelatives [p, q: Person, t: Time]{

fact static {

-- Anh chị em của một người p là những người -- khác p và có cùng bố mẹ với p all t: Time | all p: Person |

-- Mỗi người có đàn ông/phụ nữ có gia đình thì có -- một vợ/chồng all t: Time | all p: Person |

... -- Hai người không thể vừa là vợ chồng -- vừa là anh em của nhau được all t: Time | no p: Person | some p.spouse.t and p.spouse.t in p.siblings.t -- Người ta không thể cưới người có -- quan hệ huyết thống all t: Time | no p: Person |

… -- một người không thể có con -- với người có quan hệ huyết thống với mình all t: Time | all p, q: Person |

-- quan hệ spouse là đối xứng all t: Time |

Chuyển đổi

v Một người được sinh ra § Thêm vào quan hệ alive.

v Chú ý: ở đây không có yêu cầu một người

phải có bố mẹ.

v Một người được sinh ra § Thêm vào quan hệ alive

Các chuỗi trạng thái

Biểu diễn một chuyển đổi

v Một chuyển đổi có thể được mô hình hóa

như một vị từ giữa hai trạng thái: § Trạng thái ngay trước khi chuyển đổi và § Trạng thái ngay sau khi chuyển đổi.

v Trong các buổi học trước

v Một instance của mô hình là một tập các giá trị thỏa mãn các ràng buộc được định nghĩa bởi multiplicity, fact,..

v Các mô hình tĩnh cho phép mô tả trạng

v Ta cũng có thể mô tả các chuyển đổi hợp

v Ví dụ:

v Hai người cưới nhau:

v ⇒ Ta thêm khái niệm về thời gian vào

v Alloy không có khái niệm về chuyển đổi

v Một phương pháp tổng quát và khá đơn

giản để mô hình hóa khía cạnh động của một hệ thống: §  thêm signature Time để biểu diễn thời gian §  thêm thành phần thời gian vào mỗi quan hệ mà nó sẽ

v Hai người cưới nhau

v Thực tế, ta không thể có một signature

phụ thuộc thời gian, vì signature độc lập về thời gian. §  Ví dụ: quan hệ Married

v Một người được sinh ra §  Tại thời điểm t, Person = {} §  Tại thời điểm t’, Person = {Sue}

v Ta không thể thêm khái niệm được sinh ra vào signature Person vì signature độc lập về thời gian.

v Một người được sinh ra §  Thêm vào quan hệ alive.

v Chú ý: ở đây không có yêu cầu một người

v Một người được sinh ra §  Thêm vào quan hệ alive

v Một chuyển đổi có thể được mô hình hóa

như một vị từ giữa hai trạng thái: §  Trạng thái ngay trước khi chuyển đổi và §  Trạng thái ngay sau khi chuyển đổi.

v Ta định nghĩa nó như một vị từ với (ít

nhất) hai tham số hình thức: t, t’: Time v Các ràng buộc trên thời gian t (t’) mô hình

v Ràng buộc điều kiện trước

v Ràng buộc điều kiện sau

v Ràng buộc frame condition

v Một hệ thống chuyển đổi là một tập các trace: các chuỗi tuần tự các bước liên quan đến thời gian được phát sinh ra từ các phép toán. v Với mỗi trace: