Mô Hình Hình Thức Dựa Trên Thành Phần Cho Các Hệ Thống PLC

Xác thực chức năng là một nhiệm vụ quan trọng trong các hệ thống nhúng phức tạp. Việc mô hình hóa chính thức hệ thống PLC để xác minh là một nhiệm vụ khó khăn. Mô hình xác minh tốt cần phải trung thực và súc tích. Một mặt, mô hình phải nhất quán với hệ thống, mặt khác, mô hình phải có quy mô phù hợp do vấn đề bùng nổ trạng thái trong quá trình xác minh. Bài báo này đề xuất một phương pháp hệ thống cho việc xây dựng mô hình xác minh. Kiến trúc hệ thống PLC và các đặc điểm của PLC được mô hình hóa dưới dạng các thành phần. Điều này có tính chất phổ quát cho tất cả các ứng dụng PLC. Chúng tôi cung cấp một phương pháp dịch tự động cho mô hình hóa phần mềm dựa trên ngữ nghĩa hoạt động. Một ví dụ nhỏ được trình bày để minh họa phương pháp của chúng tôi.