論文の概要: 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つの実世界のケーススタディに適用されている。
関連論文リスト
- Prosody in Cascade and Direct Speech-to-Text Translation: a case study
on Korean Wh-Phrases [79.07111754406841]
本研究は,韻律が重要な役割を果たす発話を明瞭にするための直接S2TTシステムの能力を評価するために,コントラスト評価を用いることを提案する。
本結果は,カスケード翻訳モデルよりも直接翻訳システムの価値を明確に示すものである。
論文 参考訳(メタデータ) (2024-02-01T14:46:35Z) - HasTEE+ : Confidential Cloud Computing and Analytics with Haskell [50.994023665559496]
信頼性コンピューティングは、Trusted Execution Environments(TEEs)と呼ばれる特別なハードウェア隔離ユニットを使用して、コテナントクラウドデプロイメントにおける機密コードとデータの保護を可能にする。
低レベルのC/C++ベースのツールチェーンを提供するTEEは、固有のメモリ安全性の脆弱性の影響を受けやすく、明示的で暗黙的な情報フローのリークを監視するための言語構造が欠如している。
私たちは、Haskellに埋め込まれたドメイン固有言語(cla)であるHasTEE+を使って、上記の問題に対処します。
論文 参考訳(メタデータ) (2024-01-17T00:56:23Z) - 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) - A Modular and Adaptive System for Business Email Compromise Detection [0.7490096698922335]
Business Email Compromise (BEC) とスピアフィッシング攻撃は、世界中の組織にとって大きな課題となっている。
機械学習の最近の進歩、特に自然言語理解(NLU)は、そのような攻撃に対抗するための有望な道を提供する。
生産環境下で2年以上にわたって実証されてきた総合的かつ効率的なBEC検出システムCAPEについて述べる。
論文 参考訳(メタデータ) (2023-08-21T15:06:02Z) - Conformance Checking for Pushdown Reactive Systems based on Visibly
Pushdown Languages [0.0]
プッシュダウンリアクティブシステムをテストすることは、正確で堅牢なソフトウェア開発プロセスを保証する上で重要であると考えられている。
本稿では,この整合性関係を用いて完全な障害カバレッジを持つテストスイートを,プッシュダウンリアクティブシステムに生成可能であることを示す。
論文 参考訳(メタデータ) (2023-08-14T14:37:43Z) - Hybrid Rule-Neural Coreference Resolution System based on Actor-Critic
Learning [53.73316523766183]
コアレゾリューションシステムは2つの主要なタスクに取り組む必要がある。
ひとつのタスクは、潜在的な言及のすべてを検出することであり、もう1つは、可能な言及ごとに前者のリンクを学習することである。
本稿では,アクター・クリティカル・ラーニングに基づく複合ルール・ニューラル・コア参照解決システムを提案する。
論文 参考訳(メタデータ) (2022-12-20T08:55:47Z) - 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) - Generalizing Cross-Document Event Coreference Resolution Across Multiple
Corpora [63.429307282665704]
クロスドキュメントイベントコア参照解決(CDCR)は、文書の集合全体にわたってイベントの特定とクラスタ化を行う必要があるNLPタスクである。
CDCRは、下流のマルチドキュメントアプリケーションに利益をもたらすことを目標としているが、CDCRの適用による改善はまだ示されていない。
これまでのCDCRシステムは,1つのコーパスでのみ開発,トレーニング,テストが行われた。
論文 参考訳(メタデータ) (2020-11-24T17:45:03Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。