Rapid Prototyping of Embedded Software Using Selective Formalism

Our software synthesis tool, CSP++, generates C++ source code from verifiable CSPm specifications, and in-cludes a framework for runtime execution. Our technique of selective formalism allows the synthesized formal con-trol backbone code to be linked with non-formal user-coded C++ functions that carry out I/O and data pro-cessing. This tool already facilitates rapid prototyping of formally-specified software by bypassing the customary manual translation from a formal notation. In this work, we extend the rapid prototyping capability to SOPC (sys-tem on programmable chip) by targeting the CSP++ execu-tion framework to an FPGA processor core. This is demon-strated with a new point-of-sale case study. 1