Automated Synthesis of Networked Control Systems
Final Report Abstract
Networked control systems (NCSs) are feedback control systems in which the communication between sensors, controllers, and actuators is supported by a shared communication channel that is subject to numerous non-idealities including: variable communication delays, variable sampling/transmission intervals, quantization errors, packet losses, limited bandwidth, and other communication constraints. NCSs have received significant attention within the scientific and industrial communities in the past two decades because of their high architectural flexibility and low installation and maintenance costs. For example, automotive architectures in high-end cars today consist of almost 100 electronic control units (ECUs) connected by a variety of communication channels like CAN, FlexRay, and Ethernet. Given such a distributed and heterogeneous architecture, the non-idealities caused by the communication channels can result in a significant deviation in control performance in such applications. This research project aimed to develop an innovative design process, in which the embedded control software for plants in NCSs is synthesized from high-level correctness requirements in a push-button and formal manner. Requirements for modern NCS applications go beyond conventional properties in control theory (e.g. stability) and include temporal logic specifications such as properties expressed as linear temporal logic (LTL) formulae or as automata on infinite strings. In particular, we investigated correct-by-construction controller synthesis of temporal logic specifications for NCSs by constructively deriving symbolic abstractions of NCSs, while considering the network non-idealities simultaneously. Finally, we provided a front-end toolbox taking a model of the plant, described by an ordinary differential (or difference) equation, or its corresponding symbolic model, the network properties, and a logic specification as inputs and providing automatically a provably correct controller as executable C/C++ code as an output enforcing the given specification on the plant in the NCS. In addition, we provided an interface between our toolbox and Matlab for realistic simulations of the plants and the network imperfections.
Publications
-
Finite abstractions of networked control systems. 53rd IEEE Conference on Decision and Control, 95-100.
Zamani, Majid; Mazo, Manuel & Abate, Alessandro
-
Symbolic models of networked control systems: A feedback refinement relation approach. 2016 54th Annual Allerton Conference on Communication, Control, and Computing (Allerton), 187-193.
Khaled, Mahmoud; Rungger, Matthias & Zamani, Majid
-
SENSE: Abstraction-Based Synthesis of Networked Control Systems. Electronic Proceedings in Theoretical Computer Science, 272, 65-78.
Khaled, Mahmoud; Rungger, Matthias & Zamani, Majid
-
Symbolic Abstractions of Networked Control Systems. IEEE Transactions on Control of Network Systems, 5(4), 1622-1634.
Zamani, Majid; Mazo, Manuel; Khaled, Mahmoud & Abate, Alessandro
-
Cloud-Ready Acceleration of Formal Method Techniques for Cyber–Physical Systems. IEEE Design & Test, 38(5), 25-34.
Khaled, Mahmoud & Zamani, Majid
-
A Framework for Output-Feedback Symbolic Control. IEEE Transactions on Automatic Control, 68(9), 5600-5607.
Khaled, Mahmoud; Zhang, Kuize & Zamani, Majid
