論文の概要: Formal Runtime Error Detection During Development in the Automotive Industry

• arxiv url: http://arxiv.org/abs/2310.16468v1
• Date: Wed, 25 Oct 2023 08:44:52 GMT
• ステータス: 処理完了
• システム内更新日: 2023-10-26 15:44:29.811913
• Title: Formal Runtime Error Detection During Development in the Automotive Industry
• Title（参考訳）: 自動車産業開発における形式的エラー検出
• Authors: Jesko Hecking-Harbusch, Jochen Quante, Maximilian Schlund
• Abstract要約: 安全関連ソフトウェアでは,音声静的プログラム解析を用いて実行時エラーの欠如を証明することが推奨されている。 この分析は、開発者が長時間実行し、多くの誤報を発生させるため、しばしば重荷と見なされる。 本稿では,自動推論契約がモジュールレベルの解析にどのようにコンテキストを追加するかを示す。
• 参考スコア（独自算出の注目度）: 0.1611401281366893
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Modern automotive software is highly complex and consists of millions lines of code. For safety-relevant automotive software, it is recommended to use sound static program analysis to prove the absence of runtime errors. However, the analysis is often perceived as burdensome by developers because it runs for a long time and produces many false alarms. If the analysis is performed on the integrated software system, there is a scalability problem, and the analysis is only possible at a late stage of development. If the analysis is performed on individual modules instead, this is possible at an early stage of development, but the usage context of modules is missing, which leads to too many false alarms. In this case study, we present how automatically inferred contracts add context to module-level analysis. Leveraging these contracts with an off-the-shelf tool for abstract interpretation makes module-level analysis more precise and more scalable. We evaluate this framework quantitatively on industrial case studies from different automotive domains. Additionally, we report on our qualitative experience for the verification of large-scale embedded software projects.
• Abstract（参考訳）: 現代の自動車ソフトウェアは非常に複雑で、数百万行のコードで構成される。 安全関連ソフトウェアでは,音声静的プログラム解析を用いて実行時エラーの欠如を証明することが推奨されている。 しかし、この分析は開発者が長時間実行し、多くの誤報を発生させるため、しばしば負担になると見なされる。 統合ソフトウェアシステム上で解析を行う場合、スケーラビリティの問題が発生し、その解析は開発後期にのみ可能である。 分析が個々のモジュール上で実行される場合、これは開発の初期段階で可能であるが、モジュールの使用状況が欠落しているため、誤報が多すぎる。 本稿では,自動推論契約がモジュールレベルの解析にどのようにコンテキストを追加するかを示す。 これらのコントラクトを抽象的な解釈のための既製のツールで活用することで、モジュールレベルの分析をより正確かつスケーラブルにすることができる。 我々は,この枠組みを自動車分野の異なる産業事例から定量的に評価する。 さらに,大規模組み込みソフトウェアプロジェクトの検証における質的な経験について報告する。

関連論文リスト

• Leveraging Slither and Interval Analysis to build a Static Analysis Tool [0.0]
  本稿では,現在最先端の分析ツールで検出されていない,あるいは完全に検出されていない欠陥の発見に向けた進展について述べる。 我々は,Slither上に構築された動作ソリューションを開発し,各命令の実行時の契約状態を評価する。
  論文  参考訳（メタデータ） (2024-10-31T09:28:09Z)
• Codev-Bench: How Do LLMs Understand Developer-Centric Code Completion? [60.84912551069379]
  Code-Development Benchmark (Codev-Bench)は、細粒度で現実世界、リポジトリレベル、開発者中心の評価フレームワークです。 Codev-Agentは、リポジトリのクローリングを自動化し、実行環境を構築し、既存のユニットテストから動的呼び出しチェーンを抽出し、データ漏洩を避けるために新しいテストサンプルを生成するエージェントベースのシステムである。
  論文  参考訳（メタデータ） (2024-10-02T09:11:10Z)
• Scaling Symbolic Execution to Large Software Systems [0.0]
  シンボル実行は、プログラム検証とバグ検出ソフトウェアの両方で使用される一般的な静的解析手法である。 我々は、Clang Static Analyzerと呼ばれるエラー検出フレームワークと、その周辺に構築されたインフラストラクチャーであるCodeCheckerに焦点を当てた。
  論文  参考訳（メタデータ） (2024-08-04T02:54:58Z)
• Easing Maintenance of Academic Static Analyzers [0.0]
  Mopsaは、音を出すことを目的とした静的分析プラットフォームである。 この記事では、2017年以来のMopsaのメンテナンスを簡素化するために、私たちが作り出したツールとテクニックについて説明する。
  論文  参考訳（メタデータ） (2024-07-17T11:29:21Z)
• Leveraging Large Language Models for Efficient Failure Analysis in Game Development [47.618236610219554]
  本稿では,テストの失敗の原因となるコードの変更を自動的に識別する手法を提案する。 このメソッドは、LLM(Large Language Models)を利用して、エラーメッセージと対応するコード変更を関連付ける。 当社のアプローチは新たに作成したデータセットで71%の精度に達しています。
  論文  参考訳（メタデータ） (2024-06-11T09:21:50Z)
• Customizing Static Analysis using Codesearch [1.7205106391379021]
  様々な静的解析アプリケーションを記述するのによく使われる言語は、Datalogである。 アプリケーションセキュリティと静的分析の専門家のための慣れ親しんだフレームワークを提供すると同時に、開発者がカスタムの静的解析ツールを簡単に構築できるようにすることを目標としています。 我々のアプローチでは,高速ランタイムを持つプログラムのみを含むDatalogの亜種であるStarLangという言語を導入しています。
  論文  参考訳（メタデータ） (2024-04-19T09:50:02Z)
• It Is Time To Steer: A Scalable Framework for Analysis-driven Attack Graph Generation [50.06412862964449]
  アタックグラフ(AG)は、コンピュータネットワークに対するマルチステップ攻撃に対するサイバーリスクアセスメントをサポートする最も適したソリューションである。 現在の解決策は、アルゴリズムの観点から生成問題に対処し、生成が完了した後のみ解析を仮定することである。 本稿では,アナリストがいつでもシステムに問い合わせることのできる新しいワークフローを通じて,従来のAG分析を再考する。
  論文  参考訳（メタデータ） (2023-12-27T10:44:58Z)
• The Hitchhiker's Guide to Program Analysis: A Journey with Large Language Models [18.026567399243]
  大規模言語モデル(LLM)は静的解析に代わる有望な選択肢を提供する。 本稿では,LLM支援静的解析のオープン空間を深く掘り下げる。 LLiftは,静的解析ツールとLLMの両方を併用した,完全に自動化されたフレームワークである。
  論文  参考訳（メタデータ） (2023-08-01T02:57:43Z)
• D2A: A Dataset Built for AI-Based Vulnerability Detection Methods Using Differential Analysis [55.15995704119158]
  静的解析ツールによって報告されたラベル問題に対する差分解析に基づくアプローチであるD2Aを提案する。 D2Aを使用して大きなラベル付きデータセットを生成し、脆弱性識別のためのモデルをトレーニングします。
  論文  参考訳（メタデータ） (2021-02-16T07:46:53Z)
• DirectDebug: Automated Testing and Debugging of Feature Models [55.41644538483948]
  変数モデル(例えば、特徴モデル)は、ソフトウェアアーティファクトの変数と共通性を表現する一般的な方法である。 複雑でしばしば大規模な機能モデルは欠陥になりうる、すなわち、ソフトウェアアーチファクトの期待される変動特性を表現しない。
  論文  参考訳（メタデータ） (2021-02-11T11:22:20Z)
• Self-Supervised Log Parsing [59.04636530383049]
  大規模ソフトウェアシステムは、大量の半構造化ログレコードを生成する。 既存のアプローチは、ログ特化や手動ルール抽出に依存している。 本稿では,自己教師付き学習モデルを用いて解析タスクをマスク言語モデリングとして定式化するNuLogを提案する。
  論文  参考訳（メタデータ） (2020-03-17T19:25:25Z)

関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。

指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。