Ensuring Software Safety in the Automotive Industry

AdaCore, a pioneer of th e Open Source movement, has been associated with the Ada programming language from the beginning. In this edition of Expert Insights, AdaCore’s chief product and revenue officer, Quentin Ochem, talks about ways to ensure software safety in the automotive industry and how the Spark programming language, which evolved from Ada, is well-suited to meet international standards. He talks about the value of international standards like ISO 26262 in preventing recalls and the differences between static analysis and formal methods in finding possible software errors. For best practices, software needs to have been designed with this idea of safety, of reliability, of formalism in mind.

Transcript

00:00:01 Hello and welcome to expert insight. Today we are speaking with Quentyn Oshim, chief product and revenue officer for Adore about ensuring software safety in the automotive industry. And we're going to get right into the technical details. Quentyn, what can you tell me about these recalls that are going on? There were over two million vehicle recalls in the US last year in part

00:00:22 because vehicles have become so complex. Um, can you briefly explain ISO 26262? the one subject we want to talk about today and why international standards like that one and others can help OEMs avoid recalls. So you have to realize the amount of software that is in the car nowadays and the amount of things that this software is doing. I mean to to a large extent cars are more complex

00:00:45 than than planes from a from a software standpoint right you have hidden software that is managing all of the uh function of the car the so-called assistance driving. So, you know, when you drive and your car knows when to slow down or maybe to stop, assist you when you turn or complains when you're passing a lane without uh putting your blinker on. All of these things. There's

00:01:09 massive amount of software. This this is just like the the tip of the iceberg. We're talking million lines of code that are intertwined and interconnected sometimes even with exposure on the outside which open them to cyber security threats. So it's extremely easy to make little mistakes uh in those million lines of code and little mistakes can have very very significant

00:01:34 uh consequences. There's a a very famous case that dates for maybe 15 years ago which was a Toyota system that was accelerating the vehicle without uh the intention of the driver and that that resulted in in accidents. So that's an extreme case, but you can have an array of things and and typically when errors on software are detected, then they lead to updates. But of course,

00:02:00 your car is not like your Windows machine, right? If you need an update, you don't want that update to happen while you're driving or when you don't know about it. So uh that needs to be done in the context of a recall where the manufacturer will do an actual patch on your vehicle. And this is of course very very expensive and this is additive to all of the other reasons why you

00:02:23 might have recall for example mechanical reasons and so on so forth. Uh it is not a new issue. The the the software industry at large has had to face those issues in other places in the past. I was talking about avionics. uh this is something that uh has been looked at since the 1890s and the one way to mitigate those issue is uh so-called safety certification processes. So for

00:02:52 automotive we talk about the ISO 26262 and what the ISO does is that it describes four categories of software if you will depending on how impactful a failure could be. And it describes what you should do to minimize uh the risk of error to minimize the the the possibility of a software mistake that would find its way to production uh and then uh you know cause a potential

00:03:27 harm with the other thing that you need to consider is that the the industry is highly fragmented. So you have a lot of manufacturers and they have that their tier ones and tier two and so on so forth which provide components. So you need some way to homogenize this entire environment. Right? If I'm Toyota, how do I make sure that who is providing my steering wheel is providing

00:03:49 that steering wheel with software that I can trust? And the ISO 26262 is the answer that the industry has adopted. Well, yeah, that's exactly a topic I wanted to get to. Right now OEMs like Toyota, like whoever, you know, they interact with suppliers and have had require them to adhere to these various standards. What is the best way for the OEMs to discuss these

00:04:10 requirements with their suppliers and sort of get them on board with needing to, like you said, make sure the steering wheel is going to do exactly what it should? So, there's two aspects, right? Uh, one aspect is the requirements and, you know, there's no magic there. You need to have providers that uh need to be very precise in what do they expect? uh you know what is the

00:04:30 anticipated behavior and so on so forth but then once you establish that how do you ensure that it has been properly implemented and that's where you sort of the have the magic answer of the the safety standard the ISO standard say that shall respect the standard and then you are going to use independent assessors to verify that the standard has been respected this is the work of

00:04:54 two suit for example which is one of the few assessors that are trusted into doing that that doesn't provide all the answers that you want. I mean as the integrator you will still need to integrate verify things in context of the vehicle and so on so forth but that does raise significantly the trust that you have in the software and the system that is being delivered to you. You kind

00:05:16 of hinted at it there a little bit, but some of these uh complex systems, one of the solutions, one of the possible solutions to get everyone talking on the same page is better formal verification of this software. Um especially when it comes to the overarching frameworks that are involved here. Uh can you talk about that a little bit? How developers can use these verification systems to

00:05:37 increase the reliability and security of their systems? Yes, absolutely. So if you step back of course when you look at the ISO 26262 a big part of it is verification and you have the traditional methods of verification that combines a lot of testing uh and then what we call static analysis which is about looking at the code and trying to find possible errors.

00:06:01 But there's another way uh that you can go about for this thing which is as you just mentioned formal methods right and the idea behind formal methods is that you're going to describe properties on the software. You cannot unfortunately describe everything but there's a number of thing that you can describe and you're going to have a mathematical method to demonstrate that this property

00:06:23 holds within the entire application. So if I gave you a simple example, you may say something like this going to be bit technical but you might have heard of this buffer overflow which is a very common issue in normally to mitigate the odds of a buffer overflow you would use a combination of testing static analysis fuzzing and so on so forth. But with formal methods you can describe that

00:06:47 property very easily. my software should not have buffer overflow and then you're going to have a mathematical demonstration that in all possible cases no buffer overflow can possibly happen. Uh and that's a very simple property. You can describe more complex properties. You can define part of your requirements in terms of formal methods for analysis. Now I want to contrast uh

00:07:10 what it means uh to look at these requirement properties from the traditional angle and the formal method angles. You use traditional methodologies, you will always be able to demonstrate that for a number of cases, those that you could look at your software is okay. But you cannot say this error is not possible at all. Whilst when you use formal method, uh

00:07:32 it's kind of a bulletproof demonstration if you will. This class of problem does not exist. When you talk about different coding languages and things to sort of get into these solutions, do any of them stand up? I mean, I feel like I've heard Spark mentioned as a as a coding language that's particularly well suited Yeah, that's a that's an interesting question. It's in order to achieve that,

00:07:52 you need a formalism that is fit that has been designed uh with with this idea of of safety of of reliability of formalism in mind. And there aren't that many languages that have been built for that. As a matter of fact, this formal method idea usually they lead to extensions to existing languages uh often in the form of comments which is sort of adding a layer of complexity and

00:08:17 the connection is not easy. So it's been hard uh to to to deploy those methodology in I would say outside of the research lab in a in a context. Now, Spark is interesting because Spark is an evolution of a language that is called ADAB that was developed in the early 80s uh with really this idea to specify as much as possible in software to let the compiler verify things or generate

00:08:43 checks and so on so forth. And it turns out that all of these ideas that we developed uh in the 80s lend themselves particularly well to the need of formal methods because all of the information is is there already. So indeed today I would go as far as saying that the only programming language that allows you to deploy formal methods at the level of the programmer right there are many

00:09:06 other places where you may want to do that but for programming sake today spark is really the only language that allows you to do that at scale in industrial context. Well that that's one reason why it keeps coming up in in these sort of discussions. I know as we evolve or as the industry evolves and these these challenges keep coming up, maybe that'll

00:09:27 be the solution next time. Maybe it'll be another thing. But for today, that's a great insight uh from our expert Quentyn Ocean, chief product and revenue officer at ADOR. Quentyn, thank you so much for joining us today. Thank you.