論文の概要: Contract Based Program Models for Software Model Checking

• arxiv url: http://arxiv.org/abs/2503.11236v1
• Date: Fri, 14 Mar 2025 09:34:59 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-03-17 13:08:08.536722
• Title: Contract Based Program Models for Software Model Checking
• Title（参考訳）: ソフトウェアモデル検査のための契約型プログラムモデル
• Authors: Jesper Amilon, Dilian Gurov,
• Abstract要約: 構成モデル検査のために以前に開発された形式主義を提案する。 InCで書かれた組込み型安全クリティカルソフトウェアにおいて,提案する検証手法をサポートするために,作業フローとツールチェーンの構想について述べる。
• 参考スコア（独自算出の注目度）: 0.0
• License:
• Abstract: Model checking temporal properties of software is algorithmically hard. To be practically feasible, it usually requires the creation of simpler, abstract models of the software, over which the properties are checked. However, creating suitable abstractions is another difficult problem. We argue that such abstract models can be obtained with little effort, when the state transformation properties of the software components have already been deductively verified. As a concrete, language-independent representation of such abstractions we propose the use of \emph{flow graphs}, a formalism previously developed for the purposes of compositional model checking. In this paper, we describe how we envisage the work flow and tool chain to support the proposed verification approach in the context of embedded, safety-critical software written in~C.
• Abstract（参考訳）: ソフトウェアの時間特性のモデルチェックはアルゴリズム的に難しい。 現実的に実現するには、通常は、プロパティがチェックされる、より単純で抽象的なソフトウェアモデルを作成する必要がある。 しかし、適切な抽象化を作成することは、別の難しい問題である。 このような抽象モデルは、ソフトウェアコンポーネントの状態変換特性が導出的に検証されている場合、ほとんど努力せずに得ることができると我々は主張する。 このような抽象概念の具体的、言語に依存しない表現として、構成モデル検査のために以前に開発された形式主義である \emph{flow graphs} を提案する。 本稿では,C言語で書かれた組込み型安全クリティカルソフトウェアにおいて,作業フローとツールチェーンが提案する検証手法をサポートする方法について述べる。

関連論文リスト

• Accessible Smart Contracts Verification: Synthesizing Formal Models with Tamed LLMs [7.087237546722617]
  ソフトウェア正当性を確立する最も強力な方法の1つは、フォーマルな方法を使用することである。 私たちの仕事は、形式モデルの作成を自動化することで、この重大な欠点に対処します。 このようにして、形式モデルを作成するのに必要な時間を大幅に削減する。
  論文  参考訳（メタデータ） (2025-01-22T15:57:29Z)
• Formal Analysis of the Contract Automata Runtime Environment with Uppaal: Modelling, Verification and Testing [0.3807314298073301]
  有限状態オートマトン方言を用いて指定されたサービスアプリケーションを実現するため、tt CAREと呼ばれる分散ランタイムアプリケーションが導入された。 tt CAREの形式的モデリング、検証、テストについて詳述する。
  論文  参考訳（メタデータ） (2025-01-22T15:03:25Z)
• Runtime Verification on Abstract Finite State Models [0.0]
  マルチスレッドJavaプログラムの実行から有限状態モデルを抽出する方法を示し、精度特性のランタイム検証を実行する。 本論文の主な貢献は,プロパティ保存抽象モデルのオンラインプロパティチェックを通じて,実行時検証の効率性を示すことである。
  論文  参考訳（メタデータ） (2024-06-18T15:32:31Z)
• Fine-Tuning Enhances Existing Mechanisms: A Case Study on Entity Tracking [53.66999416757543]
  本研究では,微調整が言語モデルに実装された内部メカニズムに与える影響について検討する。 微調整はモデルの機械的操作を変えるのではなく、強化する。
  論文  参考訳（メタデータ） (2024-02-22T18:59:24Z)
• Formal Verification Of A Shopping Basket Application Model Using PRISM [0.0]
  ショッピング・バスケット・アプリケーション・モデルにおけるPrism Model Checkerを用いたシミュレーションの結果を示す。 目的は、買い物客が買い物プロセスの多くの定義された状態を通過するときの行動をシミュレートすることである。
  論文  参考訳（メタデータ） (2023-07-16T00:14:40Z)
• Lifted Model Checking for Relational MDPs [12.574454799055026]
  pCTL-REBELは、リレーショナルMDP上のpCTL特性を検証するためのリフトモデルチェック手法である。 pCTLモデル検査手法は, 無限領域であっても, リレーショナルMDPに対して決定可能であることを示す。
  論文  参考訳（メタデータ） (2021-06-22T13:12:36Z)
• Model-Invariant State Abstractions for Model-Based Reinforcement Learning [54.616645151708994]
  textitmodel-invarianceという新しいタイプの状態抽象化を紹介します。 これにより、状態変数の見当たらない値の新しい組み合わせへの一般化が可能になる。 このモデル不変状態抽象化を通じて最適なポリシーを学習できることを実証する。
  論文  参考訳（メタデータ） (2021-02-19T10:37:54Z)
• DirectDebug: Automated Testing and Debugging of Feature Models [55.41644538483948]
  変数モデル(例えば、特徴モデル)は、ソフトウェアアーティファクトの変数と共通性を表現する一般的な方法である。 複雑でしばしば大規模な機能モデルは欠陥になりうる、すなわち、ソフトウェアアーチファクトの期待される変動特性を表現しない。
  論文  参考訳（メタデータ） (2021-02-11T11:22:20Z)
• Goal-directed Generation of Discrete Structures with Conditional Generative Models [85.51463588099556]
  本稿では,強化学習目標を直接最適化し,期待される報酬を最大化するための新しいアプローチを提案する。 提案手法は、ユーザ定義プロパティを持つ分子の生成と、所定の目標値を評価する短いピソン表現の同定という2つのタスクで検証する。
  論文  参考訳（メタデータ） (2020-10-05T20:03:13Z)
• Exploring Software Naturalness through Neural Language Models [56.1315223210742]
  ソフトウェア自然性仮説(Software Naturalness hypothesis)は、自然言語処理で使用されるのと同じ手法でプログラミング言語を理解することができると主張している。 この仮説は,事前学習されたトランスフォーマーベース言語モデルを用いて,コード解析タスクを実行することによって検討する。
  論文  参考訳（メタデータ） (2020-06-22T21:56:14Z)
• Interpretable Entity Representations through Large-Scale Typing [61.4277527871572]
  本稿では,人間の読みやすいエンティティ表現を作成し,箱から高パフォーマンスを実現する手法を提案する。 我々の表現は、微粒な実体型に対する後続確率に対応するベクトルである。 特定のドメインに対して,学習に基づく方法で,型セットのサイズを縮小できることを示す。
  論文  参考訳（メタデータ） (2020-04-30T23:58:03Z)

関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。

指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。