WEKO3
インデックスリンク
アイテム
形式仕様記述に基づく検証の自動化
https://fukuyama-u.repo.nii.ac.jp/records/8152
https://fukuyama-u.repo.nii.ac.jp/records/815242f8dc4d-ea94-4ca6-8321-faa40c0e5556
| 名前 / ファイル | ライセンス | アクション |
|---|---|---|
KJ00005781548.pdf (736.1 kB)
|
|
| Item type | 紀要論文(ELS) / Departmental Bulletin Paper(1) | |||||
|---|---|---|---|---|---|---|
| 公開日 | 2003-12-01 | |||||
| タイトル | ||||||
| タイトル | 形式仕様記述に基づく検証の自動化 | |||||
| タイトル | ||||||
| タイトル | On an Automatic Verification based on Formal Specifications | |||||
| 言語 | en | |||||
| 言語 | ||||||
| 言語 | jpn | |||||
| キーワード | ||||||
| 主題Scheme | Other | |||||
| 主題 | 形式仕様 | |||||
| キーワード | ||||||
| 主題Scheme | Other | |||||
| 主題 | Z | |||||
| キーワード | ||||||
| 主題Scheme | Other | |||||
| 主題 | 代数仕様言語 | |||||
| キーワード | ||||||
| 主題Scheme | Other | |||||
| 主題 | 検証 | |||||
| キーワード | ||||||
| 言語 | en | |||||
| 主題Scheme | Other | |||||
| 主題 | Formal Specification | |||||
| キーワード | ||||||
| 言語 | en | |||||
| 主題Scheme | Other | |||||
| 主題 | Z | |||||
| キーワード | ||||||
| 言語 | en | |||||
| 主題Scheme | Other | |||||
| 主題 | Algebraic Specification Language | |||||
| キーワード | ||||||
| 言語 | en | |||||
| 主題Scheme | Other | |||||
| 主題 | Verification | |||||
| 資源タイプ | ||||||
| 資源タイプ識別子 | http://purl.org/coar/resource_type/c_6501 | |||||
| 資源タイプ | departmental bulletin paper | |||||
| ページ属性 | ||||||
| 内容記述タイプ | Other | |||||
| 内容記述 | P(論文) | |||||
| 著者名(日) |
石川, 洋
× 石川, 洋 |
|||||
| 著者名よみ | ||||||
| 識別子Scheme | WEKO | |||||
| 識別子 | 43764 | |||||
| 姓名 | イシカワ, ヒロシ | |||||
| 著者名(英) | ||||||
| 識別子Scheme | WEKO | |||||
| 識別子 | 43765 | |||||
| 姓名 | ISHIKAWA, Hiroshi | |||||
| 言語 | en | |||||
| 著者所属(日) | ||||||
| 値 | 福山大学工学部情報処理工学科 | |||||
| 著者所属(英) | ||||||
| 言語 | en | |||||
| 値 | Department of Information Processing Engineering, Faculty of Engineering, Fukuyama University | |||||
| 抄録(英) | ||||||
| 内容記述タイプ | Other | |||||
| 内容記述 | We presents an approach to reason about specifications written in a formal specification language automatically. Our reasoning approach is based as follows: (1)Specifications are written in Z, one of formal specification languages. (2)Reasoning system is based on W, a logic for the Z notation. (3)Verification system is written using CafeOBJ. The logic W is similar to a sequent calculus in the style of Gentzen. CafeOBJ is an executable algebraic specification language. Therefore our approach attempts to transform the specifications into sequents. This paper gives an example how to translate the Z. notations into sequents and how to prove using them. | |||||
| 雑誌書誌ID | ||||||
| 収録物識別子タイプ | NCID | |||||
| 収録物識別子 | AN00217655 | |||||
| 書誌情報 |
福山大学工学部紀要 巻 27, p. 225-232, 発行日 2003-12 |
|||||
