証明責務の構造に基づくEvent-Bモデルの設計および証明支援手法

• 資料種別: 博士論文
• タイトル: 証明責務の構造に基づくEvent-Bモデルの設計および証明支援手法
• 著者・編者: 佐藤, 直人; Naoto, Sato
• 著者標目: 佐藤, 直人; Naoto, Sato
• 出版年月日等: 2016-12-31
• 出版年（W3CDTF）: 2016-12-31
• 並列タイトル等: Supporting Methods for Modeling and Proving in Event-B based on Constructions of Proof Obligations
• 授与機関名: 電気通信大学
• 授与年月日: 2016-12-31
• 授与年月日（W3CDTF）: 2016-12-31
• 報告番号: 甲第877号
• 学位: 博士（工学）
• 博論授与番号: 甲第877号
• 本文の言語コード: jpn
• 対象利用者: 一般
• 一般注記: 形式手法Event-B では，証明対象の仕様をモデル記述し，モデルから作成される証明責務を証明することで仕様の正しさを示せる．しかし記述したモデルに矛盾や不備がある場合は，証明責務を証明できない．その場合，その証明責務を満たすようにモデルを修正する．しかし，モデルを修正することにより，既に実施済みの証明が無効化され，証明の手戻りが発生する可能性がある．本研究では，上記証明の手戻りを防止可能なモデル修正手法を提案する．さらに，提案手法の適用可能性および有効性を確認するため，ファイル転送プロトコルを対象とする適用例とその評価結果を示す．また，上記提案手法の前提となるモデル全体像を策定する工程に対しても，分割戦略木と呼ぶ記法に基づく手法を整備する．; 2016
• 国立国会図書館永続的識別子: info:ndljp/pid/11008573; https://dl.ndl.go.jp/pid/11008573
• コレクション（共通）: 障害者向け資料
• コレクション（障害者向け資料：レベル1）: テキストデータ
• コレクション（個別）: 国立国会図書館デジタルコレクション > デジタル化資料 > 博士論文; https://dl.ndl.go.jp/collections/A00014
• 収集根拠: 博士論文（自動収集）
• 受理日（W3CDTF）: 2018-01-02T17:18:43+09:00
• 作成日（W3CDTF）: 2016-12-19
• 記録形式（IMT）: application/pdf
• オンライン閲覧公開範囲: 国立国会図書館内限定公開
• デジタル化資料送信: 図書館・個人送信対象外
• 遠隔複写可否（NDL）: 可
• 掲載誌（URI）: http://id.nii.ac.jp/1438/00007913/
• 連携機関・データベース: 国立国会図書館 : 国立国会図書館デジタルコレクション; https://dl.ndl.go.jp

目次

2023-12-08 再収集