SENSE: Abstraction and Symbolic Controller Synthesis for Networked Control Systems

OMNet++ simulation of a networked-vehicle controller synthesized using SENSE. Here, we demonstrate the reach-avoid specification. The remotely controlled vehicle need to reach the target while avoiding the obstacle.

SENSE is an open source toolbox for the symbolic abstraction and controller synthesis for networked control systems (NCS). The tool is implemented in C++ comes with MATLAB and OMNet++ interfaces to access the synthesized controller as well as to simulate the closed loop NCS.

The tool is intended to be used and extended by researches in the area of formal methods for cyber physical systems. The tool assumes that the user ready has a symbolic abstraction of the plant (controlled system) within the network. Users can easly use the SCOTS tool to construct such abstractions before using the SENSE toolbox. It is able to use such provided abstraction along with a description of the network parameters to construct an expanded abstraction that combines the plant and the network information into single symbolic abstraction.

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 (files generated from SCOTS tool are accepted as input). 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.

OMNet++ simulation of a networked-robot controller synthesized using SENSE. Here, we demonstrate the infinitely-often specification. The remotely controlled robot need to keep revisiting two targets while avoiding the obstacle Network packet visualization is turned-off for this example to increase simulation speed.

SENSE implements direct 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. The tool currently provides supports for NCS with packets are assumed to suffer from fixed delays (i.e. FIFO communication channels), however it was designed allowing for extensions to further NCS classes.  SENSE supports controller synthesis for the specifications of reachability and safety. 

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

Download SENSE

Please go to the download page.