Tài liệu Đặc tả hình thức - Mô hình minh họa: Hotel Room Locking - Nguyễn Thị Minh Tuyền: LOGO
Đặc tả hình thức
Nguyễn Thị Minh Tuyền
Mô hình minh họa:
Hotel Room Locking
Nguyễn Thị Minh Tuyền 1
Đặc tả hình thức
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 ...
33 trang |
Chia sẻ: putihuynh11 | Lượt xem: 526 | Lượt tải: 0
Bạn đang xem trước 20 trang mẫu tài liệu Đặc tả hình thức - Mô hình minh họa: Hotel Room Locking - Nguyễn Thị Minh Tuyền, để tải tài liệu gốc về máy bạn click vào nút DOWNLOAD ở trên
LOGO
Đặc tả hình thức
Nguyễn Thị Minh Tuyền
Mô hình minh họa:
Hotel Room Locking
Nguyễn Thị Minh Tuyền 1
Đặc tả hình thức
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
}
-- FrontDesk gồm hai quan hệ:
-- 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 đó
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
9 Nguyễn Thị Minh Tuyền
Room Key
Guest
currentKey.!
? keys
.lastKey.?
.occupant.
keys.
Đặ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 ] {
-- 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
(k = ck.t and ck.t' = ck.t)
-- khách hàng mới
or (k = nextKey [ck.t, r.keys] and ck.t' = k)
-- 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 ]{
let occ = FrontDesk.occupant | {
-- 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)
}
-- 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 ] {
-- khách giữ mã số cửa
g.keys.t' = g.keys.t + k
let occ = FrontDesk.occupant | {
-- 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
}
let lk = FrontDesk.lastKey | {
-- 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]
}
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
26 Nguyễn Thị Minh Tuyền
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
Đặc tả hình thức
T1: Thao tác check-in
27 Nguyễn Thị Minh Tuyền
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
Room
Đặc tả hình thức
T2: Thao tác check-out
28 Nguyễn Thị Minh Tuyền
v Guest1 thực hiện check out, và người ở phòng đó bị
xóa đi
Đặc tả hình thức
T3: Thao tác check-in
29 Nguyễn Thị Minh Tuyền
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
Room
Đặc tả hình thức
T4: Thao tác enter
30 Nguyễn Thị Minh Tuyền
v Guest1 đưa khóa Key1 vào mở phòng Room và được
chấp nhậ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
LOGO
Các file đính kèm theo tài liệu này:
- dac_ta_hinh_thuc_08_alloy_case_study_3046_1994199.pdf