Automated Translation of C/C++ Models into a Synchronous Formalism

For complex systems that are reusing intellectual property components, functional and compositional design correctness are an important part of the design process. Common system level capture in software programming languages such as C/C++ allow for a comfortable design entry and simulation, but mere simulation is not enough to ensure proper design integration. Validating that reused components are properly connected to each other and function correctly has become a major issue for such designs and requires the use of formal methods. In this paper, we propose an approach in which we automatically translate C/C++ programs into the synchronous formalism SIGNAL, hence enabling the application of formal methods without having to deal with the complex and error prone task to build formal models by hand. The main benefit of considering the model of SIGNAL for C/C++ languages lies in the formal nature of the synchronous language SIGNAL, which supports verification and optimization techniqu...

• Type: Conference
• Year: 2006
• Where: ECBS
• Authors: Hamoudi Kalla, Jean-Pierre Talpin, David Berner, Loïc Besnard
• Keywords: C/C++, ECBS 2006, Formal Methods, Hardware, Translate C/c++ Programs