FRETish要求のための構成的証明フレームワーク【JST・京大機械翻訳】

Conrad Esther; Titolo Laura; Giannakopoulou Dimitra; Pressburger Thomas; Dutle Aaron

プレプリント

J-GLOBAL ID：202202218068392896 整理番号：22P0025878

FRETish要求のための構成的証明フレームワーク【JST・京大機械翻訳】

A Compositional Proof Framework for FRETish Requirements

出版者サイト {{ this.onShowPLink() }} 複写サービスで全文入手
高度な検索・分析はJDreamⅢで

この文献はプレプリントです。プレプリントについてはこちらをご確認ください。

著者 (5件)： , , , ,
資料名：
発行年： 2022年01月10日プレプリントサーバーでの情報更新日： 2022年01月10日
JST資料番号： O7000B 資料種別：プレプリント
記事区分：プレプリント発行国：アメリカ合衆国 (USA) 言語：英語 (EN)

構造化自然言語は,最も書かれた要求と線形時間論理のような数学的形式仕様を作るあいまいな自然言語間の貿易空間を提供する。FRETはNASAで開発されたシステム要求の導出のための構造化自然言語である。関連するオープンソースツールFretは,いくつかの検証と解析ツールに入力できる時間論理式にFRETish要求を翻訳するためのサポートを提供する。安全クリティカルシステムの文脈において,生成された公式が対応するFRETish要求の意味論を正確に捉えることを確実にすることが重要である。本論文は,Fretによって計算されたFRETish仕様とそれらの時間的論理対応物の間の意味的等価性の証明と新しい記述意味論を含むFRETish言語の厳密な形式化を提示する。完全形式化と証明をプロトタイプ検証システム(PVS)定理証明器において開発した。【JST・京大機械翻訳】

, , , , , , , , , , , ,
, , 【Automatic Indexing@JST】

計算機システム開発

前のページに戻る