論文の概要: Quantifying Software Correctness by Combining Architecture Modeling and
Formal Program Analysis
- arxiv url: http://arxiv.org/abs/2401.14320v1
- Date: Thu, 25 Jan 2024 17:18:33 GMT
- ステータス: 処理完了
- システム内更新日: 2024-01-26 13:58:28.840155
- Title: Quantifying Software Correctness by Combining Architecture Modeling and
Formal Program Analysis
- Title（参考訳）: アーキテクチャモデリングと形式的プログラム分析を組み合わせたソフトウェア正しさの定量化
- Authors: Florian Lanzinger, Christian Martin, Frederik Reiche, Samuel Teuber,
Robert Heinrich, Alexander Weigl
- Abstract要約: QuACは、サービス指向ソフトウェアシステムの正しさを定量化するモジュラーアプローチである。
本稿では,モデリングツールPalladioと推論検証ツールKeYを用いたJava用QuACの実装について述べる。
- 参考スコア（独自算出の注目度）: 41.375461087536294
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: Most formal methods see the correctness of a software system as a binary
decision. However, proving the correctness of complex systems completely is
difficult because they are composed of multiple components, usage scenarios,
and environments. We present QuAC, a modular approach for quantifying the
correctness of service-oriented software systems by combining software
architecture modeling with deductive verification. Our approach is based on a
model of the service-oriented architecture and the probabilistic usage
scenarios of the system. The correctness of a single service is approximated by
a coverage region, which is a formula describing which inputs for that service
are proven to not lead to an erroneous execution. The coverage regions can be
determined by a combination of various analyses, e.g., formal verification,
expert estimations, or testing. The coverage regions and the software model are
then combined into a probabilistic program. From this, we can compute the
probability that under a given usage profile no service is called outside its
coverage region. If the coverage region is large enough, then instead of
attempting to get 100% coverage, which may be prohibitively expensive, run-time
verification or testing approaches may be used to deal with inputs outside the
coverage region. We also present an implementation of QuAC for Java using the
modeling tool Palladio and the deductive verification tool KeY. We demonstrate
its usability by applying it to a software simulation of an energy system.
- Abstract（参考訳）: ほとんどの形式的手法は、ソフトウェアシステムの正しさを二分決定と見なす。
しかし、複雑なシステムの正確性を証明することは、複数のコンポーネント、利用シナリオ、環境から構成されているため困難である。
提案するQuACは,ソフトウェアアーキテクチャモデリングと帰納的検証を組み合わせることで,サービス指向ソフトウェアシステムの正しさを定量化するモジュール方式である。
私たちのアプローチは、サービス指向アーキテクチャのモデルとシステムの確率論的利用シナリオに基づいています。
単一のサービスの正確性はカバレッジ領域によって近似される。これは、そのサービスの入力が誤って実行されないことを証明した公式である。
カバレッジ領域は、形式的検証、専門家の推定、テストなど、さまざまな分析の組み合わせによって決定することができる。
カバレッジ領域とソフトウェアモデルは、確率的プログラムに結合される。
これにより、特定の使用状況下では、そのカバレッジ領域外ではサービスが呼び出されない確率を計算できる。
カバレッジ領域が十分に大きい場合、100%カバレッジを取得しようとする代わりに、実行時の検証やテストのアプローチが、カバレッジ領域外のインプットに使用される可能性がある。
また,モデリングツールのPalladioと推論検証ツールのKeYを用いて,Java用QuACの実装を提案する。
エネルギーシステムのソフトウェアシミュレーションに適用することにより,そのユーザビリティを実証する。
関連論文リスト
- SKADA-Bench: Benchmarking Unsupervised Domain Adaptation Methods with Realistic Validation [55.87169702896249]
Unsupervised Domain Adaptation (DA) は、ラベル付きソースドメインでトレーニングされたモデルを適用して、ラベルなしのターゲットドメインでデータ分散シフトをうまく実行する。
本稿では,DA手法の評価と,再重み付け,マッピング,部分空間アライメントなど,既存の浅層アルゴリズムの公平な評価を行うフレームワークを提案する。
本ベンチマークでは,現実的な検証の重要性を強調し,現実的なアプリケーションに対する実践的なガイダンスを提供する。
論文 参考訳（メタデータ） (2024-07-16T12:52:29Z) - Data-Driven Distributionally Robust Safety Verification Using Barrier Certificates and Conditional Mean Embeddings [0.24578723416255752]
問題を非現実的な仮定にシフトすることなく,スケーラブルな形式検証アルゴリズムを開発する。
問題を非現実的な仮定にシフトさせることなく,スケーラブルな形式検証アルゴリズムを開発するためには,バリア証明書の概念を用いる。
本稿では,2乗法最適化とガウス過程エンベロープを用いて効率よくプログラムを解く方法を示す。
論文 参考訳（メタデータ） (2024-03-15T17:32:02Z) - Discovering Decision Manifolds to Assure Trusted Autonomous Systems [0.0]
本稿では,システムが提示できる正誤応答の範囲を最適化した探索手法を提案する。
この多様体は、従来のテストやモンテカルロシミュレーションよりもシステムの信頼性をより詳細に理解する。
この概念実証では,本手法を自動運転車のループ内ソフトウェア評価に適用する。
論文 参考訳（メタデータ） (2024-02-12T16:55:58Z) - Finding Software Vulnerabilities in Open-Source C Projects via Bounded
Model Checking [2.9129603096077332]
我々は,汎用ソフトウェアシステムの脆弱性を効果的に検出できる境界モデル検査手法を提唱する。
我々は,最先端の有界モデルチェッカーを用いて,大規模ソフトウェアシステムを検証する手法を開発し,評価した。
論文 参考訳（メタデータ） (2023-11-09T11:25:24Z) - Path Structured Multimarginal Schr\"odinger Bridge for Probabilistic
Learning of Hardware Resource Usage by Control Software [1.7601096935307592]
経路構造を持つマルチマルジナル・シュル「オーディンガー橋問題 (MSBP) の解法は、最も測定値の高い軌道である。
制御ソフトウェアによるハードウェアリソース利用の学習において,MSBPを解くアルゴリズムの進歩を活用している。
論文 参考訳（メタデータ） (2023-10-01T07:35:12Z) - Lessons from Formally Verified Deployed Software Systems (Extended version) [65.69802414600832]
本稿は、正式に認証されたシステムを作成し、実際に使用するためにデプロイした各種のアプリケーション分野のプロジェクトについて検討する。
使用する技術、適用の形式、得られた結果、そしてソフトウェア産業が形式的な検証技術やツールの恩恵を受ける能力について示すべき教訓を考察する。
論文 参考訳（メタデータ） (2023-01-05T18:18:46Z) - Satellite Image Time Series Analysis for Big Earth Observation Data [50.591267188664666]
本稿では,機械学習を用いた衛星画像時系列解析のためのオープンソースRパッケージである sit について述べる。
本手法は, Cerrado Biome のケーススタディにより, 土地利用と土地被覆マップの精度が高いことを示す。
論文 参考訳（メタデータ） (2022-04-24T15:23:25Z) - PDC-Net+: Enhanced Probabilistic Dense Correspondence Network [161.76275845530964]
高度確率密度対応ネットワーク(PDC-Net+)は、精度の高い高密度対応を推定できる。
我々は、堅牢で一般化可能な不確実性予測に適したアーキテクチャと強化されたトレーニング戦略を開発する。
提案手法は,複数の挑戦的幾何マッチングと光学的フローデータセットに対して,最先端の結果を得る。
論文 参考訳（メタデータ） (2021-09-28T17:56:41Z) - Probabilistic Case-based Reasoning for Open-World Knowledge Graph
Completion [59.549664231655726]
ケースベース推論(CBR)システムは,与えられた問題に類似した事例を検索することで,新たな問題を解決する。
本稿では,知識ベース(KB)の推論において,そのようなシステムが実現可能であることを示す。
提案手法は,KB内の類似エンティティからの推論パスを収集することにより,エンティティの属性を予測する。
論文 参考訳（メタデータ） (2020-10-07T17:48:12Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。