General information about the structure of SENSE is presented here. However, we suggest referring to the manual for further details. The C++ part of SENSE provides the algorithms to compute the symbolic model of Networked Control Systems (NCS) and to synthesize controllers based on the computed model.

The input is supposed to be a BDD that represnts the transition relation of the plant within the NCS. Such BDD can be generated by constructing a symbolic model using the library SCOTS inside SENSE. Then the file should be safed in a file. The tool should then be provided with details about the NCS itself.

The output is a BDD that represents the transition relation of the NCS. Users can further continue and synthesize symbolic controllers for the NCS. We provide fixed-point operations to synthesize controllers that enforce any of the following specifications: 

• Reachabilitly
• Safety
• Persistence
• Recurrence

The tool contains a Matlab interface to simulate the generated controller in the closed loop system and to visualize the abstract state space together with the atomic propositions. The tool allows for generating C/C++ or VHDL/Verilog codes to cover hardware and software implementations of the synthesized controllers. The figure to the right presents the internal structure and the work flow inside SENSE.