論文の概要: Contract Based Verification of Non-functional Requirements for Embedded Automotive C Code
- arxiv url: http://arxiv.org/abs/2605.21532v1
- Date: Tue, 19 May 2026 21:12:45 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-05-22 20:14:18.459103
- Title: Contract Based Verification of Non-functional Requirements for Embedded Automotive C Code
- Title（参考訳）: 組込み自動車Cコードの非機能要件の契約ベース検証
- Authors: Jesper Amilon, Merlijn Sevenhuijsen, Mattias Nyberg, Karl Palmskog,
- Abstract要約: 制御フローやデータフローの制限のような非機能要件は、組み込みシステムの安全性にとって重要である。
Cモジュールのためのインタフェース仕様契約言語を提案する。
Scania trucks におけるソフトウェアを用いた安全クリティカル C コードの2つのケーススタディについて報告する。
- 参考スコア（独自算出の注目度）: 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.
- Abstract（参考訳）: コードコントラクトは、組み込みシステムにおけるセーフティクリティカルなソフトウェアの機能要件を特定するための堅牢な方法を提供する。
例えば、ANSI/ISO C Specification Language (ACSL) は、Frama-CフレームワークのWpプラグインによって正式に検証されたCコードの機能的振る舞いを指定できる。
しかし、制御フローやデータフローの制限といった非機能要件は、組み込みシステムの安全性にも重要である。
サブコンストラクタ、ジュニアディベロッパ、あるいは大きな言語モデルによって生成された信頼できないコードは、Wpによって検証できるが、それでも安全でない関数を呼んだり、初期化されていないプログラム変数を使ったりすることができる。
この問題に対処するため,安全クリティカルな組込みシステムにおいて,C言語の非機能要件に関する一般的なルールを構築した。
我々の規則は、MISRA-Cのような一般的なCルールセットと直交しており、モジュールとそのインターフェースによる相互作用を中心にしている。
ルールのチェックを可能にするために,Cモジュールのためのインタフェース仕様契約言語を提案する。
このプラグインはCモジュールとその契約を入力として、制御フローとデータフロー特性をチェックし、許可された関数のみがモジュールによって呼び出されることを保証する。
私たちはチェッカーをツールチェーンに統合し、信頼できないコードに対するモジュール契約とACSL契約の仕様と検証を可能にしました。
Scania trucksでは,モジュール契約とACSL関数契約を非公式なシステム要件に基づいて定義し,ツールチェーンを用いて検証した。
関連論文リスト
- enclawed: A Configurable, Sector-Neutral Hardening Framework for Single-User AI Assistant Gateways [0.0]
Enclawedは、証明不可能なピア信頼、非定型外部接続、署名付きモジュールローディング、タンパー・エビデント監査パスを必要とするデプロイメントをターゲットとする。
フレームワークには2つのフレーバーがある。オープンフレーバーはOpenClawとの互換性を維持しつつ、監査、分類、データロス防止シグナルを出力する。
実装には、セキュリティレビュー、204ケースのテストスイート、継続的インテグレーション対応のGitHub Actionsが伴います。
論文 参考訳（メタデータ） (2026-04-18T05:10:11Z) - ECM Contracts: Contract-Aware, Versioned, and Governable Capability Interfaces for Embodied Agents [14.412476605788482]
エージェントは、実行時にインストール、アップグレード、構成、管理できるモジュール機能にますます依存している。
具体的機能モジュールのためのコントラクトベースのインターフェースモデルであるECM Contractsを提示する。
本稿では,バージョンアウェア互換クラス,非推奨ルール,マイグレーション制約,ポリシーに敏感なアップグレードチェックなど,具体的機能を実現するためのリリース規律を提案する。
論文 参考訳（メタデータ） (2026-04-10T01:52:02Z) - Towards Verifiably Safe Tool Use for LLM Agents [53.55621104327779]
大規模言語モデル(LLM)ベースのAIエージェントは、データソース、API、検索エンジン、コードサンドボックス、さらにはその他のエージェントなどのツールへのアクセスを可能にすることで、機能を拡張する。
LLMは意図しないツールインタラクションを起動し、機密データを漏洩したり、クリティカルレコードを上書きしたりするリスクを発生させる。
モデルベースセーフガードのようなリスクを軽減するための現在のアプローチは、エージェントの信頼性を高めるが、システムの安全性を保証することはできない。
論文 参考訳（メタデータ） (2026-01-12T21:31:38Z) - IFEvalCode: Controlled Code Generation [69.28317223249358]
本稿では,Code LLMの命令追従能力を改善するために,前方および後方制約生成を提案する。
IFEvalCodeは、7つのプログラミング言語の1.6Kテストサンプルからなる多言語ベンチマークである。
論文 参考訳（メタデータ） (2025-07-30T08:08:48Z) - Training Language Models to Generate Quality Code with Program Analysis Feedback [66.0854002147103]
大規模言語モデル(LLM)によるコード生成は、ますます本番環境で採用されているが、コード品質の保証には失敗している。
実運用品質のコードを生成するためにLLMにインセンティブを与える強化学習フレームワークであるREALを提案する。
論文 参考訳（メタデータ） (2025-05-28T17:57:47Z) - C*: Unifying Programming and Verification in C [15.531046191957529]
C* は C プログラミングのための言語設計の証明である。
プログラマが実装コードと並行して証明コードブロックを埋め込むことで、リアルタイムの検証を可能にする。
C* は C を共通言語として使用することで実装と証明コード開発を統合する。
論文 参考訳（メタデータ） (2025-04-03T03:22:22Z) - AutoDeduct: A Tool for Automated Deductive Verification of C Code [0.3518504468878697]
私たちはFrama-Cフレームワーク上に構築されたAutoDeductツールチェーンを紹介します。
Cプログラムの関数のコントラクトを自動的に推論するテクニックの組み合わせを実装している。
AutoDeductの現在のリリースは、最初のパブリックプロトタイプである。
論文 参考訳（メタデータ） (2025-01-18T22:00:43Z) - HasTEE+ : Confidential Cloud Computing and Analytics with Haskell [50.994023665559496]
信頼性コンピューティングは、Trusted Execution Environments(TEEs)と呼ばれる特別なハードウェア隔離ユニットを使用して、コテナントクラウドデプロイメントにおける機密コードとデータの保護を可能にする。
低レベルのC/C++ベースのツールチェーンを提供するTEEは、固有のメモリ安全性の脆弱性の影響を受けやすく、明示的で暗黙的な情報フローのリークを監視するための言語構造が欠如している。
私たちは、Haskellに埋め込まれたドメイン固有言語(cla)であるHasTEE+を使って、上記の問題に対処します。
論文 参考訳（メタデータ） (2024-01-17T00:56:23Z) - Value Functions are Control Barrier Functions: Verification of Safe
Policies using Control Theory [46.85103495283037]
本稿では,制御理論から学習値関数への検証手法の適用方法を提案する。
我々は値関数と制御障壁関数の間の関係を確立する原定理を定式化する。
我々の研究は、RLベースの制御システムの汎用的でスケーラブルで検証可能な設計のための公式なフレームワークに向けた重要な一歩である。
論文 参考訳（メタデータ） (2023-06-06T21:41:31Z) - A Compositional Approach to Verifying Modular Robotic Systems [1.385411134620987]
本稿では,ロボットオペレーティング・システム(ROS)を用いたロボットシステムにおけるノードの特定のための構成的アプローチについて述べる。
我々は,これらのノードレベルの契約の構成を容易にする推論ルールを導入し,システムレベルの特性を導出する。
また、ノードのFOL仕様をキャプチャし、この契約を実装にリンクする新しいDomain-Specific Language、ROS Contract Languageも提示します。
論文 参考訳（メタデータ） (2022-08-10T18:01:40Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。