« BACK TO PROGRAM

Industrial use of Formal Methods: a feedback from various experiments with Frama-C

David Mentré - Mitsubishi Electric R&D Centre Europe (MERCE)

Mitsubishi Electric is a worldwide group developing a wide range of business to business solutions, from railway systems to satellites, from electric sub-stations to automotive equipment. Most of those solutions need to build safety and security at their core. Therefore Mitsubishi Electric, like all similar industrial groups, is struggling to keep or improve the quality of its products while reducing costs and time-to-market. Formal Methods is more and more perceived as a viable approach to reach this objective, but applying Formal Methods is not an easy journey. In this presentation, we will show some of the needs appearing in domains like railway or automotive, and how we can address those needs using Frama-C and its plug-ins like Value Analysis, WP or PathCrawler, both in the short term and in the long term, giving along the way our feedback on those experiments.

About David Mentré

David Mentré is Research Manager in Communication & Information Systems department of Mitsubishi Electric R&D Centre Europe. He received an Engineering degree from IMT Atlantique engineering school in 1996 and a Ph.D. from INRIA Rennes and Rennes 1 University in 2001. After a post-doctorate at INRIA Paris, he joined Mitsubishi Electric R&D Centre Europe in 2001 as Research Engineer. Since 2001, he worked on various subjects related to the telecommunication and computer science fields including deep packet inspection, IP protocol analysis, Quality of Service, security, LTE 3GPP protocol stack, etc. Since 2009, he is focusing his research on Formal Methods as a way to ensure 100% correctness of crucial properties in safety critical systems (in railway, factory automation, automotive...) at a lower cost. He and his colleagues use extensively Frama-C and its various plug-ins to answer industrial needs in formal verification.