論文の概要: Spreadsheet-based Configuration of Families of Real-Time Specifications

• arxiv url: http://arxiv.org/abs/2310.20395v1
• Date: Tue, 31 Oct 2023 12:16:56 GMT
• ステータス: 処理完了
• システム内更新日: 2023-11-01 15:19:41.795110
• Title: Spreadsheet-based Configuration of Families of Real-Time Specifications
• Title（参考訳）: リアルタイム仕様ファミリのスプレッドシートベース構成
• Authors: Jos\'e Proen\c{c}a (CISTER and University of Porto, Portugal), David Pereira (CISTER, Polytechnic Institute of Porto, Portugal), Giann Spilere Nandi (CISTER, Polytechnic Institute of Porto, Portugal), Sina Borrami (Alstom), Jonas Melchert (Alstom)
• Abstract要約: この作業は、分析される形式モデルと、検査される要件の変動を利用して、リアルタイム仕様のバリエーションのモデルチェックを容易にする。 形式仕様のバリエーションの設定は、特定の構造を持つMS Excelスプレッドシートで記述されており、開発者が簡単に使用することができる。 本稿では,スプレッドシートベースのインタフェースとモデルチェッカーのシンプルさを保ちながら,機能の組み合わせを解析的に活用して,これまでの作業の拡張を提案する。
• 参考スコア（独自算出の注目度）: 0.0
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Model checking real-time systems is complex, and requires a careful trade-off between including enough detail to be useful and not too much detail to avoid state explosion. This work exploits variability of the formal model being analysed and the requirements being checked, to facilitate the model-checking of variations of real-time specifications. This work results from the collaboration between academics and Alstom, a railway company with a concrete use-case, in the context of the VALU3S European project. The configuration of the variability of the formal specifications is described in MS Excel spreadsheets with a particular structure, making it easy to use also by developers. These spreadsheets are processed automatically by our prototype tool that generates instances and runs the model checker. We propose the extension of our previous work by exploiting analysis over valid combination of features, while preserving the simplicity of a spreadsheet-based interface with the model checker.
• Abstract（参考訳）: リアルタイムシステムのモデルチェックは複雑で、状態の爆発を避けるのに十分な詳細を含めるには、慎重にトレードオフする必要がある。 この作業は、分析される形式モデルと、検査される要件の変動を利用して、リアルタイム仕様のバリエーションのモデルチェックを容易にする。 この研究は、valu3s european projectの文脈で、具体的なユースケースを持つ鉄道会社alstomとアカデミックの協力関係から生まれたものである。 形式仕様のバリエーションの設定は、特定の構造を持つMS Excelスプレッドシートで記述されており、開発者が簡単に使用することができる。 これらのスプレッドシートは、インスタンスを生成してモデルチェッカーを実行するプロトタイプツールによって自動的に処理されます。 本稿では,スプレッドシートベースのインタフェースをモデルチェッカーとシンプルに保ちつつ,有効な機能の組み合わせに関する分析を活用し,これまでの作業の拡張を提案する。

関連論文リスト

• A Simple Baseline for Predicting Events with Auto-Regressive Tabular Transformers [70.20477771578824]
  イベント予測への既存のアプローチには、タイムアウェアな位置埋め込み、学習行とフィールドエンコーディング、クラス不均衡に対処するオーバーサンプリング方法などがある。 基本位置埋め込みと因果言語モデリングの目的を持つ標準自己回帰型LPM変換器を用いて,単純だが柔軟なベースラインを提案する。 私たちのベースラインは、一般的なデータセットで既存のアプローチよりも優れており、さまざまなユースケースに使用することができます。
  論文  参考訳（メタデータ） (2024-10-14T15:59:16Z)
• Multi-Grained Specifications for Distributed System Model Checking and Verification [9.14614889088682]
  我々はTLA+を用いて、ZooKeeperとTLCモデルチェッカーのきめ細かい挙動をモデル化し、その正確性を検証する。 複数きめの仕様を書くことは現実的な実践であり、不安定な状態空間を伴わずにモデルコードギャップに対処できることを示す。
  論文  参考訳（メタデータ） (2024-09-22T02:59:56Z)
• SpreadsheetBench: Towards Challenging Real World Spreadsheet Manipulation [34.8332394229927]
  SpreadsheetBenchは,現在の大規模言語モデル(LLM)を,スプレッドシートユーザのワークフローにマージするように設計されている。 合成クエリと単純化されたスプレッドシートファイルに依存する既存のベンチマークとは異なり、SpreadsheetBenchはオンラインExcelフォーラムから収集された912の質問から作られている。 単一ラウンドおよび複数ラウンドの推論条件下での各種LLMの総合評価は,最先端モデル(SOTA)と人為的性能との間に大きなギャップがあることを示唆している。
  論文  参考訳（メタデータ） (2024-06-21T09:06:45Z)
• A General Model for Aggregating Annotations Across Simple, Complex, and Multi-Object Annotation Tasks [51.14185612418977]
  ラベルの品質を改善するための戦略は、複数のアノテータに同じ項目にラベルを付け、ラベルを集約するように求めることである。 特定のタスクに対して様々なbespokeモデルが提案されているが、様々な複雑なタスクを一般化するアグリゲーションメソッドを導入するのはこれが初めてである。 本論では,3つの新たな研究課題について検討し,今後の課題を概説する。
  論文  参考訳（メタデータ） (2023-12-20T21:28:35Z)
• Quantifying Language Models' Sensitivity to Spurious Features in Prompt Design or: How I learned to start worrying about prompt formatting [68.19544657508509]
  言語モデル(LLM)は、言語技術の基本コンポーネントとして採用されている。 いくつかの広く使われているオープンソースLLMは、数ショット設定でプロンプトフォーマットの微妙な変更に対して非常に敏感であることがわかった。 本稿では,与えられたタスクに対して有効なプロンプトフォーマットのサンプルセットを迅速に評価するアルゴリズムを提案し,モデル重み付けにアクセスせずに期待性能の間隔を報告する。
  論文  参考訳（メタデータ） (2023-10-17T15:03:30Z)
• Formal Verification Of A Shopping Basket Application Model Using PRISM [0.0]
  ショッピング・バスケット・アプリケーション・モデルにおけるPrism Model Checkerを用いたシミュレーションの結果を示す。 目的は、買い物客が買い物プロセスの多くの定義された状態を通過するときの行動をシミュレートすることである。
  論文  参考訳（メタデータ） (2023-07-16T00:14:40Z)
• Improving Text Matching in E-Commerce Search with A Rationalizable, Intervenable and Fast Entity-Based Relevance Model [78.80174696043021]
  エンティティベース関連モデル(EBRM)と呼ばれる新しいモデルを提案する。 この分解により、高精度にクロスエンコーダQE関連モジュールを使用できる。 また、ユーザログから自動生成されたQEデータによるQEモジュールの事前トレーニングにより、全体的なパフォーマンスが向上することを示す。
  論文  参考訳（メタデータ） (2023-07-01T15:44:53Z)
• Merlion: A Machine Learning Library for Time Series [73.46386700728577]
  Merlionは時系列のためのオープンソースの機械学習ライブラリである。 モデルの統一インターフェースと、異常検出と予測のためのデータセットを備えている。 Merlionはまた、本番環境でのモデルのライブデプロイメントと再トレーニングをシミュレートするユニークな評価フレームワークも提供する。
  論文  参考訳（メタデータ） (2021-09-20T02:03:43Z)
• DirectDebug: Automated Testing and Debugging of Feature Models [55.41644538483948]
  変数モデル(例えば、特徴モデル)は、ソフトウェアアーティファクトの変数と共通性を表現する一般的な方法である。 複雑でしばしば大規模な機能モデルは欠陥になりうる、すなわち、ソフトウェアアーチファクトの期待される変動特性を表現しない。
  論文  参考訳（メタデータ） (2021-02-11T11:22:20Z)
• IFC models for (semi)automating common planning checks for building permits [0.0]
  IFCモデルから必要な情報を抽出して代表規則をチェックするツールが開発された。 ケーススタディは、場所、規制、入力モデルに特化していますが、遭遇した問題のタイプは、自動コードコンプライアンスチェックの一般的な例です。
  論文  参考訳（メタデータ） (2020-11-03T15:29:47Z)

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

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