Cognitive Vehicles, Interviews, Level 5 Autonomous Driving

AdaCore Interview: Confident Algorithms with Formal Proof Techniques

In the run-up to the ScaleUp 360° Auto Vision, we.CONECT had a chat with AdaCore about their session titled “Confident Algorithms with Formal Proof Techniques”, the company’s unique selling point, challenges, solutions and developments in the vehicle automation industry expected in the next 2 years.

Your solution is announced at ScaleUp 360 Auto Vision Europe under the title “Confident Algorithms with Formal Proof Techniques” What is the most important message to the participants and your clients in this context?

Our goal is to help the software development community produce higher quality software faster, with fewer bugs in the released product, which not only reduces cost but also provides a competitive advantage. Using familiar workflows, software engineers can use tools and techniques to develop software that is easier to maintain, proven to be logically sound, and can have guarantees on program properties. These tools are qualified to the highest ISO 26262 level of TCL3 and come with high-quality expert support from AdaCore.

we.CONECT: What would you highlight as the unique selling point of your solution/approach?

Traditional software development lifecycles put most of the responsibility for functional correctness in the testing and QA steps. This can be problematic when using typical testing strategies with languages such as C and C++, because the testing tends to be focused around functionality instead of incorrect or unintended usage of the language. This can lead to some serious safety and security issues that can slip by the typical QA process. In order to guarantee that these things are caught, extensive and exhaustive (read expensive) test procedures are required that may not be practical to implement.

Technologies that utilize formal proof can ameliorate the expense of these traditional setups by moving the burden of functional correctness from the testing stage to the development stage of the software development lifecycle. During the webinar we will discuss how formal proof can be used to replace testing, guarantee functional correctness, and lower the cost for developing safety-critical systems.

we.CONECT: If you think of your clients’ requirements: Which problem areas in the context of vehicle automation do you regard as particularly critical?

Software that is safety-critical and security-critical has potential to help as well as to harm. Of course, nobody wants critical software to fail, but how do you balance the concerns of software quality, time to market, and overall cost so that you can succeed?

we.CONECT: What do you think are the best approaches / technologies to meet these challenges

Technologies that effectively tackle the recurring problems of software development, that understand engineering as a human activity, that respect the true costs of bugs at various stages of software development, testing, release, and maintenance, and that have pedigree in industries with similar requirements for safety and security will provide the best quality and cost-savings. The Ada and SPARK languages aim for your success in getting software built correctly, more easily, with less risk, and with less cost.

we.CONECT: How do you assess – also with regard to the participants and speakers of ScaleUp 360 Auto Vision Europe – the developments on the market for solutions for vehicle automation in the next 1-2 years?

Automotive software has not typically been controlled by regulatory bodies because it has not been in a safety critical pathway. If the satellite radio is a little buggy, the car still functions safely. Now that more of the car’s basic functions are controlled by software, more regulatory steps need to be taken to ensure everyone’s safety. Considering the huge leaps in the technologies used in autonomous and conventional vehicles that will be discussed by the various speakers in the webinar, more due-diligence needs to be paid to the goal of meeting the safety requirements of various certifications like ISO26262 when considering the adoption of new technologies.

we.CONECT: Thank you AdaCore for chatting with us!

Join Albert Lee’s webinar session at 2020 ScaleUp 360° Auto Vision:

Session title: Confident Algorithms with Formal Proof Techniques
Date: Thursday June 04, 2020, 13:30 CET
Follow this link to sign up now for free: Online registration
Signing up automatically gives you access to all webinar sessions at ScaleUp 360° Auto Vision, June 03 – 04, 2020

ScaleUp 360° Auto Vision – the digital event deep diving into Computer Vision and Sensor Fusion technologies for autonomous vehicle perception. Experience 2 days with digital case studies by stakeholders involved in computer vision, sensor hardware, image processing and sensor fusion in the Level 5 automation scene. Learn, engage and discuss automotive tech innovation in real-time with thought leaders across the globe – right from your desk.