Kiểm chứng tính đúng đắn hệ thống tính toán của chương trình bằng kiểm duyệt mô hình

Tóm tắt Kiểm chứng tính đúng đắn hệ thống tính toán của chương trình bằng kiểm duyệt mô hình: ...ình Promela [1]:  Các khai báo kiểu và khai báo biến;  Khai báo tiến trình;  Tiến trình init. 2.1.2. Biến Cũng như hầu hết các ngôn ngữ lập trình có cấu trúc, Promela yêu cầu các biến phải được khai báo trước khi chúng được sử dụng. Khai báo biến trong Promela giống trong ngôn ngữ lập...c trạng thái của chương trình, sau đó in ra các trạng thái của thuộc tính. Một trạng thái của chương trình là bộ các giá trị của các biến, biến đếm vị trí các tiến trình. Một tính toán của chương trình là chuỗi các trạng thái bắt đầu bởi trạng thái khởi tạo và tiếp tục với những trạng thái x...động, báo cháy mức trừu tƣợng 3.2.1. Mô tả hệ thống mức trừu tƣợng Hệ thống báo động bao gồm các Sensors để phát hiện động (từ môi trường), bảng điều khiển Control Panel, và chuông báo Alarm. Khi các Sensors nhận được thông báo có động từ môi trường gửi tới, nó sẽ gửi thông báo này cho bảng ...