Kinh doanh - Marketing
Kinh tế quản lý
Biểu mẫu - Văn bản
Tài chính - Ngân hàng
Công nghệ thông tin
Tiếng anh ngoại ngữ
Kĩ thuật công nghệ
Khoa học tự nhiên
Khoa học xã hội
Văn hóa nghệ thuật
Sức khỏe - Y tế
Văn bản luật
Nông Lâm Ngư
Kỹ năng mềm
Luận văn - Báo cáo
Giải trí - Thư giãn
Tài liệu phổ thông
Văn mẫu
Giới thiệu
Đăng ký
Đăng nhập
Tìm
Danh mục
Kinh doanh - Marketing
Kinh tế quản lý
Biểu mẫu - Văn bản
Tài chính - Ngân hàng
Công nghệ thông tin
Tiếng anh ngoại ngữ
Kĩ thuật công nghệ
Khoa học tự nhiên
Khoa học xã hội
Văn hóa nghệ thuật
Y tế sức khỏe
Văn bản luật
Nông lâm ngư
Kĩ năng mềm
Luận văn - Báo cáo
Giải trí - Thư giãn
Tài liệu phổ thông
Văn mẫu
Thông tin
Điều khoản sử dụng
Quy định bảo mật
Quy chế hoạt động
Chính sách bản quyền
Giới thiệu
Đăng ký
Đăng nhập
0
Trang chủ
Công Nghệ Thông Tin
Kỹ thuật lập trình
Bài giảng Đặc tả hình thức: Chương 8 - Nguyễn Thị Minh Tuyền
Đ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
Hữu Lương
82
33
pdf
Đang chuẩn bị nút TẢI XUỐNG, xin hãy chờ
Tải xuống
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 .
TÀI LIỆU LIÊN QUAN
Bài giảng Đặc tả hình thức: Chương 5 - PGS.TS. Vũ Thanh Nguyên
Bài giảng Đặc tả hình thức: Chương 5 - PGS.TS. Vũ Thanh Nguyên
Bài giảng Đặc tả hình thức: Chương 5 - PGS.TS. Vũ Thanh Nguyên
Bài giảng Đặc tả hình thức: Chương 1 - PGS.TS. Vũ Thanh Nguyên
Bài giảng Đặc tả hình thức: Chương 1 - PGS.TS. Vũ Thanh Nguyên
Bài giảng Đặc tả hình thức: Chương 1 - PGS.TS. Vũ Thanh Nguyên
Bài giảng Đặc tả hình thức: Chương 0 - Nguyễn Thị Minh Tuyền
Bài giảng Đặc tả hình thức: Chương 2 - PGS.TS. Vũ Thanh Nguyên
Bài giảng Đặc tả hình thức: Chương 2 - PGS.TS. Vũ Thanh Nguyên
Bài giảng Đặc tả hình thức: Chương 2 - PGS.TS. Vũ Thanh Nguyên
crossorigin="anonymous">
Đã phát hiện trình chặn quảng cáo AdBlock
Trang web này phụ thuộc vào doanh thu từ số lần hiển thị quảng cáo để tồn tại. Vui lòng tắt trình chặn quảng cáo của bạn hoặc tạm dừng tính năng chặn quảng cáo cho trang web này.