論文の概要: Sedeve-Kit, a Specification-Driven Development Framework for Building Distributed Systems
- arxiv url: http://arxiv.org/abs/2509.11566v1
- Date: Mon, 15 Sep 2025 04:14:00 GMT
- ステータス: 翻訳完了
- システム内更新日: 2025-09-16 17:26:23.143817
- Title: Sedeve-Kit, a Specification-Driven Development Framework for Building Distributed Systems
- Title（参考訳）: Sedeve-Kit - 分散システム構築のための仕様駆動開発フレームワーク
- Authors: Hua Guo, Yunhong Ji, Xuan Zhou,
- Abstract要約: 本稿では,分散システムのための仕様駆動開発フレームワークを提案する。
第1段階は、TLA$+$でシステム仕様と不変性を定義する。
第2段階では、確立された仕様に基づいて、実装の一貫性と正確性を保証するコードを書きます。
- 参考スコア（独自算出の注目度）: 2.8282788866878623
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: Developing distributed systems presents significant challenges, primarily due to the complexity introduced by non-deterministic concurrency and faults. To address these, we propose a specification-driven development framework. Our method encompasses three key stages. The first stage defines system specifications and invariants using TLA${^+}$. It allows us to perform model checking on the algorithm's correctness and generate test cases for subsequent development phases. In the second stage, based on the established specifications, we write code to ensure consistency and accuracy in the implementation. Finally, after completing the coding process, we rigorously test the system using the test cases generated in the initial stage. This process ensures system quality by maintaining a strong connection between the abstract design and the concrete implementation through continuous verification.
- Abstract（参考訳）: 分散システムの開発は、主に非決定論的並行性と障害によって引き起こされる複雑さによって、重大な課題を呈する。
このような問題に対処するため,我々は仕様駆動開発フレームワークを提案する。
提案手法は3つの重要な段階を含む。
第1段階は TLA${^+}$ を用いてシステム仕様と不変性を定義する。
これにより、アルゴリズムの正しさのモデルチェックを実行し、その後の開発フェーズのテストケースを生成することができる。
第2段階では、確立された仕様に基づいて、実装の一貫性と正確性を保証するコードを書きます。
最後に、コーディング処理を完了した後、初期生成したテストケースを用いてシステムを厳格にテストする。
このプロセスは、連続的な検証を通じて抽象設計と具体的な実装との強いつながりを保ち、システム品質を保証する。
関連論文リスト
- OpenCodeReasoning-II: A Simple Test Time Scaling Approach via Self-Critique [59.18475981916166]
OpenCodeReasoning-IIは、250万の質問解決批判三部作からなるデータセットである(約35万のユニークなプログラミング質問)。
本研究では,2段階の教師付き微調整戦略を採用する。第1段階はコード生成のための微調整に焦点を当て,第2段階はコード生成と批判の両方のためのモデルの共同トレーニングを行う。特に,コード生成と批判モデルの統合は,競争力のある符号化性能を大幅に向上させる。
論文 参考訳（メタデータ） (2025-07-11T23:35:54Z) - Training Language Models to Generate Quality Code with Program Analysis Feedback [66.0854002147103]
大規模言語モデル(LLM)によるコード生成は、ますます本番環境で採用されているが、コード品質の保証には失敗している。
実運用品質のコードを生成するためにLLMにインセンティブを与える強化学習フレームワークであるREALを提案する。
論文 参考訳（メタデータ） (2025-05-28T17:57:47Z) - Reinforcing Compositional Retrieval: Retrieving Step-by-Step for Composing Informative Contexts [67.67746334493302]
大規模言語モデル(LLM)は、多くのタスクにまたがる顕著な機能を示してきたが、複雑なタスクを扱うために外部のコンテキストに依存していることが多い。
我々は、このプロセスをマルコフ決定プロセス(MDP)としてモデル化するトリエンコーダシーケンシャルレトリバーを提案する。
提案手法は,サンプル間の依存関係を明示的にモデル化することの重要性を強調し,ベースラインを一貫して大幅に上回ることを示す。
論文 参考訳（メタデータ） (2025-04-15T17:35:56Z) - On Sequential Fault-Intolerant Process Planning [60.66853798340345]
我々は、逐次的フォールトトレラントプロセス計画(SFIPP)と呼ばれる計画問題を提案し、研究する。
SFIPPは、全ての段階が成功する場合にのみ計画が成功すると判断される多くの連続した多段階決定問題に共通する報酬構造をキャプチャする。
私たちは、異なるアクションを選択して、それぞれのステージで成功の確率を未知にする必要がある設定のために、確実に厳密なオンラインアルゴリズムを設計します。
論文 参考訳（メタデータ） (2025-02-07T15:20:35Z) - Testing Compositionality [0.0]
本稿では,実践において相互受理を利用するための3つの主要なアルゴリズムを提案する。
まず、仕様の相互受容を検証し、有効な実装すべてに対する構成性を証明する。
第2に,特定のブラックボックス実装に対する相互受け入れをチェックする,健全で徹底的なモデルベーステスト手順を提案する。
論文 参考訳（メタデータ） (2024-07-06T09:45:13Z) - Discovering Decision Manifolds to Assure Trusted Autonomous Systems [0.0]
本稿では,システムが提示できる正誤応答の範囲を最適化した探索手法を提案する。
この多様体は、従来のテストやモンテカルロシミュレーションよりもシステムの信頼性をより詳細に理解する。
この概念実証では,本手法を自動運転車のループ内ソフトウェア評価に適用する。
論文 参考訳（メタデータ） (2024-02-12T16:55:58Z) - A Verification Framework for Component-Based Modeling and Simulation
Putting the pieces together [0.0]
提案する検証フレームワークは,コンポーザビリティを異なるレベルで検証するための方法,テクニック,ツールサポートを提供する。
特に、コンポーザビリティ全体の正しさにおける重要性と、プロセスで生じる困難度から、ダイナミック・セマンティック・コンポータビリティ(Dynamic-Semantic Composability)のレベルに注目します。
論文 参考訳（メタデータ） (2023-01-08T18:53:28Z) - Complete Agent-driven Model-based System Testing for Autonomous Systems [0.0]
複雑な自律輸送システムをテストするための新しいアプローチについて述べる。
検証と検証に関して最も重大な問題のいくつかを軽減することを目的としている。
論文 参考訳（メタデータ） (2021-10-25T01:55:24Z) - Fold2Seq: A Joint Sequence(1D)-Fold(3D) Embedding-based Generative Model
for Protein Design [70.27706384570723]
Fold2Seqは特定の標的に条件付きタンパク質配列を設計するための新しいフレームワークである。
Fold2Seqの性能は, シーケンス設計の速度, カバレッジ, 信頼性において向上したか, 同等であったかを示す。
フォールドベースのFold2Seqの独特な利点は、構造ベースのディープモデルやRosettaDesignと比較して、3つの現実世界の課題においてより明確になる。
論文 参考訳（メタデータ） (2021-06-24T14:34:24Z) - CoCoMoT: Conformance Checking of Multi-Perspective Processes via SMT
(Extended Version) [62.96267257163426]
我々はCoCoMoT(Computing Conformance Modulo Theories)フレームワークを紹介する。
まず、純粋な制御フロー設定で研究したSATベースのエンコーディングを、データ認識ケースに持ち上げる方法を示す。
次に,プロパティ保存型クラスタリングの概念に基づく新しい前処理手法を提案する。
論文 参考訳（メタデータ） (2021-03-18T20:22:50Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。