論文の概要: Temporal HAL-API Dependencies as a Gateway to Formal Embedded Software Development
- arxiv url: http://arxiv.org/abs/2512.12788v1
- Date: Sun, 14 Dec 2025 18:08:09 GMT
- ステータス: 翻訳完了
- システム内更新日: 2025-12-16 17:54:56.438692
- Title: Temporal HAL-API Dependencies as a Gateway to Formal Embedded Software Development
- Title（参考訳）: フォーマルな組み込みソフトウェア開発へのゲートウェイとしての時間的HAL-API依存性
- Authors: Manuel Bentele, Andreas Podelski, Axel Sikora, Bernd Westphal,
- Abstract要約: THAD(Temporal HAL-API Dependencies)は、組み込みソフトウェア開発における興味深い正しさのクラスを捉えるのに有用である。
THADは、産業組み込みソフトウェア開発において、フォーマルな手法を広く、より経済的に利用するためのゲートウェイを形成するかもしれない。
- 参考スコア（独自算出の注目度）: 1.1199585259018456
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: Temporal HAL-API Dependencies (THADs) can be useful to capture an interesting class of correctness properties in embedded software development. They demand a moderate effort for specification (which can be done via program annotations) and verification (which can be done automatically via software model checking). In this sense, they have the potential to form an interesting sweet spot between generic properties (that demand virtually no specification effort, and that are typically addressed by static analysis) and application-specific properties as addressed by full-fledged formal methods. Thus, they may form a gateway to wider and more economic use of formal methods in industrial embedded software development.
- Abstract（参考訳）: THAD(Temporal HAL-API Dependencies)は、組み込みソフトウェア開発における興味深い正しさのクラスを捉えるのに有用である。
彼らは仕様書(プログラムのアノテーションで行うことができる)と検証(ソフトウェアモデルチェックで自動的に行うことができる)に適度な努力を必要とします。
この意味では、それらはジェネリックプロパティ(ほとんど仕様の努力を必要とせず、静的解析によって対処される)と、本格的な形式メソッドによって対処されるアプリケーション固有のプロパティの間の興味深いスイートスポットを形成する可能性がある。
したがって、産業組み込みソフトウェア開発において形式的手法を広く、より経済的に活用するためのゲートウェイを形成することができる。
関連論文リスト
- Data Dependency-Aware Code Generation from Enhanced UML Sequence Diagrams [54.528185120850274]
本稿では,API2Depという新しいステップバイステップコード生成フレームワークを提案する。
まず、サービス指向アーキテクチャに適した拡張Unified Modeling Language (UML) APIダイアグラムを紹介します。
次に、データフローの重要な役割を認識し、専用のデータ依存推論タスクを導入する。
論文 参考訳（メタデータ） (2025-08-05T12:28:23Z) - Re:Form -- Reducing Human Priors in Scalable Formal Software Verification with RL in LLMs: A Preliminary Study on Dafny [78.1575956773948]
強化学習(RL)で訓練された大規模言語モデル(LLM)は、信頼性も拡張性もない、という大きな課題に直面している。
有望だが、ほとんど報われていない代替手段は、フォーマルな言語ベースの推論である。
生成モデルが形式言語空間(例えばダフニー)で機能する厳密な形式体系におけるLLMの接地は、それらの推論プロセスと結果の自動的かつ数学的に証明可能な検証を可能にする。
論文 参考訳（メタデータ） (2025-07-22T08:13:01Z) - Leveraging LLMs for Formal Software Requirements -- Challenges and Prospects [0.0]
VERIFAI1は、このギャップを埋めるための自動化および半自動化アプローチを調査することを目的としている。
本論文では, 課題の繰り返しと今後の研究方向性を明らかにするために, 関連文献の予備的な合成について述べる。
論文 参考訳（メタデータ） (2025-07-18T19:15:50Z) - An approach to performance portability through generic programming [0.0]
この研究は、低レベルおよび冗長なプログラミングツールを、C++のテンプレートメタプログラミングに基づく高レベルな汎用アルゴリズムに統合するための設計アプローチを説明する。
これにより、HPCのハードウェアの多様化期間において、科学ソフトウェアは保守性と効率が向上する。
論文 参考訳（メタデータ） (2023-11-08T21:54:43Z) - Lessons from Formally Verified Deployed Software Systems (Extended version) [65.69802414600832]
本稿は、正式に認証されたシステムを作成し、実際に使用するためにデプロイした各種のアプリケーション分野のプロジェクトについて検討する。
使用する技術、適用の形式、得られた結果、そしてソフトウェア産業が形式的な検証技術やツールの恩恵を受ける能力について示すべき教訓を考察する。
論文 参考訳（メタデータ） (2023-01-05T18:18:46Z) - SOLIS -- The MLOps journey from data acquisition to actionable insights [62.997667081978825]
本稿では,基本的なクロスプラットフォームテンソルフレームワークとスクリプト言語エンジンを使用しながら,すべての要件をサポートする統合デプロイメントパイプラインとフリー・ツー・オペレートアプローチを提案する。
しかし、このアプローチは、実際のプロダクショングレードシステムに機械学習機能を実際にデプロイするために必要な手順やパイプラインを提供していない。
論文 参考訳（メタデータ） (2021-12-22T14:45:37Z) - IFC models for (semi)automating common planning checks for building
permits [0.0]
IFCモデルから必要な情報を抽出して代表規則をチェックするツールが開発された。
ケーススタディは、場所、規制、入力モデルに特化していますが、遭遇した問題のタイプは、自動コードコンプライアンスチェックの一般的な例です。
論文 参考訳（メタデータ） (2020-11-03T15:29:47Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。