論文の概要: Checking the HAL Interface Specification Continuously, Right from the Start

• arxiv url: http://arxiv.org/abs/2512.16897v1
• Date: Thu, 18 Dec 2025 18:55:17 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-12-19 18:10:32.235991
• Title: Checking the HAL Interface Specification Continuously, Right from the Start
• Title（参考訳）: HALインターフェースの仕様を最初から継続的にチェックする
• Authors: Manuel Bentele, Onur Altinordu, Jan Körner, Andreas Podelski, Axel Sikora,
• Abstract要約: ステップ間の正式な接続なしに,複数のイテレーションで組込みアプリケーションを開発します。 このアプローチのアイデアは、ソフトウェアモデルチェックの特定の機能を活用することです。 このアプローチに従って、チェックは各ステップ、特に最終アプリケーションプログラムで成功します。
• 参考スコア（独自算出の注目度）: 1.0439136407307046
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: The correct use of a Hardware Abstraction Layer (HAL) interface in embedded applications is crucial to prevent malfunctions, crashes, or even hardware damage. Software model checking has been successfully applied to check interface specifications in application programs, but its employment in industrial practice is hindered by its unpredictability (whether it succeeds for a given application program or not). In this paper, we present a novel approach to address this problem by checking the HAL interface specification continuously and right from the start of the development. I.e., we develop an embedded application in several iterations without a formal connection between the steps. The steps start from a program skeleton which does nothing but calling HAL functions. Actual functionality is added consecutively. The HAL interface specification is checked in each step of the sequence. The idea of the approach is to exploit a specific feature of software model checking: Its attempt to compute exactly the abstraction that is needed for the check to succeed may carry over from one step to the next, even if there is no formal connection between the steps. The experience from a preliminary experimental evaluation of our approach in the development of embedded applications is very promising. Following our approach, the check succeeds in each step and in particular in the final application program.
• Abstract（参考訳）: 組み込みアプリケーションにおけるハードウェア抽象化層(HAL)インターフェースの正しい使用は、故障やクラッシュ、さらにはハードウェアの損傷を防ぐために不可欠である。 ソフトウェアモデルチェックは、アプリケーションプログラムのインターフェース仕様のチェックにうまく適用されているが、産業におけるその雇用はその予測不可能さ(特定のアプリケーションプログラムで成功するかどうかに関わらず)によって妨げられている。 本稿では,HALインタフェースの仕様を開発開始時から継続的に,かつ右にチェックすることで,この問題に対処する新しいアプローチを提案する。 すなわち、ステップ間の正式な接続なしに、複数のイテレーションで組込みアプリケーションを開発します。 ステップは、HAL関数を呼び出すだけで何もしないプログラムスケルトンから始まる。 実際の機能は連続して追加される。 HALインターフェース仕様はシーケンスの各ステップでチェックされる。 成功するためのチェックに必要な抽象化を正確に計算しようとする試みは、たとえステップの間に正式な接続がなくても、あるステップから次のステップへと引き継がれる可能性がある。 組込みアプリケーションの開発における我々のアプローチの予備的な実験的評価から得られた経験は、非常に有望である。 このアプローチに従って、チェックは各ステップ、特に最終アプリケーションプログラムで成功します。

関連論文リスト

• Relevant HAL Interface Requirements for Embedded Systems [1.1199585259018456]
  ハードウェア抽象化層(HAL)の適切な使用は、システム障害につながる可能性がある。 本稿では,システム障害に関する報告から,証明可能な要件を抽出する手法を提案する。
  論文  参考訳（メタデータ） (2025-12-16T15:47:26Z)
• A Case Study on Model Checking and Runtime Verification for Awkernel [0.7199733380797578]
  人間が手動で同時動作をレビューしたり、可能なすべての実行をカバーしたテストケースを書くことは難しい。 本稿では,スケジューラなどの並列ソフトウェアの開発手法を提案する。
  論文  参考訳（メタデータ） (2025-03-12T11:27:45Z)
• Simulated Interactive Debugging [7.3742419367796535]
  我々は,学生がデバッグプロセスに沿って対話的に指導する「シミュレート・インタラクティブ」という手法を提案する。 このガイダンスは、生徒がソリューションを修復し、適切な学習経験を持つことを奨励することを目的としている。 従来のフォールトローカライズ手法と大規模言語モデルを用いた実装を開発した。
  論文  参考訳（メタデータ） (2025-01-16T17:47:18Z)
• Go-Oracle: Automated Test Oracle for Go Concurrency Bugs [6.773048267569272]
  Go言語では、バグが大きな問題となっている。 我々の研究は、Goプログラムのテストオラクル問題に対処し、テスト実行をパスまたはフェールとして自動的に分類することを目指している。 ネイティブなGo実行トレーサを使用して、包括的な実行イベントをキャプチャします。 トランスフォーマーベースのニューラルネットワークをトレーニングする前に、これらのトレースを前処理してエンコードして、トレースをパスまたはフェールのいずれかとして効果的に分類します。
  論文  参考訳（メタデータ） (2024-12-11T03:07:56Z)
• ExploraCoder: Advancing code generation for multiple unseen APIs via planning and chained exploration [70.26807758443675]
  ExploraCoderはトレーニング不要のフレームワークで、大規模な言語モデルにコードソリューションで見えないAPIを呼び出す権限を与える。 実験の結果、ExploreaCoderは、事前のAPI知識に欠けるモデルのパフォーマンスを大幅に改善することが示された。
  論文  参考訳（メタデータ） (2024-12-06T19:00:15Z)
• Unsupervised Continual Anomaly Detection with Contrastively-learned Prompt [80.43623986759691]
  UCADと呼ばれる新しい非教師付き連続異常検出フレームワークを提案する。 このフレームワークは、対照的に学習したプロンプトを通じて、UDAに継続的な学習能力を持たせる。 我々は総合的な実験を行い、教師なし連続異常検出とセグメンテーションのベンチマークを設定した。
  論文  参考訳（メタデータ） (2024-01-02T03:37:11Z)
• ChatDev: Communicative Agents for Software Development [84.90400377131962]
  ChatDevはチャットを利用したソフトウェア開発フレームワークで、特別なエージェントがコミュニケーション方法についてガイドされる。 これらのエージェントは、統一された言語ベースのコミュニケーションを通じて、設計、コーディング、テストフェーズに積極的に貢献する。
  論文  参考訳（メタデータ） (2023-07-16T02:11:34Z)
• Semi-Oblivious Chase Termination for Linear Existential Rules: An Experimental Study [5.936402320555635]
  チェイス手順は、制約のある推論を可能にする、データベースの基本的なアルゴリズムツールである。 データベースと一連の制約を入力として取り、制約によって決定されたデータベースを反復的に完了します。 しかし、重要な課題は、それが終了しないかもしれないという事実であり、それが与えられたデータベースと一連の制約を終了するかどうかをチェックする問題に繋がる。
  論文  参考訳（メタデータ） (2023-03-22T18:21:01Z)

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

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