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