The automotive industry is transitioning to Software- Defined Vehicles (SDVs) and Automotive Grade Linux (AGL), emphasizing modular and updatable software stacks. AGL, an open-source platform for High- Performance Computers (HPC) in modern vehicles, en- sures scalability, real-time performance, and interoper- ability by integrating diverse software components from multiple suppliers. It reduces costs, fosters innovation, and adheres to industry standards.
This thesis leverages AGL to tackle SDV integration and verification challenges. It aims to develop automated formal modeling methods for open-source SDV compo- nents and their compositions, enabling structured ver- ification. Formal models will be created for individ- ual components and integrated into a cohesive system, with verification applied to ensure reliability. An HPC demonstrator with AGL will showcase these methods, streamlining integration checks and supporting scal- able, efficient verification workflows.
Download as PDF
Student Target Groups:
- Computer Science (CS)
- Information and Computer Engineering (ICE)
- Electrical Engineering (EE)
Thesis Type:
Goal and Tasks:
- Develop a method for the automatic formal model- ing of open-source SDV components.
- Implement a method to generate formal models for individual components and their integration.
- Verify the components and their integration using formal verification techniques.
- Evaluate the method’s effectiveness through a demonstrator system utilizing an HPC with AGL.
Recommended Prior Knowledge:
- Formal Methods and Model Checking Techniques
- Proficiency in Programming (e.g., C/C++, Python)
- Familiarity with Open-Source Software
Start:
Contact: