論文の概要: Assurance Case Development for Evolving Software Product Lines: A Formal Approach
- arxiv url: http://arxiv.org/abs/2511.03026v1
- Date: Tue, 04 Nov 2025 21:52:14 GMT
- ステータス: 翻訳完了
- システム内更新日: 2025-11-06 18:19:32.259519
- Title: Assurance Case Development for Evolving Software Product Lines: A Formal Approach
- Title(参考訳): ソフトウェア製品ラインの進化のための保証事例開発--形式的アプローチ
- Authors: Logan Murphy, Torin Viger, Alessio Di Sandro, Aren A. Babikian, Marsha Chechik,
- Abstract要約: 重要なソフトウェアエンジニアリングでは、構造化保証ケース(AC)が、重要なシステムプロパティがエビデンスによってどのようにサポートされているかを示すために使用されます。
本稿では,交流発生と回帰解析の形式的アプローチについて述べる。
我々は,SPLの可変性を考慮したAC言語を定式化し,テンプレートベースのAC開発について検討する。
- 参考スコア(独自算出の注目度): 5.038351795081423
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: In critical software engineering, structured assurance cases (ACs) are used to demonstrate how key system properties are supported by evidence (e.g., test results, proofs). Creating rigorous ACs is particularly challenging in the context of software product lines (SPLs), i.e, sets of software products with overlapping but distinct features and behaviours. Since SPLs can encompass very large numbers of products, developing a rigorous AC for each product individually is infeasible. Moreover, if the SPL evolves, e.g., by the modification or introduction of features, it can be infeasible to assess the impact of this change. Instead, the development and maintenance of ACs ought to be lifted such that a single AC can be developed for the entire SPL simultaneously, and be analyzed for regression in a variability-aware fashion. In this article, we describe a formal approach to lifted AC development and regression analysis. We formalize a language of variability-aware ACs for SPLs and study the lifting of template-based AC development. We also define a regression analysis to determine the effects of SPL evolutions on variability-aware ACs. We describe a model-based assurance management tool which implements these techniques, and illustrate our contributions by developing an AC for a product line of medical devices.
- Abstract(参考訳): 重要なソフトウェアエンジニアリングでは、構造化保証ケース(AC)が、重要なシステムプロパティがエビデンス(例えば、テスト結果、証明)によってどのようにサポートされているかを示すために使用されます。
厳格なACの作成はソフトウェア製品ライン(SPL)の文脈において特に困難である。
SPLは非常に多数の製品を含むことができるため、個々の製品に対して厳密な交流を開発することは不可能である。
さらに、機能の変更や導入によってSPLが進化したとしても、この変更の影響を評価することは不可能である。
代わりに、単一のACをSPL全体に対して同時に開発できるようにACの開発とメンテナンスを解除し、可変性に留意した回帰分析を行う必要がある。
本稿では,交流発生と回帰解析の形式的アプローチについて述べる。
我々は,SPLの可変性を考慮したAC言語を定式化し,テンプレートベースのAC開発について検討する。
また, 変動性を考慮した交流に対するSPL進化の影響を決定するための回帰分析も定義する。
本稿では,これらの手法を実装したモデルベース保証管理ツールについて述べる。
関連論文リスト
- Verifying Correctness of PLC Software during System Evolution using Model Containment Approach [22.261628532402067]
そこで本研究では,PLCソフトウェアのアップグレード版の正当性を保証するための検証に基づく手法を提案する。
我々は,自家製のペトリネット型封じ込めチェッカーを開発した。
当社のアプローチを,ソフトウェアアップグレードに一般的なツールであるVerifAPSと比較し,約4倍のパフォーマンス向上を確認した。
論文 参考訳(メタデータ) (2025-09-06T04:45:17Z) - LASA: Enhancing SoC Security Verification with LLM-Aided Property Generation [7.52190283487474]
形式的プロパティ検証(FPV)は、設計の振る舞いをモデル化し、検証する機能を提供する。
現在のプラクティスでは、そのようなプロパティを作成するためにかなりの手作業が必要で、時間がかかり、コストがかかり、エラーが発生します。
本稿では,LLMと検索拡張生成(RAG)を活用して非空きセキュリティ特性を創出する新しいフレームワークであるLASAを提案する。
論文 参考訳(メタデータ) (2025-06-22T01:21:03Z) - Self-Refinement Strategies for LLM-based Product Attribute Value Extraction [51.45146101802871]
本稿では,製品属性値抽出タスクに2つの自己補充手法を適用した。
実験の結果, 2つの自己補充技術は, 処理コストを大幅に増大させながら, 抽出性能を著しく向上させることができないことがわかった。
開発データを持つシナリオでは、ファインチューニングが最もパフォーマンスが高いのに対して、ファインチューニングの上昇コストは製品記述の量が増加するにつれてバランスがとれる。
論文 参考訳(メタデータ) (2025-01-02T12:55:27Z) - KaPQA: Knowledge-Augmented Product Question-Answering [59.096607961704656]
我々はAdobe AcrobatとPhotoshop製品に焦点を当てた2つのQAデータセットを紹介した。
また、製品QAタスクにおけるモデルの性能を高めるために、新しい知識駆動型RAG-QAフレームワークを提案する。
論文 参考訳(メタデータ) (2024-07-22T22:14:56Z) - PLACIDUS: Engineering Product Lines of Rigorous Assurance Cases [1.71849622776539]
クリティカルなソフトウェアエンジニアリングでは、構造化保証ケース(AC)が、重要なプロパティがエビデンスアーティファクトによってどのようにサポートされているかを示すために使用されます。
本稿では,形式的手法とソフトウェア製品ラインエンジニアリングを統合する手法であるPLACIDUSを提案する。
論文 参考訳(メタデータ) (2024-07-14T22:13:44Z) - Integrated Modeling, Verification, and Code Generation for Unmanned Aerial Systems [10.292890852621346]
無人航空システム(UAS)は、産業生産、軍事作戦、災害救助などの安全上重要な分野で広く利用されている。
本稿では,UASのモデリング,検証,コード生成に対する統合的なアプローチを検討することを目的とする。
論文 参考訳(メタデータ) (2024-06-13T14:53:40Z) - Transformers as Statisticians: Provable In-Context Learning with
In-Context Algorithm Selection [88.23337313766353]
この研究はまず、変換器がICLを実行するための包括的な統計理論を提供する。
コンテクストにおいて、トランスフォーマーは、幅広い種類の標準機械学習アルゴリズムを実装可能であることを示す。
エンフィングル変換器は、異なるベースICLアルゴリズムを適応的に選択することができる。
論文 参考訳(メタデータ) (2023-06-07T17:59:31Z) - Progressive Open-Domain Response Generation with Multiple Controllable
Attributes [13.599621571488033]
本稿では,この課題に対処するために,漸進的に訓練された階層型バリデコーダを提案する。
PHEDはTransformerにConditional AutoEncoder (CVAE)をデプロイし、属性の1つの側面を1段階に含める。
PHEDは最先端のニューラルジェネレーションモデルを大きく上回り、期待通り多様な応答を生成する。
論文 参考訳(メタデータ) (2021-06-07T08:48:39Z) - DirectDebug: Automated Testing and Debugging of Feature Models [55.41644538483948]
変数モデル(例えば、特徴モデル)は、ソフトウェアアーティファクトの変数と共通性を表現する一般的な方法である。
複雑でしばしば大規模な機能モデルは欠陥になりうる、すなわち、ソフトウェアアーチファクトの期待される変動特性を表現しない。
論文 参考訳(メタデータ) (2021-02-11T11:22:20Z) - Hierarchical Variational Autoencoder for Visual Counterfactuals [79.86967775454316]
条件変量オート(VAE)は、説明可能な人工知能(XAI)ツールとして注目されている。
本稿では, 後部の効果がいかに緩和され, 対物的効果が成功するかを示す。
本稿では,アプリケーション内の分類器を視覚的に監査できる階層型VAEについて紹介する。
論文 参考訳(メタデータ) (2021-02-01T14:07:11Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。