Verification of Decision Making Software in an Autonomous Vehicle: An Industrial Case Study

• Correctness of autonomous driving systems is crucial as incorrect behaviour may have catastrophic consequences. Many different hardware and software components (e.g. sensing, decision making, actuation, and control) interact to solve the autonomous driving task, leading to a level of complexity that brings new challenges for the formal verification community. Though formal verification has been used to prove correctness of software, there are significant challenges in transferring such techniques to an agile software development process and to ensure widespread industrial adoption. In the light of these challenges, the identification of appropriate formalisms, and consequently the right verification tools, has significant impact on addressing them. In this paper, we evaluate the application of different formal techniques from supervisory control theory, model checking, and deductive verification to verify existing decision and control software (in development) for an autonomous vehicle. We discuss how the verification objective differs with respect to the choice of formalism and the level of formality that can be applied. Insights from the case study show a need for multiple formal methods to prove correctness, the difficulty to capture the right level of abstraction to model and specify the formal properties for the verification objectives.

Ämnesord

NATURVETENSKAP  -- Data- och informationsvetenskap -- Programvaruteknik (hsv//swe)

NATURAL SCIENCES  -- Computer and Information Sciences -- Software Engineering (hsv//eng)

TEKNIK OCH TEKNOLOGIER  -- Elektroteknik och elektronik -- Robotteknik och automation (hsv//swe)

ENGINEERING AND TECHNOLOGY  -- Electrical Engineering, Electronic Engineering, Information Engineering -- Robotics (hsv//eng)

TEKNIK OCH TEKNOLOGIER  -- Elektroteknik och elektronik -- Reglerteknik (hsv//swe)

ENGINEERING AND TECHNOLOGY  -- Electrical Engineering, Electronic Engineering, Information Engineering -- Control Engineering (hsv//eng)

NATURVETENSKAP  -- Data- och informationsvetenskap -- Datavetenskap (hsv//swe)

NATURAL SCIENCES  -- Computer and Information Sciences -- Computer Sciences (hsv//eng)

TEKNIK OCH TEKNOLOGIER  -- Elektroteknik och elektronik -- Datorsystem (hsv//swe)

ENGINEERING AND TECHNOLOGY  -- Electrical Engineering, Electronic Engineering, Information Engineering -- Computer Systems (hsv//eng)

Nyckelord

Autonomous driving · Formal verification · Supervisory Control Theory · Model checking · Deductive verification

Publikations- och innehållstyp

kon (ämneskategori)

ref (ämneskategori)