tailieunhanh - 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 .

• Kỹ thuật lập trình
• Bài giảng Đặc tả hình thức
• Đặc tả hình thức
• Mô hình minh họa
• Hotel Room Locking
• Mô hình hóa bằng Alloy
• Phát sinh khóa mới
• Đặc tả hàm
• Đặc tả đệ quy
• Đặc tả hàm tường minh
• Đặc tả hàm không tường minh
• Lập trình phần mềm
• Công nghệ phần mềm
• Đặc tả phần mềm
• Ngôn ngữ đặc tả hình thức
• Đặc tả yêu cầu phần mềm
• Bài giảng Đặc tả yêu cầu phần mềm
• Công nghệ phần mềm nâng cao
• Phân loại đặc tả yêu cầu phần mềm
• Đặc tả phi hình thức phần mềm
• Đặc tả hình thức phần mềm
• Mô hình Thế giới thực
• Quy trình công nghệ phần mềm
• Ngôn ngữ hình thức
• Thiết kế ở mức cao
• Đặc tả ở mức mã nguồn
• JML nâng cao
• Từ khóa chính trong JML
• Các tính năng nâng cao
• Đặc tả các ngoại lệ
• Thừa kế đặc tả
• Các trường model
• Đặc tả không hình thức
• Phép toán vị từ
• Cơ sở đặc tả hình thức
• Luật suy diễn
• Cơ sở toán học trong đặc tả hình thức
• Hệ thống phần mềm
• Lỗi phần mềm
• Ngôn ngữ và hệ thống
• Các ngôn ngữ đặc tả
• Kiểm tra mô hình
• Mô hình hóa dữ liệu
• Kiểu dữ liệu
• Đặc tả operation
• Dữ liệu kiểu mảng
• Kiểu đối tượng phức
• Kiểu tập hợp
• Design by contract
• Ngôn ngữ đặc tả
• Công cụ hỗ trợ
• Giới thiệu về ESC Java2
• Cách sử dụng và thuộc tính
• Cấu trúc của ESC
• Các file đặc tả
• Thủ thuật và cạm bẫy
• Đặc tả thừa kế
• Đặc tả sử dụng ánh xạ
• Kiểu ánh xạ
• Ngôn ngữ đặc tả Z
• Phép toán trên giản đồ