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

The cover of this title could differ from library to library.

Available in National Diet Library

国立国会図書館デジタルコレクション

Digital data available（The University of Electro-Communications）

Check on the publisher's website

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

Persistent ID (NDL): info:ndljp/pid/10233494

Material type: 博士論文

Author: 佐藤, 直人ほか

Publisher: The University of Electro-Communications

Publication date: 2016-12-31

Material Format: Digital

Capacity, size, etc.: -

Name of awarding university/degree: 電気通信大学,博士（工学）

View All

Notes on use at the National Diet Library

本資料は、掲載誌(URI)等のリンク先にある学位授与機関のWebサイトやCiNii Dissertationsから、本文を自由に閲覧できる場合があります。

Notes on use

Note (General)：: 形式手法Event-B では，証明対象の仕様をモデル記述し，モデルから作成される証明責務を証明することで仕様の正しさを示せる．しかし記述したモデルに矛盾や不備がある場合は，証明責務を証明できない．その場合，その証明責務を満たすようにモデルを修正する．しかし，モデルを修正することにより，既に実施済みの...

Search by Bookstore

Read this material in an accessible format.

View materials in accessible formats for people with print disabilities (1Type)

Search by Bookstore

Read in Disability Resources

Other Services
- テキストデータ check it on 国立国会図書館デジタルコレクション

Bibliographic Record

You can check the details of this material, its authority (keywords that refer to materials on the same subject, author's name, etc.), etc.

Digital

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