論文の概要: PLACIDUS: Engineering Product Lines of Rigorous Assurance Cases
- arxiv url: http://arxiv.org/abs/2407.10345v1
- Date: Sun, 14 Jul 2024 22:13:44 GMT
- ステータス: 処理完了
- システム内更新日: 2024-07-16 16:40:16.542934
- Title: PLACIDUS: Engineering Product Lines of Rigorous Assurance Cases
- Title（参考訳）: PLACIDUS:厳格な保証事例の製品ライン
- Authors: Logan Murphy, Torin Viger, Alessio Di Sandro, Marsha Chechik,
- Abstract要約: クリティカルなソフトウェアエンジニアリングでは、構造化保証ケース(AC)が、重要なプロパティがエビデンスアーティファクトによってどのようにサポートされているかを示すために使用されます。
本稿では,形式的手法とソフトウェア製品ラインエンジニアリングを統合する手法であるPLACIDUSを提案する。
- 参考スコア（独自算出の注目度）: 1.71849622776539
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: In critical software engineering, structured assurance cases (ACs) are used to demonstrate how key properties (e.g., safety, security) are supported by evidence artifacts (e.g., test results, proofs). ACs can also be studied as formal objects in themselves, such that formal methods can be used to establish their correctness. Creating rigorous ACs is particularly challenging in the context of software product lines (SPLs), wherein a family of related software products is engineered simultaneously. Since creating individual ACs for each product is infeasible, AC development must be lifted to the level of product lines. In this work, we propose PLACIDUS, a methodology for integrating formal methods and software product line engineering to develop provably correct ACs for SPLs. To provide rigorous foundations for PLACIDUS, we define a variability-aware AC language and formalize its semantics using the proof assistant Lean. We provide tool support for PLACIDUS as part of an Eclipse-based model management framework. Finally, we demonstrate the feasibility of PLACIDUS by developing an AC for a product line of medical devices.
- Abstract（参考訳）: 重要なソフトウェアエンジニアリングにおいて、構造化保証ケース(AC)は、キープロパティ(例えば、安全性、セキュリティ)がエビデンスアーティファクト(例えば、テスト結果、証明)によってどのようにサポートされているかを示すために使用されます。
ACは自身で形式的対象として研究することもでき、形式的手法はそれらの正当性を確立するのに使うことができる。
厳格なACを作成することは、ソフトウェア製品ライン(SPL)のコンテキストにおいて特に困難であり、関連するソフトウェア製品のファミリーが同時に設計される。
製品ごとに個別のACを作成することは不可能であるため、AC開発は製品ラインのレベルまで引き上げる必要がある。
本研究では,形式的手法とソフトウェア製品ラインエンジニアリングを統合する手法であるPLACIDUSを提案する。
PLACIDUS の厳密な基盤を提供するため,可変性を考慮した AC 言語を定義し,その意味を証明アシスタントである Lean を用いて定式化する。
Eclipseベースのモデル管理フレームワークの一部としてPLACIDUSのツールサポートを提供しています。
最後に,医療機器の製品ライン用ACを開発し,PLACIDUSの実現可能性を示す。
関連論文リスト
- Using Assurance Cases to Guide Verification and Validation of Research Software [0.0]
胸部画像から大動脈の3次元分画を自動的に抽出するソフトウェアをケーススタディとして,ACがVnV活性を誘導する方法を解説する。
ケーススタディでは、信頼を構築するための唯一の関心事ではなく、ソフトウェアとユーザの責任を明確に区別することが有用であることを強調している。
論文 参考訳（メタデータ） (2024-11-05T17:39:32Z) - Designing and Implementing a Generator Framework for a SIMD Abstraction Library [53.84310825081338]
SIMD抽象化ライブラリを生成するための新しいエンドツーエンドフレームワークであるTSLGenを提案する。
私たちのフレームワークは既存のライブラリに匹敵するもので、同じパフォーマンスを実現しています。
論文 参考訳（メタデータ） (2024-07-26T13:25:38Z) - Integrated Modeling, Verification, and Code Generation for Unmanned Aerial Systems [10.292890852621346]
無人航空システム(UAS)は、産業生産、軍事作戦、災害救助などの安全上重要な分野で広く利用されている。
本稿では,UASのモデリング,検証,コード生成に対する統合的なアプローチを検討することを目的とする。
論文 参考訳（メタデータ） (2024-06-13T14:53:40Z) - Automating SBOM Generation with Zero-Shot Semantic Similarity [2.169562514302842]
Software-Bill-of-Materials (SBOM)は、ソフトウェアアプリケーションのコンポーネントと依存関係を詳述した総合的なインベントリである。
本稿では,破壊的なサプライチェーン攻撃を防止するため,SBOMを自動生成する手法を提案する。
テスト結果は説得力があり、ゼロショット分類タスクにおけるモデルの性能を示す。
論文 参考訳（メタデータ） (2024-02-03T18:14:13Z) - InferAligner: Inference-Time Alignment for Harmlessness through
Cross-Model Guidance [56.184255657175335]
我々は,無害アライメントのためのクロスモデルガイダンスを利用する新しい推論時間アライメント手法であるtextbfInferAligner を開発した。
実験結果から,本手法はファイナンス,医学,数学の分野特化モデルに極めて効果的に適用可能であることが示された。
これは有害な命令とジェイルブレイク攻撃の両方のアタック成功率(ASR)を著しく低下させ、下流タスクではほとんど変化のないパフォーマンスを維持している。
論文 参考訳（メタデータ） (2024-01-20T10:41:03Z) - Operationalizing Assurance Cases for Data Scientists: A Showcase of
Concepts and Tooling in the Context of Test Data Quality for Machine Learning [1.6403311770639912]
保証事例( Assurance Cases, AC)は、安全工学において、品質主張を構造化された方法で議論するための確立されたアプローチである。
我々は,データサイエンティストが日々使用している技術であるPythonとJupyter Notebookに基づいて,機械学習(ML)コンポーネントのためのACの運用を支援するフレームワークを提案する。
ノートブックを通じて文書化されたフレームワークのアプリケーションの結果は、既存のACツールに統合できる。
論文 参考訳（メタデータ） (2023-12-08T09:34:46Z) - Simulation-based Safety Assurance for an AVP System incorporating
Learning-Enabled Components [0.6526824510982802]
テスト、検証、検証 AD/ADASセーフティクリティカルなアプリケーションが大きな課題のひとつとして残っています。
安全クリティカルな学習可能システムの検証と検証を目的としたシミュレーションベースの開発プラットフォームについて説明する。
論文 参考訳（メタデータ） (2023-09-28T09:00:31Z) - OpenICL: An Open-Source Framework for In-context Learning [48.75452105457122]
In-context Learning (ICL) と大規模言語モデル評価のためのオープンソースツールキット OpenICL を紹介する。
OpenICLは、ユーザが自分のニーズに合ったさまざまなコンポーネントを簡単に組み合わせられるように、非常に柔軟なアーキテクチャで研究に親しみやすい。
OpenICLの有効性は、分類、QA、機械翻訳、意味解析を含む幅広いNLPタスクで検証されている。
論文 参考訳（メタデータ） (2023-03-06T06:20:25Z) - Lessons from Formally Verified Deployed Software Systems (Extended version) [65.69802414600832]
本稿は、正式に認証されたシステムを作成し、実際に使用するためにデプロイした各種のアプリケーション分野のプロジェクトについて検討する。
使用する技術、適用の形式、得られた結果、そしてソフトウェア産業が形式的な検証技術やツールの恩恵を受ける能力について示すべき教訓を考察する。
論文 参考訳（メタデータ） (2023-01-05T18:18:46Z) - SMT-Based Safety Verification of Data-Aware Processes under Ontologies
(Extended Version) [71.12474112166767]
我々は、このスペクトルで最も調査されたモデルの1つ、すなわち単純なアーティファクトシステム(SAS)の変種を紹介する。
このDLは適切なモデル理論特性を享受し、後方到達性を適用可能なSASを定義することができ、対応する安全問題のPSPACEにおける決定可能性をもたらす。
論文 参考訳（メタデータ） (2021-08-27T15:04:11Z) - Safe RAN control: A Symbolic Reinforcement Learning Approach [62.997667081978825]
本稿では,無線アクセスネットワーク(RAN)アプリケーションの安全管理のためのシンボル強化学習(SRL)アーキテクチャを提案する。
我々は、ユーザが所定のセルネットワークトポロジに対して高レベルの論理的安全性仕様を指定できる純粋に自動化された手順を提供する。
ユーザがシステムに意図仕様を設定するのを支援するために開発されたユーザインターフェース(UI)を導入し、提案するエージェントの動作の違いを検査する。
論文 参考訳（メタデータ） (2021-06-03T16:45:40Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。