BDD2Implement

BDD2Implement: A Code Generation Tool for Symbolic Controllers. BDD2Implement is a C++ tool to generate hardware/software implementations of BDD-based symbolic controllers. Having the tools SCOTS and SENSE that generate BDD-based sysbolic controllers of (networked) general nonlinear dynamical systems, BDD2Implement completes missing ring in the automatic synthesis technique. BDD2Implement accepts static or dynamic determinized symbolic controllers in the form of BDD-files. The BDD files encodes the controller dynamics as boolean functions. If the provided controller is not determinized, BDD2Implement provides a determinization of the controller. Due to the technquie used in BDD2Implement, the generated implementations are formal. This guarantees the generated codes are exactly achieveing the behaviour in the provided controllers. Consequently, the whole development cycle SCOTS/SENSE/BDD2Implement is now formal. Theoritically (i.e. not implemented in the tool), the generated codes can be converted back to their exact controllers which implies their formality.

Keywords for this software

Anything in here will be replaced on browsers that support the canvas element


References in zbMATH (referenced in 1 article )

Showing result 1 of 1.
Sorted by year (citations)

  1. Khaled, Mahmoud; Zamani, Majid: \textsfpFaces: an acceleration ecosystem for symbolic control (2019)