Embedded systems are used in many safety-critical domains, including in medicine, traffic, and critical infrastructure. Due to the strict timing requirements such systems usually have to fulfill, they often run on real-time operating systems (RTOS). As the RTOS influences the function and the timing behavior of the system, it becomes important to rigorously ensure the correctness and safety of applications running on them while taking into account the semantics of the operating system. Existing verification approaches are either limited to specific RTOS components or based on explicit state space exploration techniques such as model checking, which do not scale well for concurrent or timed applications. In this article, we propose a deductive approach to verify crucial safety properties about applications written for the widely-used RTOS FreeRTOS using the VerCors verifier. Our key ideas are threefold: (1) We provide a formalization of a wide variety of FreeRTOS features and an automatic encoding of FreeRTOS applications for verification with VerCors. (2) We adapt and enhance an existing approach for automatic invariant generation to largely automate the typically high-effort verification process. (3) We present a systematic technique to verify both functional and timing-related properties of cooperative RTOS applications. We demonstrate the applicability of our approach on a FreeRTOS demo application as well as an adaptive cruise control system.

Abstract This paper gives an overview of the most recent developments on the VerCors verifier. VerCors is a deductive verifier for concurrent software, written in multiple programming languages, where the specifications are written in terms of pre-/postcondition contracts using permission-based separation logic. In essence, VerCors is a program transformation tool: it translates an annotated program into input for the Viper framework, which is then used as verification back-end. The paper discusses the different programming languages and features for which VerCors provides verification support. It also discusses how the tool internally has been reorganised to become easily extendible, and to improve the connection and interaction with Viper. In addition, we also introduce two tools built on top of VerCors, which support correctness-preserving transformations of verified programs. Finally, we discuss how the VerCors verifier has been used on a range of realistic case studies.

Simultaneous localization and mapping (SLAM) is a prerequisite for accurate navigation of autonomous vehicles. Although this is often safety- critical, systematic approaches for testing the correctness and accuracy of SLAM algorithms are missing. In this paper, we present an approach for automated and systematic testing of SLAM algorithms. We identify challenging environmental features for SLAM, define coverage criteria that characterize the SLAM problem’s input space, and develop a method for automatically generating high-coverage tests. We demonstrate the effectiveness of our approach with a case study on an existing FastSLAM implementation.