Bài giảng Đặc tả hình thức: Chương 8 - Nguyễn Thị Minh Tuyền

Số trang: 33 Loại file: pdf Dung lượng: 668.73 KB Lượt xem: 12 Lượt tải: 0

Hoai.2512

Phí tải xuống: 4,000 VND

Xem trước 4 trang đầu tiên của tài liệu này:

Thông tin tài liệu:

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,...
Nội dung trích xuất từ tài liệu:
Bài giảng Đặc tả hình thức: Chương 8 - Nguyễn Thị Minh Tuyền 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 thức