論文の概要: A Case Study on Model Checking and Runtime Verification for Awkernel

• arxiv url: http://arxiv.org/abs/2503.09282v1
• Date: Wed, 12 Mar 2025 11:27:45 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-03-13 15:39:53.133764
• Title: A Case Study on Model Checking and Runtime Verification for Awkernel
• Title（参考訳）: Awkernelのモデル検査と実行時検証に関する事例研究
• Authors: Akira Hasegawa, Ryuta Kambe, Toshiaki Aoki, Yuuki Takano,
• Abstract要約: 人間が手動で同時動作をレビューしたり、可能なすべての実行をカバーしたテストケースを書くことは難しい。 本稿では,スケジューラなどの並列ソフトウェアの開発手法を提案する。
• 参考スコア（独自算出の注目度）: 0.7199733380797578
• License:
• Abstract: In operating system development, concurrency poses significant challenges. It is difficult for humans to manually review concurrent behaviors or to write test cases covering all possible executions, often resulting in critical bugs. Preemption in schedulers serves as a typical example. This paper proposes a development method for concurrent software, such as schedulers. Our method incorporates model checking as an aid for tracing code, simplifying the analysis of concurrent behavior; we refer to this as model checking-assisted code review. While this approach aids in tracing behaviors, the accuracy of the results is limited because of the semantics gap between the modeling language and the programming language. Therefore, we also introduce runtime verification to address this limitation in model checking-assisted code review. We applied our approach to a real-world operating system, Awkernel, as a case study. This new operating system, currently under development for autonomous driving, is designed for preemptive task execution using asynchronous functions in Rust. After implementing our method, we identified several bugs that are difficult to detect through manual reviews or simple tests.
• Abstract（参考訳）: オペレーティングシステム開発では、並行処理が大きな課題となる。 人間が手動で同時動作をレビューしたり、可能なすべての実行をカバーしたテストケースを書いたりすることは難しい。 スケジューラのプリエンプションは典型的な例である。 本稿では,スケジューラなどの並列ソフトウェアの開発手法を提案する。 本手法では,コード追跡の補助としてモデルチェックを取り入れ,並列動作の解析を簡略化する。 このアプローチは動作の追跡に役立つが、モデリング言語とプログラミング言語のセマンティックスギャップのため、結果の精度は限られている。 そこで本研究では,モデル検査支援コードレビューにおいて,この制限に対処するための実行時検証も導入する。 実世界のオペレーティングシステムであるAwkernelのケーススタディとして,我々のアプローチを適用した。 この新しいオペレーティングシステムは現在、自動運転のために開発中であり、Rustの非同期関数を使用したプリエンプティブタスク実行用に設計されている。 提案手法の実装後,手動によるレビューや簡単なテストで検出が難しいいくつかのバグを特定した。

関連論文リスト

• Revisit Self-Debugging with Self-Generated Tests for Code Generation [18.643472696246686]
  自己生成テストによる自己改善は、有望なソリューションだが、その限界と現実的な可能性を十分に探求することができない。 プロセスにはポストエグゼクティブとインエグゼクティブ自己老化という2つのパラダイムを提案する。 実行後の自己老化は基本的な問題に苦しむが、自己生成テストによって生じるバイアスのため、競合する問題の改善の可能性を示す。
  論文  参考訳（メタデータ） (2025-01-22T10:54:19Z)
• Go-Oracle: Automated Test Oracle for Go Concurrency Bugs [6.773048267569272]
  Go言語では、バグが大きな問題となっている。 我々の研究は、Goプログラムのテストオラクル問題に対処し、テスト実行をパスまたはフェールとして自動的に分類することを目指している。 ネイティブなGo実行トレーサを使用して、包括的な実行イベントをキャプチャします。 トランスフォーマーベースのニューラルネットワークをトレーニングする前に、これらのトレースを前処理してエンコードして、トレースをパスまたはフェールのいずれかとして効果的に分類します。
  論文  参考訳（メタデータ） (2024-12-11T03:07:56Z)
• Commit0: Library Generation from Scratch [77.38414688148006]
  Commit0は、AIエージェントにスクラッチからライブラリを書くよう促すベンチマークである。 エージェントには、ライブラリのAPIを概説する仕様文書と、インタラクティブなユニットテストスイートが提供されている。 Commit0はまた、モデルが生成したコードに対して静的解析と実行フィードバックを受け取る、インタラクティブな環境も提供する。
  論文  参考訳（メタデータ） (2024-12-02T18:11:30Z)
• NExT: Teaching Large Language Models to Reason about Code Execution [50.93581376646064]
  大規模言語モデル(LLM)のコードは通常、プログラムの表面テキスト形式に基づいて訓練される。 NExTは,プログラムの実行トレースを検査し,実行時の動作を判断する手法である。
  論文  参考訳（メタデータ） (2024-04-23T01:46:32Z)
• Improving the Learning of Code Review Successive Tasks with Cross-Task Knowledge Distillation [1.0878040851638]
  本研究では,これらのタスクを同時に処理するために,クロスタスク知識蒸留を利用した新しいディープラーニングアーキテクチャdisCOREVを紹介する。 提案手法は, BLEUスコアによる評価値と, CodeBLEUスコアによるより正確なコード修正値から, より良いレビューコメントを生成する。
  論文  参考訳（メタデータ） (2024-02-03T07:02:22Z)
• Understanding prompt engineering may not require rethinking generalization [56.38207873589642]
  言語モデルによって与えられるPAC-Bayesと組み合わさったプロンプトの離散的性質は、文献の標準によって非常に厳密な一般化境界をもたらすことを示す。 この研究は、プロンプトエンジニアリングの広範な実践を正当化する可能性がある。
  論文  参考訳（メタデータ） (2023-10-06T00:52:48Z)
• Generative Models as a Complex Systems Science: How can we make sense of large language model behavior? [75.79305790453654]
  事前訓練されたモデルから望ましい振る舞いを排除し、望ましくないモデルを避けながら、NLPを再定義した。 言語モデルの振る舞いをタスク間性能を説明するカテゴリに分解する体系的な取り組みについて論じる。
  論文  参考訳（メタデータ） (2023-07-31T22:58:41Z)
• A Static Evaluation of Code Completion by Large Language Models [65.18008807383816]
  単純なプログラミング問題に対するモデル生成コードの機能的正当性を評価するために,実行ベースベンチマークが提案されている。 プログラムを実行せずにエラーを検出するlinterのような静的解析ツールは、コード生成モデルを評価するために十分に研究されていない。 抽象構文木を利用して,Pythonのコード補完における静的エラーを定量化する静的評価フレームワークを提案する。
  論文  参考訳（メタデータ） (2023-06-05T19:23:34Z)
• Execution Time Program Verification With Tight Bounds [6.36836017515443]
  本稿では,コア命令型プログラミング言語の実行時間境界を推論するための証明システムを提案する。 3つのケースに対してHoareロジックを定義し、注釈付きコスト対応操作セマンティクスに関してその健全性を証明する。 証明システムの実用性は、サンプルプログラムに適用するために必要な異なるモジュールのOCamlの実装で実証される。
  論文  参考訳（メタデータ） (2022-10-20T09:02:13Z)
• Measuring Coding Challenge Competence With APPS [54.22600767666257]
  コード生成のベンチマークであるAPPSを紹介する。 私たちのベンチマークには1万の問題が含まれています。 GPT-Neoのような最近のモデルでは、導入問題のテストケースの約15%をパスできる。
  論文  参考訳（メタデータ） (2021-05-20T17:58:42Z)

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

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