Bài giảng Đặc tả hình thức - Chương 8: 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 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