Giáo trình Đặc tả hình thức - Chương 8: Mô hình minh họa-Hotel Room Locking - Nguyễn Thị Minh Tuyền

Nội dung text: Giáo trình Đặc tả hình thức - Chương 8: Mô hình minh họa-Hotel Room Locking - Nguyễn Thị Minh Tuyền

1. 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
2. Hotel Room Locking Nguyễn Thị Minh Tuyền 2 Đặc tả hình thức
3. 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. Nguyễn Thị Minh Tuyền 3 Đặc tả hình thức
4. 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. Nguyễn Thị Minh Tuyền 4 Đặc tả hình thức
5. 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. Nguyễn Thị Minh Tuyền 5 Đặc tả hình thức
6. 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. Nguyễn Thị Minh Tuyền 6 Đặc tả hình thức
7. 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 } Nguyễn Thị Minh Tuyền 7 Đặc tả hình thức
8. 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 } Nguyễn Thị Minh Tuyền 8 Đặc tả hình thức
9. Biểu đồ mô hình cho hệ thống currentKey. ! ? keys Room Key .lastKey. ? keys. .occupant. Guest Nguyễn Thị Minh Tuyền 9 Đặc tả hình thức
10. 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 Nguyễn Thị Minh Tuyền 10 Đặc tả hình thức
11. 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 } Nguyễn Thị Minh Tuyền 11 Đặc tả hình thức
12. 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] } Nguyễn Thị Minh Tuyền 12 Đặc tả hình thức
13. 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 } Nguyễn Thị Minh Tuyền 13 Đặc tả hình thức
14. 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 } Nguyễn Thị Minh Tuyền 14 Đặc tả hình thức
15. 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. Nguyễn Thị Minh Tuyền 15 Đặc tả hình thức
16. 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' } Nguyễn Thị Minh Tuyền 16 Đặc tả hình thức
17. 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’] } Nguyễn Thị Minh Tuyền 17 Đặc tả hình thức
18. 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 Nguyễn Thị Minh Tuyền 18 Đặc tả hình thức
19. 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’] } Nguyễn Thị Minh Tuyền 19 Đặc tả hình thức
20. 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 Nguyễn Thị Minh Tuyền 20 Đặc tả hình thức
21. 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’] } Nguyễn Thị Minh Tuyền 21 Đặc tả hình thức
22. 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 Nguyễn Thị Minh Tuyền 22 Đặc tả hình thức
23. 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’] } Nguyễn Thị Minh Tuyền 23 Đặc tả hình thức
24. 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 } Nguyễn Thị Minh Tuyền 24 Đặc tả hình thức
25. 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) Nguyễn Thị Minh Tuyền 25 Đặc tả hình thức
26. 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 Nguyễn Thị Minh Tuyền 26 Đặc tả hình thức
27. 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 Room Nguyễn Thị Minh Tuyền 27 Đặc tả hình thức
28. T2: Thao tác check-out v Guest1 thực hiện check out, và người ở phòng đó bị xóa đi Nguyễn Thị Minh Tuyền 28 Đặc tả hình thức
29. 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 Room Nguyễn Thị Minh Tuyền 29 Đặc tả hình thức
30. T4: Thao tác enter v Guest1 đưa khóa Key1 vào mở phòng Room và được chấp nhận. Nguyễn Thị Minh Tuyền 30 Đặc tả hình thức
31. 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" ) } Nguyễn Thị Minh Tuyền 31 Đặc tả hình thức
32. 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ụ Nguyễn Thị Minh Tuyền 32 Đặc tả hình thức