Ten Years of Industrial Experiments with Frama-C at Mitsubishi Electric R&D Centre Europe

Mitsubishi Electric R &D Centre Europe (MERCE), the advanced European research laboratory of Mitsubishi Electric group, has been carrying research activity on Formal Methods for more than 10 years now. MERCE applied various formal methods in its projects and, among them, MERCE conducted several extensive experiments with Frama-C, from safety to security applications, in different industrial domains. Through three of these experiments, namely industrial code verification, automated test generation and verification of an industrial firewall, this chapter gives some feedback on several Frama-C ’s capabilities based on the plug-ins EvaEva , PathCrawlerPathCrawler and WpWp . Demonstrating the tractability of the solutions in industrial context is one of the leading issues when MERCE evaluates tools and methods. Frama-C appears as a mature technology which can be operated in very different contexts from classical testing to full-fledged formal functional verification.