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
References in zbMATH (referenced in 1 article )
Showing result 1 of 1.
- Khaled, Mahmoud; Zamani, Majid: \textsfpFaces: an acceleration ecosystem for symbolic control (2019)