| 講演名 | 2002/5/10 スコーレム標準形を用いたZ仕様の代数仕様への変換 石川 洋, |
|---|---|
| PDFダウンロードページ | PDFダウンロードページへ |
| 抄録(和) | 形式仕様言語Zは高い表現力を持っているが,それによって記述された仕様を検証するためには,人間が地道に演繹規則に従って計算しなければならない.ソフトウェアの規模が増大化し,構造が複雑化すると,もはや人手で処理することは困難である.この問題を解決するために,Zで記述された仕様(以降,Z仕様と呼ぶ)を実行可能な処理系で動作可能な記述に変換し,コンピュータ支援による検証を行なうというアプローチがいくつか提案されている.我々はZ仕様を実行可能な処理系を持つ代数仕様への変換規則と,その規則に基づいて構築した仕様の変換システムを提案してきた.従来のシステムでは,ごく限られた記述しか扱えなかった.本稿では,従来では対応できなかった,限量記号を含む論理式をスコーレム標準形を利用して等式で記述する方法を提案する.変換によって生成された代数仕様は手動による修正が必要であるが,この枠組が体系化されると,Z仕様から代数仕様への変換作業効率の向上が見込まれる.そしてZ仕様の検証がコンピュータ支援により代数仕様によって自動化されることになり,検証作業の効率化も期待できる. |
| 抄録(英) | The formal specification language Z has been used to specify a wide spectrum of software systems. Specifications expressed using the Z notation have to be checked whether they satisfy some requirement or not. As the scale of software systems are growing, it is difficult to check manually. To clear the problem, there are many approaches to proof support for Z. We have suggested how to convert specifications in Z into the representation of an algebraic specification language that has an implementation. Some restricted specifications are allowed to convert. In this paper, we suggest how to convert the predicate part of the scheme including quantifiers into the representation of an algebraic specification language using Skolem Normal Form. In present, we have to edit a part of the algebraic specifications generated such a method. By improving our method, we can expect an efficient computer-assisted checking for the specification of large and/or complicated software systems. |
| キーワード(和) | 形式仕様言語Z / スキーマ / スコーレム標準形 / 代数仕様言語 |
| キーワード(英) | Z:Formal Specification Language / Schema / Skolem Normal Form / Algebraic Specification Language |
| 資料番号 | SS2002-2 |
| 発行日 |
| 研究会情報 | |
| 研究会 | SS |
|---|---|
| 開催期間 | 2002/5/10(から1日開催) |
| 開催地（和） | |
| 開催地（英） | |
| テーマ（和） | |
| テーマ（英） | |
| 委員長氏名（和） | |
| 委員長氏名（英） | |
| 副委員長氏名（和） | |
| 副委員長氏名（英） | |
| 幹事氏名（和） | |
| 幹事氏名（英） | |
| 幹事補佐氏名（和） | |
| 幹事補佐氏名（英） | |
| 講演論文情報詳細 | |
| 申込み研究会 | Software Science (SS) |
|---|---|
| 本文の言語 | JPN |
| タイトル（和） | スコーレム標準形を用いたZ仕様の代数仕様への変換 |
| サブタイトル（和） | |
| タイトル（英） | A method to convert Z Specification into Algebraic Specification using Skolem Normal Form |
| サブタイトル（和） | |
| キーワード(1)（和/英） | 形式仕様言語Z / Z:Formal Specification Language |
| キーワード(2)（和/英） | スキーマ / Schema |
| キーワード(3)（和/英） | スコーレム標準形 / Skolem Normal Form |
| キーワード(4)（和/英） | 代数仕様言語 / Algebraic Specification Language |
| 第 1 著者 氏名（和/英） | 石川 洋 / Hiroshi ISHIKAWA |
| 第 1 著者 所属（和/英） | 福山大学工学部 Faculty of Engineering, Fukuyama University |
| 発表年月日 | 2002/5/10 |
| 資料番号 | SS2002-2 |
| 巻番号（vol） | vol.102 |
| 号番号（no） | 63 |
| ページ範囲 | pp.- |
| ページ数 | 6 |
| 発行日 | |