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

LOGO<br /> <br /> Đặc tả hình thức<br /> Mô hình minh họa:<br /> Hotel Room Locking<br /> <br /> Nguyễn Thị Minh Tuyền<br /> <br /> Nguyễn Thị Minh Tuyền<br /> <br /> 1<br /> <br /> Hotel Room Locking<br /> <br /> Nguyễn Thị Minh Tuyền<br /> <br /> 2<br /> <br /> Đặc tả hình thức<br /> <br /> Vấn đề đặt ra<br /> v Mô hình hóa bằng Alloy hệ thống khóa<br /> cửa sử dụng thẻ từ để đóng mở cửa<br /> phòng khách sạn.<br /> §  Khi đã tạo thẻ mới cho một phòng thì khách trước đó<br /> không thể vào phòng bằng thẻ cũ được.<br /> <br /> v Mô hình hóa cả khía cạnh tĩnh và<br /> động của hệ thống.<br /> <br /> Nguyễn Thị Minh Tuyền<br /> <br /> 3<br /> <br /> Đặc tả hình thức<br /> <br /> Mô tả vấn đề<br /> v Khách sạn sử dụng một mã số khóa mới cho<br /> khách hàng tiếp theo<br /> §  Thiết lập lại mã khóa mới để đảm bảo mã số khóa được lưu<br /> trên thẻ trước đó không hoạt động nữa.<br /> §  Bộ khóa là một đơn vị độc lập, đơn giản (sử dụng pin) với một<br /> bộ nhớ lưu giữ mã số hiện tại.<br /> <br /> v Thiết bị phần cứng phát sinh một chuỗi các<br /> số ngẫu nhiên.<br /> v Bộ khóa chỉ mở được hoặc bằng mã số khóa<br /> hiện tại hoặc mã số khóa tiếp theo của nó.<br /> §  Nếu một mã số khóa tiếp theo được thiết lập,<br /> •  mã số khóa tiếp theo đó trở thành mã số khóa hiện tại và<br /> •  mã số khóa trước đó sẽ không được chấp nhận nữa.<br /> <br /> Nguyễn Thị Minh Tuyền<br /> <br /> 4<br /> <br /> Đặc tả hình thức<br /> <br /> v Không yêu cầu giao tiếp giữa lễ tân và<br /> khóa cửa.<br /> v Bằng cách<br /> §  đồng bộ hóa giữa lễ tân và khóa cửa được khởi tạo<br /> lần đầu, và<br /> §  sử dụng cùng bộ phát sinh mã số ngẫu nhiên,<br /> §  => lễ tân có thể lưu giữ thông tin của mã khóa hiện<br /> tại với cửa.<br /> <br /> Nguyễn Thị Minh Tuyền<br /> <br /> 5<br /> <br /> Đặc tả hình thức<br /> <br />