論文の概要: Towards Practical Requirement Analysis and Verification: A Case Study on Software IP Components in Aerospace Embedded Systems
- arxiv url: http://arxiv.org/abs/2404.00795v1
- Date: Sun, 31 Mar 2024 20:51:26 GMT
- ステータス: 処理完了
- システム内更新日: 2024-04-04 01:41:21.599082
- Title: Towards Practical Requirement Analysis and Verification: A Case Study on Software IP Components in Aerospace Embedded Systems
- Title（参考訳）: 実用的要件分析と検証に向けて:航空宇宙組み込みシステムにおけるソフトウェアIPコンポーネントを事例として
- Authors: Zhi Ma, Cheng Wen, Jie Su, Ming Zhao, Bin Yu, Xu Lu, Cong Tian,
- Abstract要約: 本稿では,航空宇宙組み込みシステムから派生したソフトウェアIPコンポーネントのケーススタディを提案する。
この研究は、構造化されていない自然言語を正式な仕様に変換するために、Large Language Modelsを使うことから始まる。
ソースコードが抽出された時間論理特性を満たすかどうかを確認するために、3つの異なる検証手法が使用される。
- 参考スコア（独自算出の注目度）: 14.989142843525133
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: IP-based software design is a crucial research field that aims to improve efficiency and reliability by reusing complex software components known as intellectual property (IP) components. To ensure the reusability of these components, particularly in security-sensitive software systems, it is necessary to analyze the requirements and perform formal verification for each IP component. However, converting the requirements of IP components from natural language descriptions to temporal logic and subsequently conducting formal verification demands domain expertise and non-trivial manpower. This paper presents a case study on software IP components derived from aerospace embedded systems, with the objective of automating the requirement analysis and verification process. The study begins by employing Large Language Models to convert unstructured natural language into formal specifications. Subsequently, three distinct verification techniques are employed to ascertain whether the source code meets the extracted temporal logic properties. By doing so, five real-world IP components from the China Academy of Space Technology (CAST) have been successfully verified.
- Abstract（参考訳）: IPベースのソフトウェア設計は、知的財産権(IP)コンポーネントとして知られる複雑なソフトウェアコンポーネントを再利用することで、効率と信頼性を向上させることを目的とした重要な研究分野である。
これらのコンポーネント、特にセキュリティに敏感なソフトウェアシステムにおいて、これらのコンポーネントの再利用性を確保するためには、要求を分析し、各IPコンポーネントに対して正式な検証を行う必要がある。
しかし、IPコンポーネントの要件を自然言語記述から時相論理に変換し、形式的な検証を行うにはドメインの専門知識と非自明なマンパワーが必要である。
本稿では,空域組み込みシステムから派生したソフトウェアIPコンポーネントを,要求分析と検証プロセスの自動化を目的としたケーススタディを提案する。
この研究は、構造化されていない自然言語を正式な仕様に変換するために、Large Language Modelsを使うことから始まる。
その後、ソースコードが抽出された時間論理特性を満たすかどうかを確認するために、3つの異なる検証手法が使用される。
これにより、中国宇宙技術アカデミー(CAST)の5つの現実世界のIPコンポーネントが検証された。
関連論文リスト
- Using Large Language Models for the Interpretation of Building Regulations [7.013802453969655]
大規模言語モデル(LLM)は、ユーザのプロンプトに応答する論理的に一貫性のあるテキストとソースコードを生成することができる。
本稿では, 建物規制をLegalRuleMLに変換する際のLLMの性能を, 数ショットの学習設定で評価する。
論文 参考訳（メタデータ） (2024-07-26T08:30:47Z) - Networks of Networks: Complexity Class Principles Applied to Compound AI Systems Design [63.24275274981911]
多くの言語モデル推論コールからなる複合AIシステムは、ますます採用されている。
本研究では,提案した回答の生成と正当性検証の区別を中心に,ネットワークネットワーク(NoN)と呼ばれるシステムを構築した。
我々は,Kジェネレータを備えた検証器ベースの判定器NoNを導入し,"Best-of-K"あるいは"judge-based"複合AIシステムのインスタンス化を行う。
論文 参考訳（メタデータ） (2024-07-23T20:40:37Z) - RITFIS: Robust input testing framework for LLMs-based intelligent
software [6.439196068684973]
RITFISは、自然言語入力に対するインテリジェントソフトウェアの堅牢性を評価するために設計された最初のフレームワークである。
RITFISは17の自動テスト手法を採用しており、元々はディープニューラルネットワーク(DNN)ベースのインテリジェントソフトウェア用に設計された。
LLMベースの知的ソフトウェア評価におけるRITFISの有効性を実証的検証により示す。
論文 参考訳（メタデータ） (2024-02-21T04:00:54Z) - Using the Abstract Computer Architecture Description Language to Model
AI Hardware Accelerators [77.89070422157178]
AI統合製品の製造者は、製品のパフォーマンス要件に適合するアクセラレータを選択するという、重大な課題に直面します。
抽象コンピュータアーキテクチャ記述言語(ACADL)は、コンピュータアーキテクチャブロック図の簡潔な形式化である。
本稿では,AIハードウェアアクセラレーションのモデル化にACADLを用いること,DNNのマッピングにACADL記述を使用し,タイミングシミュレーションのセマンティクスを解説し,性能評価結果の収集を行う。
論文 参考訳（メタデータ） (2024-01-30T19:27:16Z) - Large Language Models Based Automatic Synthesis of Software
Specifications [3.081650600579376]
SpecSynは、自然言語ソースからソフトウェア仕様を自動的に合成するフレームワークである。
提案手法は,シーケンス・ツー・シーケンスの学習問題として,ソフトウェア仕様の合成を定式化する。
論文 参考訳（メタデータ） (2023-04-18T01:22:44Z) - ETLP: Event-based Three-factor Local Plasticity for online learning with
neuromorphic hardware [105.54048699217668]
イベントベース3要素局所塑性(ETLP)の計算複雑性に明らかな優位性を有する精度の競争性能を示す。
また, 局所的可塑性を用いた場合, スパイキングニューロンの閾値適応, 繰り返しトポロジーは, 時間的構造が豊富な時間的パターンを学習するために必要であることを示した。
論文 参考訳（メタデータ） (2023-01-19T19:45:42Z) - Online Learning Probabilistic Event Calculus Theories in Answer Set
Programming [70.06301658267125]
イベント認識(CER)システムは、事前に定義されたイベントパターンを使用して、ストリーミングタイムスタンプデータセットで発生を検出する。
本稿では,複雑なイベントパターンによる確率論的推論を,イベント計算で重み付けされたルールの形で行うことができるAnswer Set Programming(ASP)に基づくシステムを提案する。
その結果, 効率と予測の両面で, 新たなアプローチの優位性が示された。
論文 参考訳（メタデータ） (2021-03-31T23:16:29Z) - Multi-Agent Reinforcement Learning with Temporal Logic Specifications [65.79056365594654]
本研究では,時間論理仕様を満たすための学習課題を,未知の環境下でエージェントのグループで検討する。
我々は、時間論理仕様のための最初のマルチエージェント強化学習手法を開発した。
主アルゴリズムの正確性と収束性を保証する。
論文 参考訳（メタデータ） (2021-02-01T01:13:03Z) - Formal Verification of Robustness and Resilience of Learning-Enabled State Estimation Systems [20.491263196235376]
我々は,ロボット工学の分野で広く利用されている学習可能な状態推定システム(LE-SESs)に注目した。
LE-SESを形式的検証の観点から検討し,システムモデルの満足度を決定する。
論文 参考訳（メタデータ） (2020-10-16T11:06:50Z) - Towards an Interface Description Template for AI-enabled Systems [77.34726150561087]
再利用(Reuse)は、システムアーキテクチャを既存のコンポーネントでインスタンス化しようとする、一般的なシステムアーキテクチャのアプローチである。
現在、コンポーネントが当初目的としていたものと異なるシステムで運用する可搬性を評価するために必要な情報の選択をガイドするフレームワークは存在しない。
我々は、AI対応コンポーネントの主情報をキャプチャするインターフェイス記述テンプレートの確立に向けて、現在進行中の作業について述べる。
論文 参考訳（メタデータ） (2020-07-13T20:30:26Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。