Formal Verification of Logical and Temporal Properties of ADAS Supervisory Control Systems

Staff Mentor:

prof. J. Hellendoorn

Other Mentor(s):

Dr. Arturo Tejada Ruiz (TNO)


Transportation and infrastructure; Networked control systems



The Integrated Vehicle Safety (IVS) department at TNO develops technology for automated driving and cooperative mobility for intelligent vehicle applications. An important aspect in all such applications (e.g., cooperative vehicle platooning, autonomous urban vehicles) are the algorithms used for control supervision.

These algorithms are in charge of, among other things, sequencing vehicle maneuvers, deciding the type of control actions needed under different (vehicle) operating conditions, reasoning about the vehicle health & safety, initiating and sustaining cooperative actions with other vehicles, etc.

Although the actions of specific supervisory algorithms are well understood, the combination of multiple such algorithms in a complete system presents significant challenges including: (unwanted) emergent behavior due to algorithm interactions, verification of joint logical and temporal properties, etc.

Assignment description:

The main goal of this assignment is to develop a framework and a methodology for the composition and formal verification of supervisory algorithms for advanced driver assistance systems (ADAS).

Main Elements

• Architectural framework for the composition of supervisory algorithms
• Formal logical and temporal verification of current TNO ADAS solutions

Added value for the project:

• Tools and methods for the formal verification of vehicle supervisory systems.

Added value for the intern:

• Know how real-life ADAS systems

• Working in a dynamic environment on automated driving functions

© Copyright Delft Center for Systems and Control, Delft University of Technology, 2017.