Rapid Prototyping of Embedded Software Using Selective Formalism

Our software synthesis tool, CSP++, generates C++ source code from verifiable CSPm specifications, and includes a framework for runtime execution. Our technique of selective formalism allows the synthesized formal control backbone code to be linked with non-formal usercoded C++ functions that carry out I/O and data processing. 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 (system on programmable chip) by targeting the CSP++ execution framework to an FPGA processor core. This is demonstrated with a new point-of-sale case study.

• Type: Conference
• Year: 2005
• Where: RSP
• Authors: John D. Carter, Ming Xu, William B. Gardner
• Keywords: Formal Control Backbone, Non-formal Usercoded C++, Rapid Prototyping, Rapid System Prototyping, RSP 2005