This paper outlines the application of the HiLeS-RCP (High Level Specification of Embedded Systems - Rich Client Platform) to model and design controllers of interleaved boost converters using the Systems Modelling Language (SysML). HiLeS-RCP allows the transformation from SysML models to Petri nets for implementation in embedded hardware. As a result, these models based on SysML can be used in Hardware-in-the-Loop (HIL) applications. In addition, the formal transformation from SysML to Petri nets is intended for structural analysis of the designed controllers in order to avoid undesired behaviours after implementation. As a case of study, HiLeS-RCP is used to model and design a supervisory controller for interleaved boost converters. This supervisory controller is implemented in FPGA; furthermore, embedded real time tools are used to evaluate the supervisory controller performance. Finally, experimental results show that the proposed methodology based on SysML and Petri nets is suitable to design controllers for interleaved boost converters.