LOGO
Đặc tả hình thức
Mô hình minh họa: Hotel Room Locking
Nguyễn Thị Minh Tuyền
Nguyễn Thị Minh Tuyền 1
Hotel Room Locking
2 Nguyễn Thị Minh Tuyền Đặc tả hình thức
Vấn đề đặt ra
v Mô hình hóa bằng Alloy hệ thống khóa cửa sử dụng thẻ từ để đóng mở cửa phòng khách sạn. § Khi đã tạo thẻ mới cho một phòng thì khách trước đó
không thể vào phòng bằng thẻ cũ được. v Mô hình hóa cả khía cạnh tĩnh và
động của hệ thống.
3 Nguyễn Thị Minh Tuyền Đặc tả hình thức
Mô tả vấn đề
v Khách sạn sử dụng một mã số khóa mới cho
khách hàng tiếp theo § Thiết lập lại mã khóa mới để đảm bảo mã số khóa được lưu
trên thẻ trước đó không hoạt động nữa.
§ Bộ khóa là một đơn vị độc lập, đơn giản (sử dụng pin) với một
bộ nhớ lưu giữ mã số hiện tại.
v Thiết bị phần cứng phát sinh một chuỗi các
số ngẫu nhiên.
v Bộ khóa chỉ mở được hoặc bằng mã số khóa hiện tại hoặc mã số khóa tiếp theo của nó. § Nếu một mã số khóa tiếp theo được thiết lập,
• mã số khóa tiếp theo đó trở thành mã số khóa hiện tại và • mã số khóa trước đó sẽ không được chấp nhận nữa.
4 Nguyễn Thị Minh Tuyền Đặc tả hình thức
v Không yêu cầu giao tiếp giữa lễ tân và
khóa cửa. v Bằng cách
§ đồng bộ hóa giữa lễ tân và khóa cửa được khởi tạo
lần đầu, và
§ sử dụng cùng bộ phát sinh mã số ngẫu nhiên, § => lễ tân có thể lưu giữ thông tin của mã khóa hiện
tại với cửa.
5 Nguyễn Thị Minh Tuyền Đặc tả hình thức
Signatures và Fields
v Các signature: Time, Key, Room, Guest,
FrontDesk
v Key là mã số khóa được lưu trên thẻ từ v FrontDesk lưu một ánh xạ giữa mỗi phòng
và mã số khóa gần nhất của nó (nếu có) và khách hàng hiện tại của nó.
v Mỗi phòng (khóa) có một tập các mã số
khóa liên quan và có chính xác một mã số khóa hiện tại tại một thời điểm.
v Mỗi mã số khóa thuộc về nhiều nhất một
phòng.
6 Nguyễn Thị Minh Tuyền Đặc tả hình thức
Signatures và Fields
module hotel open util/ordering [Time] as TO open util/ordering [Key] as KO sig Key {} sig Time {} -- Mỗi phòng có một tập các mã số khóa, -- và một mã số khóa hiện tại sig Room {
keys: set Key, currentKey: keys one -> Time
}
7 Nguyễn Thị Minh Tuyền Đặc tả hình thức
Signatures và Fields
... -- Khách giữ một tập các mã số khóa tại một thời điểm sig Guest {
keys: Key -> Time
lastKey: ánh xạ một phòng tới mã số khóa gần nhất occupant: ánh xạ một phòng tới khách
được gán vào phòng đó
} -- FrontDesk gồm hai quan hệ: -- -- -- one sig FrontDesk {
lastKey: (Room -> lone Key) -> Time, occupant: Room -> Guest -> Time
}
8 Nguyễn Thị Minh Tuyền Đặc tả hình thức
Biểu đồ mô hình cho hệ thống
currentKey.
? keys
Room
Key
keys.
Guest
9 Nguyễn Thị Minh Tuyền Đặc tả hình thức
Ràng buộc và thao tác
v Ràng buộc về Room v Phát sinh khóa mới v Khách đến nhận phòng v Khách trả phòng v Trạng thái khởi tạo v Phát sinh trace
10 Nguyễn Thị Minh Tuyền Đặc tả hình thức
Ràng buộc về Room
v Mỗi mã số khóa thuộc về nhiều nhất 1
phòng
fact {
all k: Key | lone keys.k
}
11 Nguyễn Thị Minh Tuyền Đặc tả hình thức
Phát sinh khóa mới
v Cho trước
§ một mã số khóa k và § một tập các mã số khóa ks, § hàm nextKey trả về khóa nhỏ nhất (trong thứ tự các
khóa) trong tập ks theo sau k.
fun nextKey [k: Key, ks: set Key]: set Key{
KO/min [KO/nexts[k] & ks]
}
12 Nguyễn Thị Minh Tuyền Đặc tả hình thức
Trạng thái khởi tạo
module examples/hotel open util/ordering [Time] as TO open util/ordering [Key] as KO sig Key {} sig Time {} sig Room {
keys: set Key, currentKey: Key one -> Time
} sig Guest {
keys: Key -> Time
} one sig FrontDesk {
lastKey: (Room -> lone Key) -> Time, occupant: (Room -> Guest) -> Time
}
13 Nguyễn Thị Minh Tuyền Đặc tả hình thức
Trạng thái khởi tạo
pred init [t: Time] {
-- không có khách nào có mã số khóa no Guest.keys.t -- Danh sách tại lễ tân chỉ ra rằng không có -- phòng nào được thuê no FrontDesk.occupant.t -- thông tin về mã số khóa của mỗi phòng tại -- lễ tân được đồng bộ với mã số khóa hiện tại all r: Room |
r.(FrontDesk.lastKey.t) = r.currentKey.t
}
14 Nguyễn Thị Minh Tuyền Đặc tả hình thức
Khách đến nhận phòng
pred entry [ g: Guest, r: Room, k: Key, t, t': Time ]
v Điều kiện trước:
§ Mã số khóa được sử dụng để mở phòng là một trong các mã số khóa
mà khách hàng đang giữ
v Điều kiện trước và điều kiện sau:
§ Mã số khóa trên thẻ
• hoặc khớp với mã số khóa hiện tại của khóa và mã số này không thay đổi
(không phải là khách mới)
• hoặc mã số khóa trên thẻ khớp với mã số khóa tiếp theo của khóa (khách
mới).
v Frame conditions:
§ Không thay đổi trạng thái của các phòng khác, § hoặc không thay đổi việc thiết lập lại các mã số khóa giữ bởi khách, § hoặc không thay đổi thông tin tại lễ tân.
15 Nguyễn Thị Minh Tuyền Đặc tả hình thức
Frame condition
pred noFrontDeskChange [t,t': Time]{
FrontDesk.lastKey.t = FrontDesk.lastKey.t' FrontDesk.occupant.t = FrontDesk.occupant.t'
} pred noRoomChangeExcept [rs: set Room, t,t': Time]{
all r: Room - rs |
r.currentKey.t = r.currentKey.t'
} pred noGuestChangeExcept [gs: set Guest, t,t': Time]{
all g: Guest - gs | g.keys.t = g.keys.t'
}
16 Nguyễn Thị Minh Tuyền Đặc tả hình thức
pred entry [ g: Guest, r: Room, k: Key, t, t': Time ] {
(k = ck.t and ck.t' = ck.t)
or (k = nextKey [ck.t, r.keys] and ck.t' = k)
-- mã số khóa được sử dụng để mở khóa là -- một trong các mã số khóa mà khách hàng đang giữ k in g.keys.t -- điều kiện trước và điều kiện sau let ck = r.currentKey | -- không phải là khách hàng mới -- khách hàng mới -- frame conditions noRoomChangeExcept [r, t, t’] noGuestChangeExcept [none, t, t’] noFrontDeskChange [t, t’]
}
17 Nguyễn Thị Minh Tuyền Đặc tả hình thức
Thao tác check-out
pred checkout [ g: Guest, t,t': Time ]
v Điều kiện trước:
§ Khách hàng ở một hoặc nhiều phòng.
v Điều kiện sau:
§ Phòng của khách hàng ở trạng thái trống
v Frame condition:
§ Không có gì thay đổi trừ mối quan hệ occupant
18 Nguyễn Thị Minh Tuyền Đặc tả hình thức
Check-out
one sig FrontDesk {
lastKey: (Room -> lone Key) -> Time, occupant: (Room -> Guest) -> Time
} pred checkout [ g: Guest, t,t': Time ]{
-- khách ở một hoặc nhiều phòng some occ.t.g -- phòng của khách ở tình trạng trống occ.t' = occ.t – (Room -> g)
let occ = FrontDesk.occupant | { } -- frame condition FrontDesk.lastKey.t = FrontDesk.lastKey.t' noRoomChangeExcept [none, t, t’] noGuestChangeExcept [none, t, t’]
}
19 Nguyễn Thị Minh Tuyền Đặc tả hình thức
Thao tác check-in
pred checkin [g: Guest, r: Room, k: Key, t, t': Time]
v Điều kiện trước:
§ phòng đang ở tình trạng trống § Mã số khóa là mã số tiếp theo của mã số khóa trước đó trong
chuỗi tuần tự các mã số
v Điều kiện sau:
§ Khách hàng giữ mã số khóa và trở thành người ở phòng đó. § Mã số khóa trở thành mã số khóa hiện tại của phòng
v Frame condition:
§ Không có gì thay đổi trừ quan hệ occupant và quan hệ của
khách
20 Nguyễn Thị Minh Tuyền Đặc tả hình thức
Check-in
pred checkin [ g: Guest, r: Room, k: Key, t,t': Time ] {
-- phòng đang ở tình trạng trống no r.occ.t -- khách trở thành người ở phòng đó occ.t' = occ.t + r->g
-- mã số cửa trở thành mã số khóa hiện tại của phòng lk.t' = lk.t ++ r->k -- mã số cửa là mã số khóa tiếp theo của khóa gần nhất -- trong chuỗi mã số khoá của phòng k = nextKey [r.lk.t, r.keys]
-- khách giữ mã số cửa g.keys.t' = g.keys.t + k let occ = FrontDesk.occupant | { } let lk = FrontDesk.lastKey | { } noRoomChangeExcept [none, t, t’] noGuestChangeExcept [g, t, t’]
}
21 Nguyễn Thị Minh Tuyền Đặc tả hình thức
Phát sinh trace
v Bước đầu tiên thỏa mãn điều kiện khởi tạo v Bất cứ một cặp thời gian kế tiếp nhau nào
cũng có mối liên hệ với nhau bởi § thao tác entry § thao tác check-in § thao tác check-out
22 Nguyễn Thị Minh Tuyền Đặc tả hình thức
Phát sinh trace
fact Traces {
init [TO/first] all t: Time - TO/last | let t' = TO/next [t] |
some g: Guest, r: Room, k: Key |
entry [g, r, k, t, t’] or checkin [g, r, k, t, t’] or checkout [g, t, t’]
}
23 Nguyễn Thị Minh Tuyền Đặc tả hình thức
Phân tích
v Các trường hợp không có quyền vào
phòng: § Nếu một khách g vào phòng r tại thời điểm t và thông tin lưu ở lễ tân chỉ ra rằng r đang ở tình trạng trống tại thời điểm đó, thì sau đó g phải được lưu lại với tình trạng là người ở phòng r.
assert noBadEntry {
all t: Time, r: Room, g: Guest, k: Key |
let t' = TO/next [t], o = r.FrontDesk.occupant.t | (entry [g, r, k, t, t’] and some o)
implies g in o
}
24 Nguyễn Thị Minh Tuyền Đặc tả hình thức
Phân tích
check noBadEntry for 3 but 2 Room, 2 Guest, 5 Time v Đủ để kiểm tra vấn đề với 2 guest và 2
room
v Thời gian ít nhất là 5 vì có ít nhất 4 bước thời gian cần thiết để chạy mỗi toán tử một lần.
v Có một phản ví dụ (file hotel1.als)
25 Nguyễn Thị Minh Tuyền Đặc tả hình thức
T0: Trạng thái đầu
v Ban đầu, mã số khóa hiện tại của Room là Key0, mã
số này cũng được lưu ở FontDesk
26 Nguyễn Thị Minh Tuyền Đặc tả hình thức
T1: Thao tác check-in
v Guest1 thực hiện check in phòng Room và nhận mã
số khóa Key1
v Thông tin về người ở phòng đó được cập nhật ở
FrontDesk
v Key1 được lưu lại là mã khóa gần nhất được gán cho
27
Room Nguyễn Thị Minh Tuyền
Đặc tả hình thức
T2: Thao tác check-out
v Guest1 thực hiện check out, và người ở phòng đó bị
xóa đi
28 Nguyễn Thị Minh Tuyền Đặc tả hình thức
T3: Thao tác check-in
v Guest0 thực hiện check in vào Room, và nhận chìa khóa Key2; người ở phòng Room được cập nhật v Key2 được lưu như là mã số khóa gần nhất gán cho
29
Room Nguyễn Thị Minh Tuyền
Đặc tả hình thức
T4: Thao tác enter
v Guest1 đưa khóa Key1 vào mở phòng Room và được
chấp nhận.
30 Nguyễn Thị Minh Tuyền Đặc tả hình thức
Ràng buộc cần thiết
v Không có ràng buộc nào giữa một người khách check in và việc vào phòng.
fact noIntervening {
all t: Time - TO/last |
let t’ = TO/next [t], t’’ = TO/next [t’] | all g: Guest, r: Room, k: Key |
checkin [g, r, k, t, t’] implies ( entry [g, r, k, t’, t’’] or no t" )
}
31 Nguyễn Thị Minh Tuyền Đặc tả hình thức
Phân tích
v Kiểm tra lại một lần nữa:
check noBadEntry for 3 but 2 Room, 2 Guest, 5 Time v Không có phản ví dụ (file hotel2.als) v Để chắc chắn hơn, ta tăng scope lên:
check noBadEntry for 5 but 3 Room, 3 Guest, 9 Time
v Không có phản ví dụ
32 Nguyễn Thị Minh Tuyền Đặc tả hình thức
