Contract Based Verification of Non-functional Requirements for Embedded Automotive C Code

TL;DR

This paper introduces a new approach for verifying non-functional requirements in safety-critical embedded C code by defining a contract language, implementing a checker, and applying it to real-world automotive software.

Contribution

It presents a novel set of rules for non-functional requirements, a C interface contract language, and a Frama-C plugin for verification, applied to automotive embedded systems.

Findings

Verified safety-critical C code in Scania trucks using the new toolchain.

Defined module and function contracts based on informal requirements.

Ensured control flow and data flow safety properties in embedded C code.

Abstract

Code contracts provide a robust way to specify functional requirements of safety-critical software in embedded systems. For example, the ANSI/ISO C Specification Language (ACSL) can be used to specify the functional behavior of C code that is then formally verified by the Frama-C framework's Wp plugin. However, non-functional requirements, such as restrictions on control flow and data flow, are also important for embedded systems safety. Untrusted code developed by subcontractors, junior developers, or generated by large language models, can be verified by Wp but may nevertheless call unsafe functions or use uninitialized program variables. To address this problem, we constructed a set of general rules concerning non-functional requirements of C code in safety-critical embedded systems. Our rules are orthogonal to popular C rulesets such as MISRA-C and center on modules and their interaction through interfaces. To enable checking our rules, we propose an interface specification contract language for C modules. We implemented a checker for our rules as a Frama-C plugin, which takes as input a C module and its contract and checks control flow and data flow properties, ensuring, e.g., that only permitted functions are called by the module. We integrated our checker in a toolchain to enable specification and verification of module contracts and ACSL contracts for untrusted code. We report on two case studies on safety-critical C code using software in Scania trucks, where we defined module contracts and ACSL function contracts based on informal system requirements and verified them using our toolchain.