論文の概要: Vision: An Extensible Methodology for Formal Software Verification in Microservice Systems
- arxiv url: http://arxiv.org/abs/2509.02860v1
- Date: Tue, 02 Sep 2025 22:11:46 GMT
- ステータス: 翻訳完了
- システム内更新日: 2025-09-04 21:40:46.354515
- Title: Vision: An Extensible Methodology for Formal Software Verification in Microservice Systems
- Title（参考訳）: Vision: マイクロサービスシステムにおける形式的ソフトウェア検証のための拡張可能な方法論
- Authors: Connor Wojtak, Darek Gajewski, Tomas Cerny,
- Abstract要約: スケーラビリティ、分散開発、継続的インテグレーションとデリバリのサポートなどにより、マイクロサービスシステムはますます普及しています。
本稿では,マイクロサービスソースコードを形式的システムモデルに静的に再構築する新しい手法を提案する。
- 参考スコア（独自算出の注目度）: 0.0
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: Microservice systems are becoming increasingly adopted due to their scalability, decentralized development, and support for continuous integration and delivery (CI/CD). However, this decentralized development by separate teams and continuous evolution can introduce miscommunication and incompatible implementations, undermining system maintainability and reliability across aspects from security policy to system architecture. We propose a novel methodology that statically reconstructs microservice source code into a formal system model. From this model, a Satisfiability Modulo Theories (SMT) constraint set can be derived, enabling formal verification. Our methodology is extensible, supporting software verification across multiple cross-cutting concerns. We focus on applying the methodology to verify the system architecture concern, presenting formal reasoning to validate the methodology's correctness and applicability for this concern. Additional concerns such as security policy implementation are considered. Future directions are established to extend and evaluate the methodology.
- Abstract（参考訳）: スケーラビリティ、分散開発、継続的インテグレーションとデリバリ(CI/CD)のサポートなどにより、マイクロサービスシステムはますます普及しています。
しかし、この独立したチームによる分散開発と継続的進化は、誤ったコミュニケーションと互換性のない実装を導入し、セキュリティポリシからシステムアーキテクチャに至るまで、システムの保守性と信頼性を損なう可能性がある。
本稿では,マイクロサービスソースコードを形式的システムモデルに静的に再構築する新しい手法を提案する。
このモデルから、Satifiability Modulo Theories (SMT) 制約セットを導出し、正式な検証を可能にする。
我々の方法論は拡張可能であり、複数の横断的関心事におけるソフトウェア検証をサポートする。
システムアーキテクチャの懸念を検証するために方法論を適用することに集中し、この懸念に対する方法論の正しさと適用性を検証するための正式な推論を提示します。
セキュリティポリシーの実装などの追加の懸念も考慮されている。
方法論を拡張して評価するために、今後の方向性が確立される。
関連論文リスト
- Explainable AI Systems Must Be Contestable: Here's How to Make It Happen [2.5875936082584623]
本稿では、説明可能なAIにおける競合性の最初の厳密な形式的定義について述べる。
我々は、ヒューマン中心のインターフェース、技術プロセス、組織アーキテクチャにまたがる、設計やポストホックメカニズムのモジュール化されたフレームワークを紹介します。
私たちの作業は実践者に、真のリコースと説明責任をAIシステムに組み込むためのツールを提供しています。
論文 参考訳（メタデータ） (2025-06-02T13:32:05Z) - Vulnerability Detection: From Formal Verification to Large Language Models and Hybrid Approaches: A Comprehensive Overview [3.135279672650891]
本稿では,最先端のソフトウェアテストと検証に焦点をあてる。
古典的な形式的手法、LLMに基づく分析、新しいハイブリッド手法の3つの主要なアプローチに焦点を当てている。
LLMによるインサイトとフォーマルリガーを統合することで,ソフトウェア検証の有効性とスケーラビリティが向上するかどうかを解析する。
論文 参考訳（メタデータ） (2025-03-13T18:22:22Z) - SoK: The Security-Safety Continuum of Multimodal Foundation Models through Information Flow and Game-Theoretic Defenses [58.93030774141753]
MFM(Multimodal foundation model)は、多種多様なデータモダリティを統合し、複雑で広範囲なタスクをサポートする。
本稿では,モデル行動とシステムレベルの相互作用の両方から生じる致命的な脅威を特定することで,MFMの文脈における安全性とセキュリティの概念を統一する。
論文 参考訳（メタデータ） (2024-11-17T23:06:20Z) - Testing learning-enabled cyber-physical systems with Large-Language Models: A Formal Approach [32.15663640443728]
機械学習(ML)をサイバー物理システム(CPS)に統合することは大きな利益をもたらす。
既存の検証と検証技術は、しばしばこれらの新しいパラダイムには不十分である。
本稿では, 基礎確率テストからより厳密なアプローチへ移行し, 正式な保証を実現するためのロードマップを提案する。
論文 参考訳（メタデータ） (2023-11-13T14:56:14Z) - Formal Methods for Autonomous Systems [21.989467515686858]
形式的手法は安全クリティカルシステムの正当性を確立する上で重要な役割を果たしてきた。
形式的なメソッドの主なビルディングブロックはモデルと仕様です。
様々な定式化の下で, 正しい構成合成を考察する。
論文 参考訳（メタデータ） (2023-11-02T14:18:43Z) - A Domain-Agnostic Approach for Characterization of Lifelong Learning
Systems [128.63953314853327]
「生涯学習」システムには,1)継続的学習,2)伝達と適応,3)拡張性があります。
この一連のメトリクスは、様々な複雑な生涯学習システムの開発に役立てることができることを示す。
論文 参考訳（メタデータ） (2023-01-18T21:58:54Z) - Recursively Feasible Probabilistic Safe Online Learning with Control Barrier Functions [60.26921219698514]
CBFをベースとした安全クリティカルコントローラのモデル不確実性を考慮した再構成を提案する。
次に、結果の安全制御器のポイントワイズ実現可能性条件を示す。
これらの条件を利用して、イベントトリガーによるオンラインデータ収集戦略を考案する。
論文 参考訳（メタデータ） (2022-08-23T05:02:09Z) - A Verification Framework for Certifying Learning-Based Safety-Critical
Aviation Systems [6.168537302126847]
本稿では,航空システムにおける学習ベースコンポーネントの設計時および実行時保証のための安全性検証フレームワークを提案する。
設計時保証の観点から,シミュレーション環境における異なるレベルの粒度からの知識を組み込んだオフライン混合忠実度検証ツールを提案する。
実行時保証の観点から,学習に基づく意思決定モデルのための到達可能性および統計に基づくオンラインモニタリングと安全ガードを提案する。
論文 参考訳（メタデータ） (2022-05-09T22:56:00Z) - Joint Differentiable Optimization and Verification for Certified
Reinforcement Learning [91.93635157885055]
安全クリティカル制御システムのためのモデルベース強化学習では,システム特性を正式に認定することが重要である。
本稿では,強化学習と形式検証を共同で行う枠組みを提案する。
論文 参考訳（メタデータ） (2022-01-28T16:53:56Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。