Communicating FSM partitioning for front end embedded software synthesis

Nowadays embedded software is facing more and more pressure of time to market (TTM). In order to shorten the development cycle and improve the quality of development, formal method has been widely used in embedded software development process. Usually formal method is applied as a specification method to clearly define and design systems, but recently automatic implementation has attracted intensive interests. Although there are some available commercial tools for formal method based embedded software synthesis, the generated code is acceptable for only prototyping because of its poor quality. Optimized embedded software synthesis is the key to bring out the maximal potential of formal method based embedded software development. The optimal partitioning of formal specification is a significant step in front-end embedded software synthesis, because improper partitioning incur both code explosion and poor performance. Our work is based on communicating FSM (CFSM), because CFSM is the basis of many development methods and tools, and the goal is to achieve the best performance under the constraints of code size. We formulated the partitioning problem taking into account profiling information. In order to search the tremendous solution space efficiently, genetic algorithm is applied.