Đang chuẩn bị liên kết để tải về tài liệu:
Bài giảng Đặc tả hình thức: Chương 8 - Nguyễn Thị Minh Tuyền

Bài giảng Đặc tả hình thức: Chương 8 giúp người học hiểu về "Mô hình minh họa: Hotel Room Locking". Nội dung trình bày cụ thể gồm có: Mô tả vấn đề, signatures và fields, biểu đồ mô hình cho hệ thống, bàng buộc và thao tác, phát sinh khóa mới, trạng thái khởi tạo,. | 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 Nguyễn Thị Minh Tuyền 2 Đặ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. Nguyễn Thị Minh Tuyền 3 Đặ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. Nguyễn Thị Minh Tuyền 4 Đặ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. Nguyễn Thị Minh Tuyền 5 Đặc tả hình .