What is it about?
We develop a method to prove the safety and correct implementation of embedded systems using the deductive verifier VerCors. Our approach is based on previous work on the design language SystemC, which we extend for the commonly used real-time operating system FreeRTOS. It mainly deals with the challenges of real-time operation, such as dynamic task execution times and time-dependent scheduling.
Featured Image
Photo by Lenny Kuhne on Unsplash
Why is it important?
Our approach combines the strengths of different verification techniques, deductive verification and model checking, to allow for a largely automated verification process. While we do pay for this automation with long verification times for larger programs, our deductive technique still allows us to scale well with regard to certain aspects of the system, such as the size of the data space.
Read the Original
This page is a summary of: Deductive Verification of Cooperative RTOS Applications, ACM Transactions on Embedded Computing Systems, August 2025, ACM (Association for Computing Machinery),
DOI: 10.1145/3759251.
You can read the full text:
Contributors
The following have contributed to this page
