Incremental Development, Incremental Checking: Software Model Checking of Temporal HAL Interface Specifications for Embedded Systems with a Hardware Abstraction Layer

• Applicants: Professor Dr. Andreas Podelski; Professor Dr.-Ing. Axel Sikora
• Subject Area: Software Engineering and Programming Languages
• Term: since 2022
• Project identifier: Deutsche Forschungsgemeinschaft (DFG) - Project number 503812980

The project will explore the potential of software model checking, a paradigm for black-box verification tools based on automatic abstraction via CEGAR, in a new approach. The idea is to adapt the software development process to the capabilities of software model checking (as opposed to the more usual approach of adapting the verification process to the iterative software development). The concrete context where we carry out the research is the development of application programs for embedded systems with the guarantee of the absence of violations of temporal specifications for the interface with the hardware abstraction layer.

• DFG Programme: Research Grants