The New Generation of Engineers: Yannick Moy, AdaCore

Yannick Moy is a Senior Engineer at AdaCore, where he works on software source code analyzers CodePeer and SPARK, aiming either at detecting bugs or at verifying safety/security properties. Yannick led the three-year project Hi-Lite, leading to the new version of SPARK known as SPARK 2014, a product he proudly presents in articles, conferences, classes, and blogs (in particular www.spark-2014.org). Yannick previously worked on source code analyzers for PolySpace (now The MathWorks) and at Université Paris-Sud.

 

What got you interested in electronics and the embedded engineering space?

My background is in computer science, more precisely the verification techniques to check that a software program or do not contain errors. I was lucky to have professors who were both passionate about the mathematical techniques they were teaching and enthusiastic about the preliminary uses of these techniques in industry. One such story in particular that impressed me was of the details of the crash of Ariane V during its maiden flight, and how the error that caused the crash had been found a posteriori by a new software analysis tool developed by a young researcher named Alain Deutsch. After I graduated, I joined the startup PolySpace Technologies he had founded to develop this technology.

How have you turned that experience or motivation into a successful career-to-date, and what are the key factors that have enabled success so early on in your career?

When I started working on static analysis of software in 2002, it was mostly a subject of academic research. Few deep analysis tools were available to industrial users. Since then, the supply and demand for tools have kept growing, to the point that it is not uncommon today to see projects using multiple static analysis tools. I was fortunate to be there at the start of the industrial takeoff, and to stay at the frontier between academic research and industrial tool development, which gave me the opportunity to work on multiple tools that are used in industry today: first PolySpace Verifier C++, then the Frama-C platform for C, and finally CodePeer for Ada and the new SPARK toolset for a formally verifiable Ada subset. One key factor for maintaining this essential collaboration with academic research is the openness in development, not only by using free/libre open source licenses, but also by using for example an online forge and an open mailing list, which allows others to follow/patch/discuss your problems and solutions. In our work on SPARK, we have developed in this way strong ties with the research team where I did my PhD. After years of collaboration, we are now starting a joint laboratory called ProofInUse to codevelop the SPARK technology.

Given your area of expertise, what have been the greatest challenges and/or breakthroughs during your time in the industry?

The main challenge remains the cost-effective detection of remaining errors in large and complex software. From time to time, a widely publicized error like Heartbleed reminds all that this issue has not been solved. While the critical software industry is much more secretive about errors, there seems to be enough close calls that project leaders keep looking for better ways to detect errors. As a software developer, I know all too well how easy it is to let subtle errors pass through testing and review. A related challenge is to keep the cost of verification under control. In 2011 a NASA report evaluated the cost of verifying the most critical avionics software to be approximately seven times the cost for less critical systems.

The breakthroughs came from academia, with the first optimizing compiler for C (CompCert) and operating-system kernel (seL4) for which we have a formal proof that the code is correctly implementing the desired behavior. While these achievements are inspiring, the cost of reaching that level of confidence is still very high, when you realize that "only" proving the absence of run-time errors (buffer overflows, division by zero, etc.) is an objective that very few projects achieve. In practice, I think that projects that produce software provably free of these mundane programming errors, at a much lower cost than the above projects, are worth noting, like the IRONSIDES DNS server and Muen , both written in SPARK.

What has been the single most influential trend to come out of your generation of embedded industry professionals? What do you see as the most disruptive trend or technology over the next 5-10 years?

In the last 15 years, code generation from data flow programming languages like Simulink and SCADE has largely replaced programming in C and Ada in the area of control systems. This is a good thing because code generation can prevent some types of programming errors, like the failure to initialize data. But the code generated is also much more complex to analyze in general, full of low-level conversion operations and lacking higher level abstractions like precise types. This is unfortunate, because the generated code is in general linked with manually produced code, and so the safety and security of the resulting executable can only be assessed at the code level.

Regarding the future, I'd like to say that it will be common to produce software that is 100 percent free of run-time errors in 10 years, but that would be more a wish than a prediction. I think that we will see in the future more and more heterogeneity in how the software is produced, with parts of it being generated from modeling or graphical languages like Simulink, UML, AADL. Being able to deal with this heterogeneity will be key to benefit from these technologies, in particular for verification, and static analysis is certainly part of the answer.

What advice would you offer the next generation of engineers?

Each domain of the embedded industry has different constraints, which leads to different technological choices in avionics, automotive, medical, etc. What's interesting today is that you can keep up to date with what's happening in other industries with a minimal effort online, simply by following blogs, journals, webinars, recorded conferences, etc. I find that it's been very profitable in my case.

Topics covered in this article