SENSE: Abstraction-Based Synthesis of Networked Control Systems
SENSE is an open-source framework for the symbolic abstraction and controller synthesis for networked control systems (NCS). It is implemented in C++ comes with MATLAB and OMNet++ interfaces to access the synthesized controller as well as to simulate the closed-loop NCS. SENSE has many helper tools to facilitate the analysis of the resulting symbolic models and controllers. One particular tool allows for the automatic code generation of the resulting symbolic controllers.
The framework is intended to be used and extended by researches in the area of formal synthesis of NCS. It requires that the user already have symbolic abstractions of the plant (controlled system) in NCS. Users can easily use the library SCOTS inside SENSE to construct such abstractions before using the engines of SENSE.
SENSE provides an extinsible framework for describing NCS while facilitating the procedure for abstracting such systems and synthesizing controllers for them. The implementation is mainly based on binary decision diagrams (BDD). The user provides the plant's symbolic abstraction as a BDD object. Based on the selection of the network configuration, the user provides the parameters of the communication channels. The tool provides algorithms to expand the original transition relation of the plant to a transition relation that takes into account the non-idealities of the communication channels.
SENSE can handle the construction of symbolic models and the synthesis of their controllers for any class of NCS. However, in order to refine the controllers and apply them to the original NCS, the current theory requires that the upper and lower bounds of the delays to be equal at each channel. Therefore, SENSE is currently available with only this class of NCS. Nevertheless, due to the modular design of SENSE, it is straightforward to define extra classes of NCS, e.g. taking time-varying delays into account, once the theory behind them is available.
SENSE implements operations over BDDs to expand the provided abstraction. The expanded abstraction can be then used for the process of controller synthesis. Controller synthesis is done using fixed-point operations over the expanded BDD objects. SENSE natively supports safety, reachability, persistence, and recurrence specifications given as LTL formulae.
SENSE was designed while considering the following requirements for a NCS:
- possibility to extend to different classes of NCS.
- possibility to extend targeted specifications for controller synthesis
- support for network simulations with OMNet++ for more reliable closed loop simulations
SENSE also provides the following helper tools that help analyzing the symbolic models as well as the synthesized controllers:
- bdd2implement: a tool to automatically generate C/C++ or VHDL/Verilog codes from the synthesized BDD-based controllers;
- bdd2fsm: a tool to generate files following the FSM data format or the comma-separated format of the transition relation of symbolic models. Such representation is used by many software packages to visualize graphs.
- bddDump: a tool to extract the meta-data information stored inside the generated BDD files.
- contCoverage: a tool to provide fast terminal-based ASCII-art visualization of the coverage of the synthesized controllers.
- sysExplorer: a tool to help testing the expanded transition relation or the synthesized controllers.
For more information about the structure and usage of SENSE, and also the manual, please visit the documentation section.
M. Khaled, M. Rungger, and M. Zamani. SENSE: Abstraction-Based Synthesis of Networked Control Systems. 1st International Workshop on Methods and Tools for Rigorous System Design (MeTRiD 2018), April 2018. (Preprint).
Please go to the download page.