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

• URL: http://arxiv.org/abs/2605.21532v1
• Date: Tue, 19 May 2026 21:12:45 GMT
• Title: Contract Based Verification of Non-functional Requirements for Embedded Automotive C Code
• Abstract summary: Non-functional requirements, such as restrictions on control flow and data flow, are important for embedded systems safety.<n>We propose an interface specification contract language for C modules.<n>We report on two case studies on safety-critical C code using software in Scania trucks.
• Score: 0.5296470528744145
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• 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.

Related papers

• Formal Verification of Agentic Systems over Operational Data [59.98246281888422]
  Agentic systems driven by large language models (LLMs) are increasingly deployed in real-world where they act on persistent operational data.<n>Existing approaches do not provide such system-level guarantees.<n>We study here the verification of agentic systems comprising a single LLM and a tool orchestration harness over relational operational data.
  arXiv  Detail & Related papers  (2026-08-04T13:01:30Z)
• Granite: A Modular Methodology for Foundational Verification of Hardware-Software Leakage Contracts [2.76228438275135]
  Granite is a methodology for modular verification of both functional correctness and nonleakage of RTL processors against ISA contracts.<n>We prove that the cycle-by-cycle timing of a pipelined RISC design--with speculation, precise interrupts, and I/O--is determined solely by observables specified in an ISA leakage contract.
  arXiv  Detail & Related papers  (2026-07-29T21:44:57Z)
• Code as Agent Harness [107.31925305395957]
  In emerging agentic systems, code is no longer only a target output.<n>Code increasingly serves as an operational substrate for agent reasoning, acting, environment modeling, and execution-based verification.<n>This survey provides a unified roadmap toward executable, verifiable, and stateful AI agent systems.
  arXiv  Detail & Related papers  (2026-05-18T17:59:03Z)
• enclawed: A Configurable, Sector-Neutral Hardening Framework for Single-User AI Assistant Gateways [0.0]
  enclawed targets deployments that need attestable peer trust, deny-by-clawed external connectivity, signed-module loading, and tamper-evident audit trail.<n>The framework ships in two flavors: an open flavor that preserves OpenClaw compatibility while still emitting audit, classification, and data-loss-prevention signals.<n>We accompany the implementation with a security review, a 204-case test suite, and GitHub Actions ready for continuous integration.
  arXiv  Detail & Related papers  (2026-04-18T05:10:11Z)
• ECM Contracts: Contract-Aware, Versioned, and Governable Capability Interfaces for Embodied Agents [14.412476605788482]
  Embodied agents increasingly rely on modular capabilities that can be installed, upgraded, composed, and governed at runtime.<n>We present ECM Contracts, a contract-based interface model for embodied capability modules.<n>We propose a release discipline for embodied capabilities, including version-aware compatibility classes, deprecation rules, migration constraints, and policy-sensitive upgrade checks.
  arXiv  Detail & Related papers  (2026-04-10T01:52:02Z)
• Towards Verifiably Safe Tool Use for LLM Agents [53.55621104327779]
  Large language model (LLM)-based AI agents extend capabilities by enabling access to tools such as data sources, APIs, search engines, code sandboxes, and even other agents.<n>LLMs may invoke unintended tool interactions and introduce risks, such as leaking sensitive data or overwriting critical records.<n>Current approaches to mitigate these risks, such as model-based safeguards, enhance agents' reliability but cannot guarantee system safety.
  arXiv  Detail & Related papers  (2026-01-12T21:31:38Z)
• IFEvalCode: Controlled Code Generation [69.28317223249358]
  The paper introduces forward and backward constraints generation to improve the instruction-following capabilities of Code LLMs.<n>The authors present IFEvalCode, a multilingual benchmark comprising 1.6K test samples across seven programming languages.
  arXiv  Detail & Related papers  (2025-07-30T08:08:48Z)
• Training Language Models to Generate Quality Code with Program Analysis Feedback [66.0854002147103]
  Code generation with large language models (LLMs) is increasingly adopted in production but fails to ensure code quality.<n>We propose REAL, a reinforcement learning framework that incentivizes LLMs to generate production-quality code.
  arXiv  Detail & Related papers  (2025-05-28T17:57:47Z)
• C*: Unifying Programming and Verification in C [15.531046191957529]
  C* is a proof-integrated language design for C programming.<n>It enables real-time verification by allowing programmers to embed proof-code blocks alongside implementation code.<n>C* unifies implementation and proof code development by using C as the common language.
  arXiv  Detail & Related papers  (2025-04-03T03:22:22Z)
• AutoDeduct: A Tool for Automated Deductive Verification of C Code [0.3518504468878697]
  We introduce the AutoDeduct toolchain, built on top of the Frama-C framework.<n>It implements a combination of techniques to automatically infer contracts for functions in C programs.<n>The current release of AutoDeduct is the first public prototype.
  arXiv  Detail & Related papers  (2025-01-18T22:00:43Z)
• HasTEE+ : Confidential Cloud Computing and Analytics with Haskell [50.994023665559496]
  Confidential computing enables the protection of confidential code and data in a co-tenanted cloud deployment using specialized hardware isolation units called Trusted Execution Environments (TEEs) TEEs offer low-level C/C++-based toolchains that are susceptible to inherent memory safety vulnerabilities and lack language constructs to monitor explicit and implicit information-flow leaks. We address the above with HasTEE+, a domain-specific language (cla) embedded in Haskell that enables programming TEEs in a high-level language with strong type-safety.
  arXiv  Detail & Related papers  (2024-01-17T00:56:23Z)
• Value Functions are Control Barrier Functions: Verification of Safe Policies using Control Theory [46.85103495283037]
  We propose a new approach to apply verification methods from control theory to learned value functions. We formalize original theorems that establish links between value functions and control barrier functions. Our work marks a significant step towards a formal framework for the general, scalable, and verifiable design of RL-based control systems.
  arXiv  Detail & Related papers  (2023-06-06T21:41:31Z)
• A Compositional Approach to Verifying Modular Robotic Systems [1.385411134620987]
  This paper describes a compositional approach to specifying the nodes in robotic systems built using the Robotic Operating System (ROS) We introduce inference rules that facilitate the composition of these node-level contracts to derive system-level properties. We also present a novel Domain-Specific Language, the ROS Contract Language, which captures a node's FOL specification and links this contract to its implementation.
  arXiv  Detail & Related papers  (2022-08-10T18:01:40Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.