Trong những thập kỷ gần đây, mô hình sự kiện rời rạc đã được sử dụng rộng rãi để giải quyết các vấn đề kỹ thuật điều khiển. So với mô hình hệ thống động truyền thống, nơi hành vi vật lý được mô tả rõ ràng, mô hình sự kiện rời rạc tập trung vào mức độ trừu tượng hơn, nơi hành vi logic được quan tâm. Trong luận văn này, chúng tôi tập trung vào việc kiểm chứng hình thức hành vi vòng kín logic của hệ thống điều khiển. Để đáp ứng các yêu cầu về an toàn và/hoặc khả năng hoạt động theo các thông số kỹ thuật đã cho, chúng tôi khai thác ngữ nghĩa hình thức của các chương trình điều khiển để biểu diễn toàn bộ hành vi vòng kín trong một mô hình sự kiện rời rạc, từ đó các thuộc tính cần quan tâm có thể được kiểm chứng hình thức thông qua một phương pháp hiệu quả.

Abstract:

In recent decades, discrete-event modelling has been widely utilised to address control engineering problems. Comparing with conventional dynamic system modelling where physical behaviour is explicitly to describe, discrete-event modelling focuses on a more abstract level where logical behaviour is of interest. In this dissertation, we focus on the formal verification of the logical closedloop behaviour of control systems. To satisfy safety and/or liveness requirements according to given technical specifications, we exploit the formal semantics of control programmes to represent the entire closed-loop behaviour in a discrete-event model, from which the properties of interest can be formally verified through an efficient method.

Ngôn ngữ:	eng
Tác giả:	Tang, Yiheng
Thông tin nhan đề:	Formal Verification in Automated Manufacturing
Nhà xuất bản:	FAU University Press
Loại hình:	Tài nguyên giáo dục mở / Bộ sưu tập: Kỹ thuật điều khiển - Tự động hóa
Bản quyền:	https://creativecommons.org/licenses/by/4.0/
Nguồn gốc:	https://directory.doabooks.org/handle/20.500.12854/170230
Mô tả vật lý:	187tr
Năm xuất bản:	2024