Contract Based Verification of Non-functional Requirements for Embedded Automotive C Code Jesper Amilon1 , Merlijn Sevenhuijsen1,2 , Mattias Nyberg2 , and Karl Palmskog1 KTH Royal Institute of Technology, Sweden {jamilon,palmskog}@kth.se 2 TRATON AB, Sweden {merlijn.sevenhuijsen,mattias.nyberg}@scania.com
arXiv:2605.21532v1 [cs.PL] 19 May 2026
1
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. Keywords: C · ACSL· Control flow · Data flow · Formal verification · Non-functional requirements
1
Introduction
Functional requirements of a program or system intuitively express what a system is supposed to do, such as returning some output for a particular input. In contrast, non-functional requirements intuitively express how a system or program must be constituted. Such requirements may concern, e.g., program control flow restrictions, bounds on execution time [1] and other resources such as memory [12], or even details on formatting of source code.
2
J. Amilon et al.
Functional requirements for safety-critical software, such as for embedded C code in automotive systems, can be expressed using code contracts and then formally verified for adherence to these contracts [25,43]. For example, contracts for functions in C code can be written in the ANSI/ISO C Specification Language (ACSL) [9] and verified using the Frama-C framework and toolchain [7], e.g., using the Wp plugin for deductive verification [23]. However, due to their diverse nature, non-functional requirements are difficult to capture in a single contract language and framework. For example, information flow security may be expressed at code level using type annotations, while execution time bounds may be expressed at system level using scheduler assumptions. In industrial practice, non-functional requirements are therefore often enforced by manual code reviews and tools such as linters and other static checkers, such as Cppcheck [29]. Non-functional requirements, in particular on control flow and data flow, are important in safety-critical automotive C code and explicitly mentioned by standards such as ISO 26262 [21]. Requirements on control flow in embedded systems software frequently concern inter-module properties, e.g., that a software module controlling some part of an Electronic Control Unit (ECU) does not inadvertently call certain functions in other modules. Formal verification of ACSL contracts does not rule out such undesirable calls, since the effect of the call may be independent of the properties that the contract requires. Explicit specification and checking of such essential non-functional requirements may not be necessary when embedded software is developed by experienced engineers. Code reviews may even go beyond what is necessary and address maintainability and other less safety-critical issues. But when development includes untrusted code, e.g., as developed by subcontractors or junior engineers, or generated using large language models (LLMs), explicit specification and verification become necessary to ensure system-level properties [22]. Based on our analysis of deployed embedded systems software written in C for ECUs in Scania trucks, we constructed a set of general rules for non-functional requirements of C code, centered on modules defined as pairs of .h files (declaring function signatures and datatypes) and .c files (containing data and function definitions). The rules are distilled from general requirements governing Scania embedded C code and internal coding standards, and capture properties that were found to be violated when generating code using LLMs [37]. They are orthogonal to rulesets such as the power of 10 [17] and MISRA-C [30]. To enable rule checking, we defined a module Interface Specification (IS) contract language that bridges the gap between C functions considered separately (as in ACSL) and modules of C code running inside ECUs. Conventionally, such a module realizes control software for a single ECU and externally exposes a subset of its C functions to other modules. Our module contracts constitute one step from individual ACSL function contracts towards automotive system (vehicle) level contracts. We developed a Frama-C plugin dubbed VerNFR that checks our rules for a C module using an IS contract. The plugin is released as open source software [4] and complements earlier work on verifying functional requirements using the Autodeduct toolchain [5], also based on ACSL.
Contract Based Verification of Non-functional Requirements
3
We integrated VerNFR into a toolchain to enable practical verification of both module IS contracts and ACSL function contracts. The toolchain is based on using a collection of critics on untrusted C code [22,37] that ensure the code satisfies properties from trusted specifications like contracts. We applied our toolchain in two case studies of modules of ECU controller software from Scania trucks. For each module, we annotated functions with ACSL contracts and wrote module IS contracts based on informal requirements. We then checked the latest available Scania module implementation code using VerNFR, Frama-C Wp, and Cppcheck [29]. Finally, we performed preliminary experiments on generating case study module code from specifications using two popular LLMs, resulting in verified implementations. In summary, we make the following contributions: 1. From principles rooted in modularity and information hiding, we propose a ruleset capturing general non-functional requirements of automotive C code. 2. We define a contract language that can describe key practical non-functional requirements on interfaces of C modules in automotive systems. 3. We implement a novel contract-based checker dubbed VerNFR for our rules, which we integrated into a toolchain for verification of untrusted C code. 4. We perform and report on two case studies applying our contract approach and toolchain to real-world application modules from automotive ECUs.
2
Background
In this section, we provide some background on automotive embedded C code and its specification and verification using ACSL, Frama-C, and other tools. 2.1
Embedded control software in Scania trucks
Scania trucks contain tens of Electronic Control Units (ECUs) which run software, called application modules, that control and interact with physical actuators and sensors. Each ECU has a static scheduler that repeatedly calls the entry point function of each application module every 10 ms. Application modules inside an ECU frequently interact with each other and with infrastructure software, primarily using a real-time database (RTDB) module and a diagnostics module. Commonly, an application module invoked by the scheduler runs an entry-point function which reads values from RTDB, performs some computations, and writes back the results to RTDB. Inter-ECU interaction, in contrast, is based on signals using the CAN protocol [20]. Figure 1 illustrates the embedded systems architecture used by Scania for ECUs and their application modules. An application module implementation is typically written in the C language and contains code that has no unbounded loops or recursion and is (when viewed in isolation) executed sequentially. The subset of C used at Scania for application module development roughly corresponds to MISRA-C (described in Section 2.4), but with additional conventions and rules.
4
J. Amilon et al. ECU Scheduler
write void Module
call function every 10 ms
void sgmm_10ms(void) sgmm_10ms(void) void { sgmm_10ms(void) { .... .... { } ....} }
read & write read & write
RTDB
read & write
Low-level SW/HW
read
Actuators Sensors
Diagnostics read & write
CAN
Fig. 1: ECU architecture with internal and external interactions.
2.2
Modules and C code
The embedded systems concept of an application module used by Scania does not precisely map to any definition in a language standard, such as the C99 standard that we target [19]. C99 instead divides software into translation units. Roughly speaking, a translation unit consists of a .c file and, transitively, all files included with the #include-directive. In practice, C software is often organized into implementation files (.c files) and associated header files (.h files). In this approach, a .c file contains definitions, while a corresponding .h file contains the declarations and macro language definitions intended to be shared with other translation units [15]. The declarations of other translation units are imported by including the corresponding .h files. We adhere to this convention, and operationalize an automotive application module as a pair of a .c file and an .h file of C code. Such a pair is then also a C99 translation unit. When declaring functions and variables in C, storage specifiers can be used to decide visibility to other translation units. Specifically, global declarations using the static storage specifier are not visible to other translation units. Global declarations without static storage specifier are visible to other translation units. From the module perspective, one can view functions declared without the static storage specifier as entry points to the module and functions with static storage specifier as local functions. 2.3
ACSL and Frama-C
The ANSI-C Specification Language (ACSL) [9] allows specifying properties of C code. ACSL specifications are written in the source code files as comments starting with @. ACSL is based on first-order logic and includes function contracts, loop invariants, assertions, predicates, and logical functions. An example of an ACSL function contract is shown in Figure 2 for the function update_sat. The function returns an updated value of timer, by incrementing or decrementing it by 1, depending on the condition cond. If the new value lies outside the domain [min, max], the result is truncated to the corresponding extreme point. The function is specified with an ACSL contract where the requires clause states that the two extreme points form a non-empty interval, the assigns clause states that no global memory locations are allowed to be modified, and the ensures clause specifies how the output should relate to the inputs. Frama-C is a platform for analysis and verification of C code and ACSL specifications. Frama-C is comprised of a kernel and numerous plug-ins. The
Contract Based Verification of Non-functional Requirements
5
/* @ requires min < max && min <= timer <= max ; assigns \nothing ; ensures ( cond == 0 == > \result == MAX ( min , \old ( timer ) - 1)) && ( cond != 0 == > \result == MIN ( max , \old ( timer ) + 1)); */ static int update_sat ( char cond , int timer , int min , int max ) { int res = timer ; if ( cond ) { res += 1;} else { res -= 1;} if ( res > max ) res = max ; if ( res < min ) res = min ; return res ; }
Fig. 2: Example C function annotated with an ACSL contract.
kernel is responsible for parsing the C sources and the ACSL specifications into a combined AST (Abstract Syntax Tree), which can be analyzed by the plugins. Before constructing the AST, Frama-C uses the GCC [40] preprocessor to preprocess the C sources, e.g., to resolve compiler directives such as #define. The Frama-C Wp plugin [8] is used to verify that a function satisfies its ACSL function contract. Based on weakest-precondition calculus, Wp verifies the program by generating a set of proof obligations, which must be discharged for the verification to succeed. Verification with Wp is typically combined with checking absence of run-time errors, such as array-out-of-bounds or overflows. The command line option wp-rte instructs Wp to generate proof obligations also for such run-time errors. To discharge the proof obligations, Wp relies on SMT solvers, such as Alt-Ergo [13] and Z3 [31]. The Frama-C EVA plugin [11], based on abstract interpretation, is used to calculate domain ranges for variables. The analysis performed by EVA is often used as input to other plugins. ACSL Importer is a plugin for Frama-C which allows ACSL specifications separately from C code [14]. The plugin enables listing all function contracts for modules, but does not enable expressing properties of modules themselves. 2.4
Non-functional requirements and C static checking
For safety-critical C modules in ECUs, we consider functional correctness as a baseline, which we define as adhering to given requirements on functional behavior. For example, functional requirements may be defined in natural language and then translated to ACSL contracts on module functions [43]. In contrast, nonfunctional requirements on C modules in ECUs come from a variety of sources and are unfeasible to express at code level using a single specification language. Several standards provide guidance on desirable non-functional properties of C code. ISO 26262 [21] is a standard for safety in automotive systems and includes general requirements on software, but these requirements must be contextualized significantly to be applied at the code level. The MISRA-C standard [30] defines, through a set of guidelines, a subset of C that reduces the risk for undesirable program behavior and errors. MISRA-C rules distinguish between directives and rules. Directives are guidelines that may require analysis
6
J. Amilon et al.
beyond the source code, such as documenting how the code relates to external requirements. Rules are intended to be checkable on the code itself, and typically aim to restrict usage of C constructs that are complex and error-prone. A subset of the MISRA-C rules can be checked using static analysis tools, such as Cppcheck [29]. Each guideline is further classified as mandatory, required, or advisory. Mandatory guidelines must be followed without exception to conform to MISRA-C, while required guidelines are expected to be followed but may be deviated from with justification, and advisory guidelines represent recommended practice. Cppcheck and other MISRA-C checkers commonly report the classification of each violation found in the checked code.
Table 1: Principles for interfaces in C code used in embedded systems. Principle
Motivation
1
All interaction with other modules Interacting with function calls, rather than reading and shall be manifested through function writing to global variables, simplifies modular code decalls. velopment.
2
Standardization increases code readability and disalThe interface of the module shall be lows, e.g., unconventional usage of .h files and .c files, standardized. and ensures that data-flow between modules does not cause unexpected behavior.
3
The interface specification shall define the entry-point functions for the This ensures that the interface is clear and well-defined. module, and exactly these shall be callable from other modules.
4
The interface specification shall constrain exactly which functions in other modules that are permitted to be called; and the module shall adhere to this.
5
The interface specification shall conThe behavior of other modules may depend on the call strain the call order of function calls order. For example, to ensure that variables are initialto other modules, and the module ized before they are read. shall adhere to this.
6
The interface specification shall con- This simplifies, strengthens, and clarifies the concept of stitute a single standalone artifact. an interface specification.
3
Interfaces: from Principles to Rules
This is important since (i) a function signature may be defined in several .h files, so the interface specification shall indicate which one to use, and (ii) it may be necessary to permit only a subset of the functions in an .h file to be called.
In this section, we develop principles and rules for module interfaces in automotive embedded C, which guide how modules interact with each other. The principles capture non-functional properties of the modules and are meant to complement specifications for the functional behavior, such as ACSL function contracts. We aim for the principles to enable modular development and verification of the modules. To this end, we require modules to be equipped with an Interface Specification (IS). We first introduce a set of core principles for interface properties. These principles are distilled into coding rules and a contract language for Interface Specifications, where the latter is defined in Section 4.
Contract Based Verification of Non-functional Requirements
7
Table 2: Rules for control flow. ID
Rule
Rationale
CFR1
The module may only call external functions permitted by the interface specification.
Ensures Principle 4.
CFR2
The order of external calls shall respect the order constraints in the interface specification, given an assumed call order of the entry-point functions of the module.
Ensures Principle 5.
Function pointers shall not be used
Prerequisite for checking CFR1 and CFR2.
No function definitions or initializations in the .h file.
Helps ensure Principle 2.
Include only .h files.
Helps ensure Principle 2.
Entry-point functions shall be declared in the .h file without the static storage-class specifier.
Helps ensure Principle 3.
Entry-point functions shall be defined in the .c file.
Helps ensure Principle 3.
CFR8
Non entry-point functions shall be declared in the .c file with a static storage class specifier.
Helps ensure Principle 3.
CFR9
Only entry-point functions in the interface specification shall be declared in the .h file.
Helps ensure Principle 3.
CFR10
The keyword extern shall not be used, except for the declaration of entry-point functions.
Helps ensure Principle 2.
CFR11
The types for the function declarations in the .h file and the interface specification shall match exactly.
Helps ensure Principle 3.
CFR3 CFR4 CFR5 CFR6 CFR7
3.1
Interface principles
Our principles for module interfaces, and module interface specifications are given in Table 1. In accordance with Section 2.2, we adopt the convention that a module consists of a pair of a .c file and an .h file. The principles are largely based on experience from verifying automotive embedded software [43,16,5]. We also consider the long-standing convention of employing information hiding in modular software development [33]. Information hiding means that implementation details that may be subject to change should be hidden. For example, in Principle 1, we treat global variables within a module as implementation details that can be changed at any time, whereas the entrypoint functions should provide a stable interface across module versions. 3.2
Interface rules
We operationalize the principles into 17 rules that are necessary to follow for a module to adhere to the 6 principles. We split the rules into two categories: in Table 2, rules that constrain the control flow between modules, and in Table 3, the rules that constrain the data flow between modules. For each rule, we also indicate how they relate to the 6 principles. Given an interface specification and a module, our intention is that these rules can be checked using conventional methods for static analysis or formal
8
J. Amilon et al.
ID
Rule
Rationale
DFR1
All variables with file-global scope shall be declared in the .c file with the static storage specifier.
Implies that module interaction through global variables is prohibited. Helps ensure Principle 1.
DFR2
Pointer arithmetics shall not be used.
Necessary to ensure that all interactions with other modules are through function calls. Helps ensure Principle 1.
DFR3
Explicit type casting from pointers and to pointers shall not be used.
Necessary to ensure that all interaction with other modules is through function calls. Helps ensure Principle 1.
DFR4
A static declared variable shall not be read before it is explicitly initialized or written to.
All variables shall be initialized to a meaningful value; we do not rely on default initialization to 0. Helps ensure Principle 2.
DFR5
Pointer literals shall not be used.
Necessary to ensure that all interaction with other modules is through function calls. Helps ensure Principle 1.
DFR6
Typedefs shall be used whenever applicable.
Ensures that the module interacts in a predictive way (Principle 2). For example, the same module can be used on platforms with different bit-sizes, and using typedefs ensures that the module behaves as expected on all platforms.
Table 3: Rules for data flow.
verification. In Section 5, we develop a Frama-C plugin that verifies a subset of our rules. The list of rules is, intentionally, not complete with respect to adherence to the principles. Specifically, we have not included rules that are already covered by the MISRA-C standard [30]. For example, avoiding dynamic memory allocation, i.e., malloc and calloc, could help maintain Principle 1, but this is already covered by MISRA-C directive 4.12. Similarly, array out-of-bounds accesses may corrupt the interface of a module. Avoiding array out-of-bounds accesses is part of the general MISRA-C directive 4.1: Minimize run-time errors.
4
Module Interface Specification Contract Language
Based on the principles in Section 3, we propose in this section a language for interface specification (IS) contracts. We choose to define the interface specifications as contracts, since they need to capture both assumptions and guarantees. For example, in Principle 5, we want to assume the call order for the entry-point functions, and guarantee the call order of the external calls. We provide some discussion on assume-guarantee contracts in Section 8. The intended use case of our IS contracts is to provide the necessary context for verification of the rules CFR1, CFR2, CFR6, CFR7, and CFR11 from Section 3. The remaining rules can be verified by analyzing the source code without module-related context.
Contract Based Verification of Non-functional Requirements
9
module tmon { entry_points : { void tmon_init ( void ) , int tmon_step ( void ) } entry_order : { tmon_init < tmon_step } exte rnal_c alls : { sensors : { void t m o n _ s e n s _ c r e a t e ( void ) , int tmon_ sens_r ead ( void ) } , warnings : { void t m o n _ w a r n _ c r e a t e ( void ) , void t m on _w a rn _w r it e ( int w ) } } external_call_order : { t m o n _ s e n s _ c r e a t e ( X ) < tmon _sens_ read ( X ) , t m o n _ w a r n _ c r e a t e ( Y ) < t m on _w a rn _w r it e ( Y ) } }
Fig. 3: Module Interface Specification (IS) contract .is file for a timed monitor.
tmon_b.h
tmon_a.h void tmon_init ( void ); 2 int tmon_step ( void ); 1 3
void tmon_init ( void ) ; 2 static int tmon_step ( void ) ; 3 int get_t mon_ti mer ( void ) ; 1
tmon_a.c
tmon_b.c
# include " sensors . h " 2 # include " warnings . h "
1
3
3
1
4
static int timer ;
# include " sensors . h " 2 # include " warnings . h " 4
5
5
6
void tmon_init ( void ){ timer = 5; 8 t m o n _ s e n s _ c r e a t e (); 9 t m o n _ w a r n _ c r e a t e (); 10 }
6
7
7
10
11
11
12
void tmon_step ( void ){ int sens = t mon_se ns_rea d (); 14 timer = update_sat ( 15 sens , timer , 0 , 10 16 ); 17 if ( timer == 10) { 18 // activate warning 19 t m on _ wa rn _ wr it e (1); 20 } else if ( timer == 0) { 21 // deactivate warning 22 t m on _ wa rn _ wr it e (0); 23 } else { 24 // do nothing 25 } 26 }
12
13
13
27
27
28
(a) Implementation that satisfies the tmon IS contract.
int timer ; void tmon_init ( void ) { t m o n _ s e n s _ c r e a t e () ;
8 9
}
static void tmon_step ( void ) { int sens = tm on_se ns_rea d () ; 14 timer = update_sat ( 15 sens , timer , 0 , 10 16 ); 17 if ( timer == 10) { 18 // activate warning 19 t m on _w a rn _ wr it e (1) ; 20 } else if ( timer == 0) { 21 // deactivate warning 22 x m on _w a rn _ wr it e (0) ; 23 } 24 } 25
int get_t mon_ti mer ( void ) { return timer ; 28 } 26
(b) Implementation that does not satisfy the tmon IS contract.
Fig. 4: Implementations of the timed monitor (tmon) module from Figure 3.
10
J. Amilon et al.
⟨ISContract⟩ ::= module ⟨id ⟩⟨EntryPoints⟩⟨EntryOrder ⟩⟨ExtCalls⟩⟨ExtOrder ⟩ ⟨EntryPoints⟩ ::= entry_points ⟨FunDecl ⟩∗ ⟨EntryOrder ⟩ ::= EntryOrder ⟨OrderConstraint⟩∗ ⟨ExtCalls⟩ ::= external_calls ⟨ExtModule⟩∗ ⟨ExtModule⟩ ::= ⟨id ⟩⟨FunDecl ⟩∗ ⟨ExtOrder ⟩ ::= external_order ⟨OrderConstraint⟩∗ ⟨OrderConstraint⟩ ::= ⟨id ⟩ < ⟨id ⟩ | ⟨id ⟩ > ⟨id ⟩
Fig. 5: Grammar for module IS contracts.
4.1
Running example
The IS contract in Figure 3 for the module tmon serves as a running example together with two implementations: Figure 4a, which satisfies the IS contract, and Figure 4b, which violates the IS contract. The module consists of two entrypoint functions, tmon_step and tmon_init. The tmon_init function initializes the sensor and warning functionality, and is intended to be called at startup. tmon_step is intended to be called repeatedly by a scheduler, and implements a simple timed monitor. The tmon function reads the value of a sensor and, if the value is non-zero, the timer is incremented; otherwise, it is decremented. If the timer reaches 10, a warning is activated; if the timer reaches 0, the warning is deactivated. The purpose of the timer is to act as a delay filter, ensuring that the warning is activated and deactivated only after several consecutive consistent readings. Such a delay filter is common in automotive software to avoid false warnings or flickering behavior. Indeed, tmon is a simplified version of our real-world case study module SFLD, presented in Section 7. 4.2
Contract language syntax and semantics
We define the abstract syntax of IS contracts by the grammar shown in Figure 5, where ⟨FunDecl ⟩ is a function declaration as defined by the C99 standard. We provide an informal semantics for our contract language, and leave an explicit formal semantics as future work. Given an IS contract C, we describe its semantics by considering when (and when not) a module m satisfies the contract. We say that the module m satisfies C if the following three conditions hold: (i) Precisely the entry point functions in C are declared in the .h file and defined in the .c file of m. (ii) All external functions invoked by the .c file in m are permitted by C. (iii) Assuming that invocations of the entry-point functions in C follow the entry order in C, then the invocations of the external functions by mc respect the external call order in C. For the contract in Figure 3, we see that the module implementation in Figure 4a respects (i)-(iii), and hence satisfies the contract. The module implementation
Contract Based Verification of Non-functional Requirements
11
Table 4: Implemented verification tasks in VerNFR. The column “.is file” indicates if the task depends on an IS contract file. Task
Rule
.is file
T1
External function calls are permitted by the .is file
CFR1
✓
T2
Absence of function pointers.
CFR3
–
T3 T4
No function definitions in the .h file. Only .h files are included.
CFR4 CFR5
– –
T5
All entry points in the .is file are declared.
CFR6
✓
T6
All entry points in the .is file are defined.
CFR7
✓
T7
Non-entry points are declared in the .c file with static storage specifier.
CFR8, CFR9
✓
T8
Variables have static storage specifier.
DFR1
–
T9
All memory locations are explicitly initialized or written to before they are read.
DFR4
✓
T10 Absence of pointer literals.
DFR5
–
T11 Typedefs are always used when possible.
DFR6
–
in Figure 4b, on the other hand, violates all conditions (i)-(iii). Consequently, it does not comply with the contract. Regarding (i), we consider a function declared if there is a function declaration in the .h file of m and defined in the .c file without a static storage specifier. In Figure 4b, we see that the implementation violates (i) in two places. First, it declares and defines the function mod_error_status, which is not mentioned in the IS contract. Second, the entry-point tmon_step is declared with the static keyword. Regarding (ii), Figure 4b violates this due to the illicit invocation of ext2_write. in (iii), Figure 4b violates this, since the tmon_init function fails to call ext2_create. Thus, when tmon_step is called, the constraint ext2_read < ext2_create is violated. We can also relate conditions (i)-(iii) to the rules in Section 3. Condition (i) encompasses CFR6, CFR7, and CFR11, condition (ii) encompasses CFR1, and condition (iii) encompasses CFR2.
5
VerNFR: A Frama-C Plugin for Non-Functional Verification
We present now VerNFR [4], a Frama-C plugin written in the OCaml programming language [24], which implements a series of custom analyses tailored towards verification of the rules in Section 3. In the current state, VerNFR implements 11 verification tasks, listed in Table 4. The table also indicates which of the rules in Section 3 the task targets, and whether the task requires an .is file. Each task can be run as a command-line option when running Frama-C. We also provide a script, which takes as input a .c file, an .h file, and an .is file, and runs all verification tasks.
12
J. Amilon et al.
The verification tasks are, in general, implemented by traversing the AST built by the Frama-C kernel. For Task T9, we utilize the Frama-C plugin EVA, which can compute the memory locations, including global variables, that are inputs and outputs for each function. For each function and each input global variable, we can then check that it is either explicitly initialized in the .c file or that it is an output of some predecessor function according to the order constraints in the IS contract. The Task T4 is implemented with a regex search in the source files. In the current state, the tasks do not fully cover the rules in Section 3. Rules CFR10, DFR2, and DFR3 are difficult to implement in the Frama-C framework due to pre-processing implemented by the Frama-C kernel. For example, array accesses are converted into pointer arithmetic expressions; hence, verifying the absence of pointer arithmetic is difficult without false positives. We have also yet to implement verification of CFR2, that the module respects the call order constraints in the IS contract. We expect this to be the most difficult rule to implement support for since it requires symbolic analysis to infer the possible call order sequences in a program. Returning to our example module in Figure 4, the implementation in Figure 4a passes all the tasks T1-T11, while for the other implementation in Figure 4b, verification fails for tasks T1, T5, T6, T7, T8, and T9.
6
Toolchain for Module Development and Verification
To enable practical module development and verification with VerNFR and Frama-C, we propose a workflow supported by a toolchain, which we describe in this section. Recall that in our setting, a module is defined as a pair of a .h file and a .c file, as described in Section 2.2. To reason about the development and verification process for such modules, we distinguish between trusted and untrusted artifacts. Specifications and verification tools are treated as trusted, while implementations are treated as untrusted and must be verified. These implementations are produced by an agent, which may be a human programmer or an automated system such as an LLM. Verification is carried out by a collection of critics, which are components that analyze code with or without explicit specifications. A module is considered verified if all critics succeed; otherwise, it is not verified. Failure to verify does not necessarily imply incorrectness, but rather that correctness could not be established. The implementation, together with the associated specifications and header files, is referred to as a module package, which serves as the unit of verification. Figure 6 illustrates the proposed toolchain for formal verification together with non-functional requirement verification based on VerNFR (as described in Section 5). The workflow enables constructing a verified implementation of an embedded system C module. The colors in the figure indicate trust: blue elements represent trusted artifacts, while yellow elements represent untrusted artifacts and actors.
Contract Based Verification of Non-functional Requirements
13
The workflow consists of four steps. In 1 Toolchain Input, trusted artifacts specify the expected behavior and interface of the module. In 2 Module Package, an agent generates a candidate module in the form of a .c file and a .h file. In 3 Module Verification, the module implementation is validated by a set of trusted critics. In 4 Toolchain Output, the results are aggregated into a report and a verification outcome.
1 Toolchain Input Interface specification Natural language specification
2 Module Package
mod.is
3 Module Verification Critics GCC
calls, order, ...
mod.acsl
Formal specification
/*@ requires ... */
External header files
headers
Wp Cppcheck VerNFR
types.h ...
4 Toolchain Output Output parser
Module
Agent
mod.c int mod_run(void) { ... }
mod.h
Report GCC compiler: ✓ or × Wp:
✓ or ×
Cppcheck:
✓ or ×
VerNFR:
✓ or ×
int mod_run(void);
× Not verified
Untrusted
Verified
Trusted
Fig. 6: Proposed module development and verification workflow and toolchain based on VerNFR and Frama-C, where an untrusted agent generates code that is either verified or fails to verify.
At step 1 , we specify the input needed to construct a verified implementation of a module. An agent is provided with the following information: – An interface specification: A module IS contract, as defined in Section 4, defining entry-point functions, permitted external calls, and call-order constraints. – A natural language specification: Describes the desired functional behavior of each entry-point function in the IS contract in natural language.
14
J. Amilon et al.
– A formal specification: ACSL contracts for the entry-point functions from the interface specifications. These contracts must be consistent with the natural-language requirements to avoid contradictions. Additionally, ACSL contracts are provided for all external functions allowed by the interface specifications. The external contracts are necessary both for Wp to verify the entry-point functions and for the agent to correctly implement the module, as they specify the expected behavior of all permitted external calls. – Header files: All header files required for compilation. These provide types, macros, constants, and function declarations. In 2 , the trusted inputs are provided to an untrusted agent. The agent may represent a human programmer or an automated system such as an LLM. It produces the implementation files .c file and .h file, which together form the candidate module. Since the implementation is generated by the agent, it is treated as untrusted and must be validated. The generated files are combined with the trusted specifications to become the input to the next step. In 3 , the module package is analyzed by a set of trusted critics, each targeting complementary properties, including syntactic and functional correctness, coding-standard compliance, and interface-level constraints. Compilation with GCC is the first critic. It ensures that the program is syntactically correct, welltyped, and that all required declarations are available. We run GCC as the first critic since the result of the remaining critics is not meaningful if the module does not compile. After compilation, we run the remaining critics. The Frama-C plugin Wp (see Section 2.3) verifies functional correctness, i.e., that the entry-point functions implement their ACSL contracts. We run Wp with the Wp-rte option to ensure the absence of runtime errors. Next, the Cppcheck critic performs static analysis with respect to the MISRA-C coding guidelines (see Section 2.4). Finally, the VerNFR (see Section 5) critic checks adherence to the non-functional rules defined in Section 3, Since all critics are assumed to be trusted, successful verification indicates that the implementation satisfies the checked properties. In 4 , outputs from all critics are collected by an output parser, which produces a unified report summarizing the results. The final outcome consists of the module package, the generated report, and a verification verdict. Based on the collected results, the module is classified as verified or not verified. Since the critics are not complete, a negative result indicates that correctness could not be established. However, for many programs, the critics are complete enough to reach a verdict and draw conclusions.
7
Case Studies
In this section, we present two case studies on ECU controller modules from Scania trucks, for which we have applied the toolchain in Figure 6. Before introducing the modules in detail, we describe the general approach for the case studies.
Contract Based Verification of Non-functional Requirements
15
module sfld { e nt ry _ fu nc t io n s : { void Sfld_create ( void ) , void Sfld_10ms ( void ) } entry_order : { Sfld_create < Sfld_10ms } exte rnal_c alls : { rtdb . h : { tB g e tD ia g Te st C on d ( DIAG_TEST test ) , void Rtdb_createBs ( tBs sig ) , void R td b_ c re at e S3 2 s ( t32s sig ) , tBS Rtdb_readBs ( RTDB_S sig ) , void Rtdb_writeBs ( RTDB_S sig , tBS bs ) , void Rtdb_w riteS3 2s ( RTDB_S sig , tS32S sig ) , ... } } e x t e r n a l _ c a l l _ o r d e r : { Rtdb_createBs < Rtdb_WriteBs , ... } }
Fig. 7: Excerpt of the IS contract for SFLD.
7.1
Specification and verification approach
To run the toolchain on each module, we first wrote ACSL specifications and IS contracts, based on existing requirement documents in natural language written by engineers. The ACSL specifications consist of function contracts for each entry-point function. We also wrote ACSL contracts for the external functions that are permitted to be called by the IS contract. Both the ACSL contracts for the external functions and the entry-point functions could partially be reused from previous work [43,36]. After writing the ACSL specifications and IS contracts, we identified an existing reference implementation of each module, corresponding to the latest available version of the code written by human engineers. We then ran steps (3)-(4) in Figure 6 for the reference implementations, together with the ACSL specifications and IS contracts that we wrote. Thereafter, we also performed some preliminary experiments for our toolchain with LLM-based agents that implement the modules. The results for the reference implementations are presented in Section 7.4, and the results for the LLM-based implementations are presented in Section 7.5. Since the modules are proprietary, we cannot provide their source code, ACSL specifications, or the full version of their respective natural language requirements. Instead, we give an overview of each module. The total specification and verification effort amounts to approximately 2 person weeks per case study for a verification engineer. This includes writing the ACSL specifications and the IS contract, and ensuring that they are satisfied by the reference implementations. We estimate that writing the IS contract required approximately one work day per case study; the remaining time was dedicated to writing the functional ACSL specifications. 7.2
Steering Fluid Level Detection (SFLD) case study
The SFLD (Steering Fluid Level Detection) module diagnoses the steering fluid level in a power steering system for a vehicle. The role of a power steering system is to reduce the manual force needed by drivers to steer the vehicle, for which
16
J. Amilon et al.
steering fluid is a critical component. SGMM should monitor the steering fluid level and, if it drops below a certain threshold, a warning should be emitted to the driver. SFLD is safety-critical since the loss of power steering means that the vehicle becomes difficult to operate. The requirements document for SLFD consists of a summary of the intended functionality of the module, a control flow diagram, and seven requirements expressed in a mixture of natural language and pseudo-code. An important component described in the requirements document is a delay filter, similar to our simplified example in Figure 4a. The description also details how the delay filter should be initialized upon vehicle startup. Table 5 shows the size of the implementation and the contracts for SFLD. Entry-point ACSL spec. refers to the ACSL specifications Table 5: Size in LOC for SFLD. for the entry-point functions in SFLD, and external ACSL spec. to the ACSL specifica- C implementation 88 tions for the external functions defined in the Entry-point ACSL spec. 127 IS contract. In Figure 7, we show an obfus- External ACSL spec. 109 cated excerpt of the IS contract for SFLD. The IS contract 35 IS contract for SFLD specifies that the module shall consist of two entry-point functions, Sfld_create and Sfld_10ms. Sfld_create is assumed to be called at vehicle startup and Sfld_10ms is assumed to be called every 10 ms by a scheduler, hence, Sfld_create < Sfld_10ms. The IS contract also specifies 12 external functions, together with four external call order constraints. The external functions allow the module to interact with RTDB, and the order constraints ensure that the RTDB variables are initialized before they are read from or written to. The reference implementation of SFLD consists of the two entry-point functions from the IS contract, and no local functions. Sfld_create initializes the RTDB variables used by SFLD with calls to, e.g., Rtdb_createBs. Sfld_10ms first reads the value of the oil-level sensor from RTDB and then implements the delay filter described in the requirements by incrementing or decrementing a timer that is stored in RTDB. If the timer reaches an upper threshold value, an oil-level warning is activated on the vehicle dashboard. If the timer reaches 0, the warning is deactivated. The implementation contains 17 call sites with calls to external modules, and uses one global variable with a static storage specifier, which serves as a Boolean flag to indicate if this is the first time the function is called since the last vehicle startup. 7.3
Safe Gearbox Maneuvering Module (SGMM) case study
The SGMM (Safe Gearbox Maneuvering Module) is a controller for a gearbox in an electric vehicle. Specifically, it controls two magnetic valves, the high and the low valve, which in turn control the gearbox. When there is a risk for overspeed of the vehicle engine, SGMM should block the magnetic valves to ensure that the gearbox is not activated. SGMM is safety-critical since overspeeding of the engine may lead to fatal incidents. The requirements document for SGMM consists of a summary of the functionality of the module in natural language, a control
Contract Based Verification of Non-functional Requirements
17
module sgmm { e nt ry _ fu nc t io n s : { void Sgmm_10ms ( void ) } exte rnal_c alls : { aux . h : { int Au x_ e nt er S af e SW ( void ) , void A ux_exi tSafeS W ( void ) , ... } , rtdb2 . h : { tB R t d b _ L o w V a l v e _ r e a d ( void ) , tB R t d b _ H i g h V a l v e _ r e a d ( void ) , void R t d b _ L o w V a l v e _ w r i t e ( const tB val ) , void R t d b _ H i g h V a l v e _ w r i t e ( const tB val ) , ... }, util . h : { void U t i l _ r e g i s t e r E v e n t ( void * moduleName , tU16 __LINE__ )} } external_call_order : { Aux_enterSafetySW < Aux_exitSafetySW } }
Fig. 8: Excerpt of the IS contract for SGMM.
flow diagram, and five requirements expressed as pseudo-code. The control flow diagram and the five requirements both express the conditions under which the module should ensure that the magnetic valves are blocked. Table 6 shows the size of the implementation and the contracts. Figure 8 shows an obfuscated excerpt of the IS contract. The IS Table 6: Size in LOC for SGMM. contract for SGMM specifies 13 external functions and one external call order constraint. C implementation 138 There is no initialization function in SGMM, Entry-point ACSL spec. 124 since it uses a version of RTDB where ini- External ACSL spec. 58 tialization is not delegated to the applica- IS contract 28 tion modules. Aside from reading and writing to RTDB, the implementation calls functions that control memory-safety aspects in the ECU. For example, the call to Auxc_enterSafetySW activates runtime memory-safety checks in the ECU. The implementation of SGMM consists of the single entry-point function Sgmm_10ms, expected to be called repeatedly by the scheduler every 10 ms. The implementation first reads input values from RTDB, and then checks if any of the conditions for blocking the valves are satisfied. If so, it blocks the valves by writing to the corresponding RTDB output variables. Sgmm_10ms is implemented using several local functions and 17 calls to the external modules. There are no global variables in the implementation. 7.4
Verification results
This section reports the results for the case studies using the toolchain described in Section 6, which we implemented in Python. Compilation with GCC is performed first, followed by deductive verification with Frama-C (Wp with the Wp-rte option). Further static analysis is carried out using Cppcheck with the MISRA-C:2012 addon, and non-functional rules are checked using VerNFR. Each critic reports its result to a shared aggregation step, which produces a unified report and determines the final verification outcome.
18
J. Amilon et al.
Table 7: Verification results for the SGMM and SFLD reference implementations. For Frama-C, we report the proven proof obligations over the total obligations. For Cppcheck, “req.” and “adv.” denote required and advisory MISRA-C violations, respectively. Reported times are CPU time measured using the unix time command as the sum of user and system time. SGMM Critic
Result
Compile Frama-C (Wp) VerNFR Cppcheck using MISRA
✓ ✓ (86/86) ✓ × (6 req.)
Total
SFLD
Time [s] 0.4 14.8 13.2 58.9 87.3
Result ✓ ✓ (80/80) ✓ × (4 req., 2 adv.)
Time [s] 0.3 8.4 12.0 20.1 40.7
Table 7 summarizes the verification results for the reference implementations of the two case studies. The first column lists the critics applied to the module, while the remaining columns are grouped by case study, reporting for SGMM and SFLD whether verification succeeded and the corresponding analysis time. All experiments were performed in a virtualized Linux environment (WSL2) running on a machine with an Intel Core i7-1365U CPU (6 cores, 12 threads) and 16 GB RAM. As shown in the table, both SGMM and SFLD compile successfully using GCC, all proof obligations generated by Frama-C Wp are proven, and no violations are reported by VerNFR. For SFLD, no MISRA-C violations are reported when restricting the analysis to the module implementation itself, i.e., when we exclude included header files. For SGMM, however, Cppcheck reports six required MISRA-C violations in the module implementation itself. More specifically, two violations concern assignments between expressions of incompatible or narrower essential type categories (Rule 10.3), and four violations concern missing compound statements as bodies of selection statements (Rule 15.6). When considering the full compilation unit, additional Cppcheck violations are also reported in included external library headers. For SFLD, these consist of four required and two advisory violations, primarily related to type consistency in expressions and scope-related recommendations. We discuss Cppcheck violations more generally in Section 8. The analysis times vary by an order of magnitude between the critics. Cppcheck is the most expensive critic in both case studies, with CPU times on the order of tens of seconds. Frama-C is one order of magnitude faster, while the VerNFR analysis is the least expensive, with times of only a few seconds. This ordering is consistent for both SGMM and SFLD.
Contract Based Verification of Non-functional Requirements
7.5
19
Preliminary LLM experiments
So far, our case studies have considered implementations by human agents. However, the proposed toolchain is agnostic to the origin of the code and also applies to implementations generated by LLM-based agents. To explore this, we conducted preliminary experiments using two models available through AWS Bedrock [3], namely Claude Sonnet 4.6 [6] and Llama 3 Instruct 8B [2]. In these experiments, we prompted the models with the natural-language specification, the interface specification, the required header files, and the relevant type definitions. We also imposed explicit constraints on the expected output format. In particular, the models were instructed to generate exactly one .c file and one .h file, and implement the entry-point functions from the interface specification. The prompt did not include the non-functional rules defined in Section 3; instead, it provided information on the syntax and the semantics of the IS contracts. For each generated pair of source files, we compiled them with GCC since, as discussed in Section 6, we treat successful compilation with GCC as a baseline for the other critics. If compilation succeeded, we continued with functional verification with Wp, followed by the non-functional verification with VerNFR for the rules in Section 3 and Cppcheck for MISRA-C. For the smaller model (Llama 3 Instruct 8B), we observed that the generated outputs frequently failed to follow the required format. In particular, the model often did not produce both a .c file and a .h file as specified, which led to compilation failures. In contrast, the larger model (Claude Sonnet 4.6) more consistently produced outputs in the requested format. Across our experiments, 32 generated implementations compiled successfully. For all of these, VerNFR and Cppcheck reported no violations. For all generated implementations of SGMM, the functional verification with Wp also succeeded. For SFLD, however, Wp discharged at most 82 out of 84 proof obligations within the default timeout setting of 2 seconds per proof obligation. We therefore classified all generated version of SFLD as not verified. Overall, the results indicate that achieving non-functional correctness is feasible whenever the generated source code files compile, while achieving functional correctness remains sensitive to, e.g., the complexity of the module and the completeness of the specifications. We also conducted experiments in which we omitted the IS contract from the input. In several cases, the models generated code that still adhered to the intended interface. In these cases, only the IS contract was omitted, but the external header files still provide context to the LLM. We suspect that these header files give enough context to the LLM to properly assess which RTDB functions to use, as the function names describe the intended uses. However, the IS contract is still necessary to formally verify that the interface of the generated code behaves as expected.
20
8
J. Amilon et al.
Discussion
In this paper, we consider functional verification of safety-critical code a baseline on which to improve by specifying and verifying additional properties. Yet, simply reaching this baseline using ACSL and Frama-C for our case study modules took considerable effort, both in absolute terms and in comparison to writing and verifying IS contracts. For the SFLD case study in particular, we struggled to write the ACSL specifications due to the poor quality of the natural language requirements. While we were able to study the reference implementation to resolve ambiguities and incompleteness, LLM agents may not have access to such implementations when prompted to generate modules. High quality requirements, both in natural and formal languages, are thus likely to be important in workflows similar to ours when relying on LLM agents. While our case study module reference implementations are not classified as verified due to violations reported by Cppcheck, these violations do not necessarily indicate incorrect or unsafe behavior. Instead, we believe they reflect a mismatch between the standard MISRA-C rules enforced by Cppcheck and the project and company-specific adaptations of these rules used in Scania production code. In practice, such adaptations allow certain constructs that are disallowed or discouraged by the standard MISRA-C guidelines. As a result, the violations should be interpreted as deviations from strict MISRA-C compliance rather than violations of functional correctness or module-level requirements.
9
Related Work
Many approaches and tools permit specification and verification of non-functional properties. For C, the ACSL language offers specification of memory safety and termination, which can be verified by Wp [8]. The MetACSL plugin [35] of Frama-C extends ACSL with a language for meta-properties, including relational properties such as function equivalence. The EVA plugin [11], based on abstract interpretation, can be used to bound domains for variables. None of the existing plugins, however, could be tailored to verify our rules in Section 3, and thus VerNFR complements the existing Frama-C plugin collection. Several existing formal specification languages consider control flow, for example CVPP [18], for Java and the Frama-C aoraï plugin [41] for C programs. Both CVPP and aoraï use an automata language to specify allowed sequences of function calls and then verify that all executions of a program adhere to the automata. Another approach by Soleimanifard et al. [39] uses temporal logic annotations in programs to verify procedure-level control flow, which allows verification of, e.g., certain interleaving of function calls. Compared to these approaches, the control flow side of our contract language is simpler and aimed at practical use in verification of embedded C code, but could straightforwardly be extended to support expressiveness equal to a class of finite automata. Regarding contract languages for non-functional requirements more generally, Loques et al. [28] develop a contract-based framework for developing modular software
Contract Based Verification of Non-functional Requirements
21
that adheres to non-functional requirements, and Lopez et al. [27] extend a contract language with properties such as execution time and memory consumption. In contrast, our work is specific to module interface requirements of embedded C code. Recent work integrates LLMs with formal verification or symbolic reasoning tools to assess correctness properties of generated programs [34,32,38]. For C code, Sevenhuijsen et al. [36] present a workflow in which an LLM generates candidate implementations that are iteratively refined using feedback from the compiler and verification tool. Patil et al. [34] and Sevenhuijsen et al. [37] evaluate the generation of automotive embedded C code from natural language and ACSL specifications, showing that compilable and partially or fully verifiable implementations can be obtained. While these approaches demonstrate the feasibility of combining LLM generation with verification, they target functional properties and do not explicitly address non-functional requirements such as control-flow restrictions, interface conformance, and inter-module interaction. Regarding non-functional properties of LLM-generated code, Sun et al. [42] study high-level non-functional quality characteristics, while Lin et al. [26] show that enforcing non-functional properties may impact functional correctness.
10
Conclusion
We presented principles and rules for capturing non-functional requirements in embedded systems C code, operationalized in a checker built on Frama-C. Use of our checker is complementary to functional verification of ACSL properties and MISRA-C conformance checking. The checker relies on a module-level contract language that extends a bridge from ACSL function contracts towards system level contracts, e.g., expressing end-to-end safety requirements of trucks. Heavyweight methods such as interactive theorem proving can, in principle, support trustworthy modular reasoning about system level properties, including non-functional ones, for embedded systems [10]. However, they remain far from engineering practice and industry productivity expectations. By considering more lightweight methods and languages for non-functional verification, we believe safety benefits and LLM productivity increases are more likely to accrue. Our case studies suggest that functional specification and verification remains a bottleneck in achieving trustworthy safety-critical software written in C, but can be used to pivot towards practical system level verification of a wider range of properties via the module abstraction. Acknowledgments. We thank Gustav Ung and Minal Suresh Patil for discussions on this work. The work was supported by Vinnova through the FormAI project and by Digital Futures at KTH through the Open Sandbox project.
References 1. Abella, J., Hernandez, C., Quiñones, E., Cazorla, F.J., Conmy, P.R., Azkarateaskasua, M., Perez, J., Mezzetti, E., Vardanega, T.: WCET analysis methods: Pit-
22
J. Amilon et al.
falls and challenges on their trustworthiness. In: International Symposium on Industrial Embedded Systems. pp. 1–10 (2015). https://doi.org/10.1109/SIES.2015. 7185039 2. AI@Meta: The llama 3 herd of models. arXiv preprint arXiv:2407.21783 (2024), https://arxiv.org/abs/2407.21783 3. Amazon Web Services: Amazon bedrock documentation. https://docs.aws.amazon. com/bedrock/ (2026), accessed: 2026-04-16 4. Amilon, J.: Vernfr for isola 2026 (Apr 2026). https://doi.org/10.5281/zenodo. 19706522, https://doi.org/10.5281/zenodo.19706522 5. Amilon, J., Gurov, D., Lidström, C., Nyberg, M., Ung, G., Wingbrant, O.: AutoDeduct: A tool for automated deductive verification of C code (2025), https: //arxiv.org/abs/2501.10889 6. Anthropic: Claude sonnet 4.6 system card. https://anthropic.com/ claude-sonnet-4-6-system-card (Feb 2026), accessed: 2026-04-16 7. Baudin, P., Bobot, F., Bühler, D., Correnson, L., Kirchner, F., Kosmatov, N., Maroneze, A., Perrelle, V., Prevosto, V., Signoles, J., Williams, N.: The dogged pursuit of bug-free C programs: the Frama-C software analysis platform. Commun. ACM 64(8), 56–68 (Jul 2021). https://doi.org/10.1145/3470569 8. Baudin, P., Bobot, F., Correnson, L., Dargaye, Z., Blanchard, A.: FramaC WP Plug-in Manual. CEA-List (2025), https://www.frama-c.com/download/ frama-c-wp-manual.pdf, Frama-C 32.0 (Germanium) 9. Baudin, P., Filliâtre, J.C., Marché, C., Monate, B., Moy, Y., Prevosto, V.: ACSL: ANSI/ISO C Specification Language, https://frama-c.com/download/acsl.pdf 10. Beringer, L.: Verified software units. In: Programming Languages and Systems. pp. 118–147. Springer International Publishing, Cham (2021). https://doi.org/10. 1007/978-3-030-72019-3_5 11. Bühler, D., Cuoq, P., Yakobowski, B., Lemerre, M., Maroneze, A., Perrelle, V., Prevosto, V.: Frama-C Eva Plug-in Manual. CEA-List (2025), https://www.frama-c. com/download/frama-c-eva-manual.pdf, frama-C 32.0 (Germanium) 12. Carbonneaux, Q., Hoffmann, J., Ramananandro, T., Shao, Z.: End-to-end verification of stack-space bounds for C programs. In: Proceedings of the 35th ACM SIGPLAN Conference on Programming Language Design and Implementation. pp. 270–281. PLDI ’14, Association for Computing Machinery, New York, NY, USA (2014). https://doi.org/10.1145/2594291.2594301 13. Conchon, S., Coquereau, A., Iguernlala, M., Mebsout, A.: Alt-Ergo 2.2 (Jul 2018), https://inria.hal.science/hal-01960203 14. Frama-C developers: ACSL importer (2026), https://www.frama-c.com/ fc-plugins/acsl-importer.html 15. GNU Project: Header files (2026), https://gcc.gnu.org/onlinedocs/cpp/ Header-Files.html, GCC C Preprocessor Manual, accessed 2026-03-25 16. Gurov, D., Lidström, C., Nyberg, M., Westman, J.: Deductive functional verification of safety-critical embedded C-code: An experience report. In: Petrucci, L., Seceleanu, C., Cavalcanti, A. (eds.) Critical Systems: Formal Methods and Automated Verification. pp. 3–18. Springer International Publishing, Cham (2017). https://doi.org/10.1007/978-3-319-67113-0_1 17. Holzmann, G.J.: The power of 10: rules for developing safety-critical code. Computer 39(6), 95–99 (2006). https://doi.org/10.1109/MC.2006.212 18. Huisman, M., Gurov, D.: CVPP: A tool set for compositional verification of control–flow safety properties. In: Beckert, B., Marché, C. (eds.) Formal Verification of Object-Oriented Software. pp. 107–121. Springer Berlin Heidelberg, Berlin, Heidelberg (2011). https://doi.org/10.1007/978-3-642-18070-5_8
Contract Based Verification of Non-functional Requirements
23
19. ISO: Programming languages—C (1999), ISO/IEC 9899:1999 20. ISO: Road vehicles controller area network (CAN) (2015), ISO 11898-1:2015 21. ISO: ISO26262: Road vehicles - functional safety 2nd ed. (2018) 22. Kambhampati, S., Valmeekam, K., Guan, L., Verma, M., Stechly, K., Bhambri, S., Saldyt, L., Murthy, A.: Position: LLMs can’t plan, but can help planning in LLMmodulo frameworks. In: International Conference on Machine Learning. ICML’24, JMLR.org (2024). https://doi.org/10.5555/3692070.3692991 23. Kirchner, F., Kosmatov, N., Prevosto, V., Signoles, J., Yakobowski, B.: Frama-C: A software analysis perspective. Formal Aspects of Computing 27, 573–609 (2015). https://doi.org/10.1007/s00165-014-0326-7 24. Leroy, X., Doligez, D., Frisch, A., Garrigue, J., Rémy, D., Vouillon, J.: The OCaml System: Documentation and User’s Manual. Inria (2018), https://ocaml. org/manual/ 25. Lidström, C., Gurov, D.: Contract based embedded software design. In: David, C., Sun, M. (eds.) Theoretical Aspects of Software Engineering. pp. 77–94. Springer Nature Switzerland, Cham (2023). https://doi.org/10.1007/978-3-031-35257-7_5 26. Lin, F., Kim, D.J., Li, Z., Yang, J., Tse-Hsun, Chen: RobuNFR: Evaluating the robustness of large language models on non-functional requirements aware code generation (2025), https://arxiv.org/abs/2503.22851 27. Lopez Pombo, C.G., Melgratti, H., Martinez-Suñé, A.E., Anabia, D.S., Tuosto, E.: Behavioural, functional, and non-functional contracts for dynamic selection of services. In: Di Giusto, C., Ravara, A. (eds.) Coordination Models and Languages. pp. 153–174. Springer Nature Switzerland, Cham (2025). https://doi.org/10.1007/ 978-3-031-95589-1_8 28. Loques, O., Sztajnberg, A., Curty, R., Ansaloni, S.: A contract-based approach to describe and deploy non-functional adaptations in software architectures. J. Braz. Comput. Soc. 10(1), 5–18 (2004). https://doi.org/10.1007/BF03192350 29. Marjamäki, D., contributors: Cppcheck: A tool for static C/C++ code analysis (2026), https://cppcheck.sourceforge.io/ 30. MIRA Ltd: MISRA-C:2004 Guidelines for the use of the C language in critical systems. Tech. rep., Motor Industry Software Reliability Association (Oct 2004), https://misra.org.uk/misra-c 31. de Moura, L., Bjørner, N.: Z3: An efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) Tools and Algorithms for the Construction and Analysis of Systems. pp. 337–340. Springer Berlin Heidelberg, Berlin, Heidelberg (2008). https://doi.org/10.1007/978-3-540-78800-3_24 32. Mukherjee, P., Delaware, B.: Towards Automated Verification of LLMSynthesized C Programs (Oct 2024). https://doi.org/10.48550/arXiv.2410.14835, arXiv:2410.14835 33. Parnas, D.L., Clements, P.C., Weiss, D.M.: Enhancing reusability with information hiding. In: Proceedings of the ITT Workshop on Reusability in Programming. pp. 7–9 (1983). https://doi.org/10.1145/73103.73109 34. Patil, M.S., Ung, G., Nyberg, M.: Towards Specification-Driven LLM-Based Generation of Embedded Automotive Software. In: Steffen, B. (ed.) Bridging the Gap Between AI and Reality - Second International Conference, AISoLA 2024, Crete, Greece, October 30 - November 3, 2024, Proceedings. Lecture Notes in Computer Science, vol. 15217, pp. 125–144. Springer (2024). https://doi.org/10.1007/ 978-3-031-75434-0_9 35. Robles, V., Kosmatov, N., Prevosto, V., Rilling, L., Le Gall, P.: MetAcsl: Specification and verification of high-level properties. In: Tools and Algorithms for the
24
J. Amilon et al.
Construction and Analysis of Systems. pp. 358–364. Springer International Publishing, Cham (2019). https://doi.org/10.1007/978-3-030-17462-0_22 36. Sevenhuijsen, M., Etemadi, K., Nyberg, M.: VeCoGen: Automating Generation of Formally Verified C Code with Large Language Models (2024), https://arxiv.org/ abs/2411.19275 37. Sevenhuijsen, M., Patil, M.S., Nyberg, M., Ung, G.: Generating safety-critical automotive C-programs using LLMs with formal verification. In: H. Gilpin, L., Giunchiglia, E., Hitzler, P., van Krieken, E. (eds.) International Conference on Neurosymbolic Learning and Reasoning. Proceedings of Machine Learning Research, vol. 284, pp. 353–378. PMLR (08–10 Sep 2025), https://proceedings.mlr.press/ v284/sevenhuijsen25a.html 38. Slama, F., Lemire, D.: Comparative Analysis of Loop-Free Function Evaluation Using ChatGPT and Copilot with C Bounded Model Checking. In: 2024 2nd International Conference on Foundation and Large Language Models (FLLM). pp. 58–65 (2024). https://doi.org/10.1109/FLLM63129.2024.10852461 39. Soleimanifard, S., Gurov, D., Huisman, M.: Procedure-modular specification and verification of temporal safety properties. Software & Systems Modeling 14, 83–100 (2015). https://doi.org/10.1007/s10270-013-0321-0 40. Stallman, R.M., Community, G.D.: Using the GNU Compiler Collection (GCC). Free Software Foundation (2026), https://gcc.gnu.org/onlinedocs/gcc/, GCC Version 16.0.1 41. Stouls, N.: Aorai plug-in tutorial, https://frama-c.com/download/aorai/ aorai-manual.pdf 42. Sun, X., Ståhl, D., Sandahl, K., Kessler, C.: Quality assurance of LLM-generated code: Addressing non-functional quality characteristics (2025), https://arxiv.org/ abs/2511.10271 43. Ung, G., Amilon, J., Gurov, D., Lidström, C., Nyberg, M., Palmskog, K.: Post-hoc formal verification of automotive software with informal requirements: An experience report. In: International Requirements Engineering Conference. pp. 287–298 (2024). https://doi.org/10.1109/RE59067.2024.00035