Contract Based Verification of Non-functional Requirements for Embedded Automotive C Code
Fuente:
arXiv
Saved in:
| Main Authors: | , , , |
|---|---|
| Format: | Preprint |
| Published: |
2026
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866911703285891072 |
|---|---|
| author | Amilon, Jesper Sevenhuijsen, Merlijn Nyberg, Mattias Palmskog, Karl |
| author_facet | Amilon, Jesper Sevenhuijsen, Merlijn Nyberg, Mattias Palmskog, Karl |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2605_21532 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | Contract Based Verification of Non-functional Requirements for Embedded Automotive C Code Amilon, Jesper Sevenhuijsen, Merlijn Nyberg, Mattias Palmskog, Karl Programming Languages Software Engineering 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. |
| title | Contract Based Verification of Non-functional Requirements for Embedded Automotive C Code |
| topic | Programming Languages Software Engineering |
| url | https://arxiv.org/abs/2605.21532 |