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

• Material Type: 博士論文
• Title: 証明責務の構造に基づくEvent-Bモデルの設計および証明支援手法
• Author/Editor: 佐藤, 直人; Naoto, Sato
• Author Heading: 佐藤, 直人; Naoto, Sato
• Publication Date: 2016-12-31
• Publication Date (W3CDTF): 2016-12-31
• Alternative Title: Supporting Methods for Modeling and Proving in Event-B based on Constructions of Proof Obligations
• Degree grantor/type: 電気通信大学
• Date Granted: 2016-12-31
• Date Granted (W3CDTF): 2016-12-31
• Dissertation Number: 甲第877号
• Degree Type: 博士（工学）
• Conferring No. (Dissertation): 甲第877号
• Text Language Code: jpn
• Target Audience: 一般
• Note (General): 形式手法Event-B では，証明対象の仕様をモデル記述し，モデルから作成される証明責務を証明することで仕様の正しさを示せる．しかし記述したモデルに矛盾や不備がある場合は，証明責務を証明できない．その場合，その証明責務を満たすようにモデルを修正する．しかし，モデルを修正することにより，既に実施済みの証明が無効化され，証明の手戻りが発生する可能性がある．本研究では，上記証明の手戻りを防止可能なモデル修正手法を提案する．さらに，提案手法の適用可能性および有効性を確認するため，ファイル転送プロトコルを対象とする適用例とその評価結果を示す．また，上記提案手法の前提となるモデル全体像を策定する工程に対しても，分割戦略木と呼ぶ記法に基づく手法を整備する．; 2016
• Persistent ID (NDL): info:ndljp/pid/11008573; https://dl.ndl.go.jp/pid/11008573
• Collection: 障害者向け資料
• Collection (Materials For Handicapped People:1): テキストデータ
• Collection (particular): 国立国会図書館デジタルコレクション > デジタル化資料 > 博士論文; https://dl.ndl.go.jp/collections/A00014
• Acquisition Basis: 博士論文（自動収集）
• Date Accepted (W3CDTF): 2018-01-02T17:18:43+09:00
• Date Created (W3CDTF): 2016-12-19
• Format (IMT): application/pdf
• Access Restrictions: 国立国会図書館内限定公開
• Service for the Digitized Contents Transmission Service: 図書館・個人送信対象外
• Availability of remote photoduplication service: 可
• Periodical Title (URI): http://id.nii.ac.jp/1438/00007913/
• Data Provider (Database): 国立国会図書館 : 国立国会図書館デジタルコレクション; https://dl.ndl.go.jp

Table of Contents

2023-12-08 再収集