論文の概要: Rely-guarantee Reasoning about Concurrent Reactive Systems: The PiCore
Framework, Languages Integration and Applications
- arxiv url: http://arxiv.org/abs/2309.09148v1
- Date: Sun, 17 Sep 2023 03:43:25 GMT
- ステータス: 処理完了
- システム内更新日: 2023-10-23 07:29:38.564358
- Title: Rely-guarantee Reasoning about Concurrent Reactive Systems: The PiCore
Framework, Languages Integration and Applications
- Title（参考訳）: Rely-guarantee氏が並列リアクティブシステムについて語る: PiCoreフレームワーク、言語統合、アプリケーション
- Authors: Yongwang Zhao, David Sanan
- Abstract要約: この記事では、CRSの正式な仕様と検証のための依存型推論フレームワークであるPiCoreを提案する。
我々は、複雑な反応構造をサポートするイベント仕様言語を設計し、イベントの振る舞いからCRSのリアクティブな側面の仕様とロジックを分離する。
この設計により、仕様や証明の変更なしに既存の2つの言語とそれらの信頼保証証明システムを統合することに成功した。
- 参考スコア（独自算出の注目度）: 0.0
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: The rely-guarantee approach is a promising way for compositional verification
of concurrent reactive systems (CRSs), e.g. concurrent operating systems,
interrupt-driven control systems and business process systems. However,
specifications using heterogeneous reaction patterns, different abstraction
levels, and the complexity of real-world CRSs are still challenging the
rely-guarantee approach. This article proposes PiCore, a rely-guarantee
reasoning framework for formal specification and verification of CRSs. We
design an event specification language supporting complex reaction structures
and its rely-guarantee proof system to detach the specification and logic of
reactive aspects of CRSs from event behaviours. PiCore parametrizes the
language and its rely-guarantee system for event behaviour using a
rely-guarantee interface and allows to easily integrate 3rd-party languages via
rely-guarantee adapters. By this design, we have successfully integrated two
existing languages and their rely-guarantee proof systems without any change of
their specification and proofs. PiCore has been applied to two real-world case
studies, i.e. formal verification of concurrent memory management in Zephyr
RTOS and a verified translation for a standardized Business Process Execution
Language (BPEL) to PiCore.
- Abstract（参考訳）: rely-guaranteeアプローチは、並列オペレーティングシステム、割り込み駆動制御システム、ビジネスプロセスシステムなど、同時応答システム(CRS)の構成検証のための有望な方法である。
しかし、異種反応パターン、抽象レベルの違い、現実のCRSの複雑さといった仕様は、いまだ頼りのアプローチに挑戦している。
この記事では、CRSの正式な仕様と検証のための依存型推論フレームワークであるPiCoreを提案する。
我々は,crssの反応的側面の仕様と論理をイベント振る舞いから切り離すために,複雑な反応構造とその依拠的証明システムをサポートするイベント仕様言語を設計した。
PiCoreは、Relied-guaranteeインターフェースを使用して、言語とそのRelied-guaranteeシステムのイベント動作をパラメータ化し、Relied-guaranteeアダプタを通じて、サードパーティ言語を容易に統合することができる。
この設計により、仕様や証明の変更なしに既存の2つの言語とそれらの信頼保証証明システムを統合することに成功した。
PiCoreは、Zephyr RTOSにおける並列メモリ管理の正式な検証と標準化されたBusiness Process Execution Language(BPEL)のPiCoreへの変換という、2つの実世界のケーススタディに適用されている。
関連論文リスト
- SVTRv2: CTC Beats Encoder-Decoder Models in Scene Text Recognition [77.28814034644287]
CTCモデルであるSVTRv2を提案する。
SVTRv2は、テキストの不規則性に対処し、言語コンテキストを利用するための新しいアップグレードを導入した。
我々は,SVTRv2を標準ベンチマークと最近のベンチマークの両方で評価した。
論文 参考訳（メタデータ） (2024-11-24T14:21:35Z) - Securing Legacy Communication Networks via Authenticated Cyclic Redundancy Integrity Check [98.34702864029796]
認証サイクル冗長性チェック(ACRIC)を提案する。
ACRICは、追加のハードウェアを必要とせずに後方互換性を保持し、プロトコルに依存しない。
ACRICは最小送信オーバーヘッド(1ms)で堅牢なセキュリティを提供する。
論文 参考訳（メタデータ） (2024-11-21T18:26:05Z) - A SAT-based approach to rigorous verification of Bayesian networks [13.489622701621698]
ベイジアンネットワークに適した検証フレームワークを導入し,これらの欠点に対処する。
本フレームワークは,(1)ベイジアンネットワークをブール論理リテラルに変換する2段階のコンパイルおよび符号化スキームと,(2)これらのリテラルを活用して制約として符号化された様々なプロパティを検証する形式的検証クエリの2つの主要なコンポーネントから構成される。
検証手法の効率をベンチマークし、実世界のシナリオでその実用性を実証する。
論文 参考訳（メタデータ） (2024-08-02T03:06:51Z) - Towards interfacing large language models with ASR systems using confidence measures and prompting [54.39667883394458]
本研究では,大言語モデル(LLM)を用いたASRテキストのポストホック修正について検討する。
精度の高い転写文に誤りを導入することを避けるため,信頼度に基づくフィルタリング手法を提案する。
その結果,競争力の低いASRシステムの性能が向上することが示唆された。
論文 参考訳（メタデータ） (2024-07-31T08:00:41Z) - Joint vs Sequential Speaker-Role Detection and Automatic Speech Recognition for Air-traffic Control [60.35553925189286]
本稿では,標準のASRアーキテクチャを頼りながら,両タスクを協調的に解決するトランスフォーマーベースのジョイントASR-SRDシステムを提案する。
複数のATCデータセット上でのASRとSRDの2つのケースドアプローチとの比較を行った。
論文 参考訳（メタデータ） (2024-06-19T21:11:01Z) - Rely-guarantee Reasoning about Concurrent Memory Management:
Correctness, Safety and Security [0.0]
メモリ管理の誤った仕様と実装は、システムのクラッシュや悪用可能な攻撃につながる可能性がある。
本稿では,実世界のOSにおける並列メモリ管理の最初の正式な仕様と機構的証明について述べる。
論文 参考訳（メタデータ） (2023-09-17T03:41:10Z) - Event-based Compositional Reasoning of Information-Flow Security for
Concurrent Systems [5.965840906609809]
並列システムのための情報フローセキュリティ(IFS)のための,信頼度に基づく構成推論手法を提案する。
Event''を並列言語に組み込むことで、まず言語を設計し、その言語のIFSセマンティクスを提供します。
IFSの構成的推論には、イベント上の新しい種類の巻き戻し条件(UC)を定義するために、Depended-guarantee仕様を用いる。
論文 参考訳（メタデータ） (2023-09-17T02:57:05Z) - Conformance Checking for Pushdown Reactive Systems based on Visibly
Pushdown Languages [0.0]
プッシュダウンリアクティブシステムをテストすることは、正確で堅牢なソフトウェア開発プロセスを保証する上で重要であると考えられている。
本稿では,この整合性関係を用いて完全な障害カバレッジを持つテストスイートを,プッシュダウンリアクティブシステムに生成可能であることを示す。
論文 参考訳（メタデータ） (2023-08-14T14:37:43Z) - Monitoring ROS2: from Requirements to Autonomous Robots [58.720142291102135]
本稿では,構造化自然言語で記述された要件から自律ロボットのランタイムモニタを生成するための形式的アプローチの概要について述べる。
当社のアプローチでは,Fletal Requirement Elicitation Tool (FRET) とランタイム検証フレームワークであるCopilotを,Ogma統合ツールを通じて統合しています。
論文 参考訳（メタデータ） (2022-09-28T12:19:13Z) - The Whole Truth and Nothing But the Truth: Faithful and Controllable
Dialogue Response Generation with Dataflow Transduction and Constrained
Decoding [65.34601470417967]
本稿では,ニューラルネットワークモデリングとルールベース生成の強みを組み合わせた対話応答生成のためのハイブリッドアーキテクチャについて述べる。
本実験により, 本システムは, 流布性, 妥当性, 真理性の評価において, ルールベースおよび学習的アプローチの両方に優れることがわかった。
論文 参考訳（メタデータ） (2022-09-16T09:00:49Z) - Towards Dynamic Consistency Checking in Goal-directed Predicate Answer
Set Programming [2.3204178451683264]
本稿では,動的一貫性チェック(Dynamic Consistency check)と呼ばれるトップダウン評価戦略のバリエーションを示す。
これにより、リテラルがプログラムのグローバルな制約に関連する否定と互換性がないかどうかを判断できる。
我々は、標準バージョンのs(CASP)の最大90倍のスピードアップを実験的に観察した。
論文 参考訳（メタデータ） (2021-10-22T20:38:48Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。