形式手法に関する文献について、モデル検査、定理証明、総合（モデル検査および定理証明を含む文献）に分類し、順に概要をまとめています。
また、後半では学習参考書として適切な文献を紹介します。
【モデル検査】
|
１ |
モデル検査法のソフトウェアデザイン検証への応用 |
|
文献情報 |
モデル検査法のソフトウェアデザイン検証への応用, 中島 震, コンピュータ ソフトウェア, Vol. 23 (2006) , No. 2 , 2_72-2_86 |
|
入手先 |
http://www.jstage.jst.go.jp/article/jssst/23/2/2_72/_pdf/-char/ja/ |
|
対象手法 |
SPINを中心とする。SMV, NuSMVなど他のモデル検査手法については応用動向についてまとめている。 |
|
想定読者 |
モデル検査など形式手法の前提知識の無い技術者 |
|
概要： モデル検査法およびそのツールなどに関して、技術の適用方法を伝えることに主眼をおいて分かりやすく解説している。また、ソフトウェア開発のいろいろな局面での利用例を紹介することで実用性について示している。簡単な例を用いてソフトウェアなどを状態遷移システムによるモデリングする方法と検証の基本原理について説明している。また、各種モデル検査ツールによる設計検証の応用事例を概観している。幅広くモデル検査ツールについて比較一覧をまとめている。また、モデル検査の書籍に関する概要紹介を行っている。 本文献により、始めて学習する人にとってもわかりやすくモデル検査の基本概念が理解でき、また、具体的な目的に応じてツールの選択を行う際の参考情報が得られる。 |
|
|
２ |
ソフトウェア工学からみたモデル検査法, 中島 震 |
|
文献情報 |
中島震. ソフトウェア工学からみたモデル検査法. 第22 回回路とシステム軽井沢シンポジウム,2009. |
|
入手先 |
|
|
対象手法 |
SPIN中心, SMVなども含む。 |
|
想定読者 |
モデル検査など形式手法の専門知識の無い技術者 |
|
概要： モデル検査に関して、記号モデル検査、状態探索法などのアルゴリズムの基本原理を分かり易く説明している。原理の説明において、一部、前提知識を必要とするため、抽象的に説明することで、一般の人にある程度理解できるように書かれている。また、モデル検査におけるシステムのモデリングにおいて必要とされる、モデルの抽象化について、幅広く概観している。さらに、モデリングのアプローチとして、入力情報に応じた分類を行い、その特徴比較を行っている。 具体的な実用事例は記載されていない。 |
|
|
３ |
ソフトウェア科学基礎（第10章 モデル検査ツール） |
|
文献情報 |
ソフトウェア科学基礎（第10章 モデル検査ツール）、磯部 祥尚, 櫻庭 健年, 田口 研治, 田原 康之, 粂野 文洋, 田中 譲、近代科学社 |
|
入手先 |
ISBN-10: 4764903555 （近代科学社） |
|
対象手法 |
SPIN, SMV, LTSA, UPPAAL |
|
想定読者 |
モデル検査の基礎を少し理解している人 |
|
概要： モデル検査SPIN, SMV, LTSA, UPPAALを対象に、各手法の概要、記述言語の概要、と構文に関する簡単な説明、例題によるツールの簡単な使い方についてツールの画面等を示しながらまとめている。 各手法の概要のところに、手法の用途や歴史について簡単に触れられている。 本書のモデル検査に関する章の基礎的な部分を読むなどして、モデル検査の基礎を少し理解した人を対象とした記述となっている。 |
|
|
４ |
モデルに基づく開発方法論の全て（第3章 検証） |
|
文献情報 |
組み込みソフトウェア2007 モデルに基づく開発方法論の全て, 第3章 検証, 日経BP社 |
|
入手先 |
ISBN-10: 4822202585（日経BP社） |
|
対象手法 |
NuSMV, VDＭ, LTSA, Garakabu, SCADEについて具体的に記載。Z, CafeOBJ, SPIN, ESC/Java, SLAM, BLAST, UPPAALについては概略を触れている。 |
|
想定読者 |
モデル検査など形式手法の前提知識の無い技術者 |
|
概要： 最初の章で、形式手法の概観を行い、次章以降で、NuSMV, LTSA, Garakabu, SCADE等のツールに関する具体的な特徴説明などを行っている。モデル検査を現場に導入する際の課題としてモデル検査の状態爆発の問題とそれを回避するための方法などについても説明している。 概観の章で、実応用例が数件挙げられている。また、各ツールの章でも、実応用を事例として手法の特徴や機能の概略を説明している。 |
|
【定理証明】
|
６ |
Bメソッドと支援ツール 来間 啓伸 |
|
文献情報 |
来間 啓伸, Bメソッドと支援ツール, コンピュータ ソフトウェア, Vol. 24 (2007), No. 2, 2_8-2_13 |
|
入手先 |
http://www.jstage.jst.go.jp/article/jssst/24/2/2_8/_pdf/-char/ja/ |
|
対象手法 |
Bメソッド、B4free |
|
想定読者 |
仕様検証について知識を持った人 |
|
概要： Bメソッドと、支援ツールであるB4freeについて解説している資料である。仕様検証について知識を持った人が抽象機械記法を用いた仕様記述を行い、コードを生成するまでの過程について解説されている。具体例を挙げ、そのシステムの仕様記述を例示することで具体的な記法や制約条件について記述している。また、実際のBメソッドを用いたシステムでの検証結果について参照しながらその長所についても説明されている。 本文献からはBメソッドを用いた仕様記述の概観が得られ、実際にツールを使って仕様検証をする際の参考情報が得られる。 |
|
|
７ |
オブジェクト指向形式仕様記述言語VDM++支援ツールVDMTools, 佐原 伸, 荒木 啓二郎 |
|
文献情報 |
佐原 伸, 荒木 啓二郎, オブジェクト指向形式仕様記述言語VDM++支援ツールVDMTools, コンピュータ ソフトウェア, Vol. 24 (2007), No. 2, 2_14-2_20 |
|
入手先 |
http://www.jstage.jst.go.jp/article/jssst/24/2/2_14/_pdf/-char/ja/ |
|
対象手法 |
VDM、VDM++、VICE |
|
想定読者 |
仕様記述を理解しており、VDMについての概要を把握している人 |
|
概要： VDMとその拡張VDM++、VICEによるモデル作成、仕様記述を支援するツールであるVDMToolsについて解説が行われている。VDMツールの機能概要や使い方、オブジェクト指向と同期並行処理記述を可能とするVDM++の記述例が掲載されており、ツールを用いた仕様記述の概観が得られる。また、VDM++を用いた成功例について紹介されており、適用例や適用方法の参考となる。VDM++を利用したときの筆者の経験や注意点についての情報がある。 本文献からはVDMToolsを用いた具体例と適用方法についての情報、さらにVDMを用いた仕様記述についての参考情報が得られる。 |
|
|
８ |
仕様記述言語Zと証明環境Isabelle/HOL-Z, 来間 啓伸, Burkhart WOLFF, David BASIN, 中島 震, |
|
文献情報 |
仕様記述言語Zと証明環境Isabelle/HOL-Z, 来間 啓伸, Burkhart WOLFF, David BASIN, 中島 震, コンピュータ ソフトウェア, Vol. 24 (2007), No. 2,2_21-2_26 |
|
入手先 |
|
|
対象手法 |
Z, Isabelle/HOL-Z |
|
想定読者 |
Z以外の仕様記述言語を用いたことがある人 |
|
概要： 仕様記述言語Zの概要と証明環境Isabelle/HOL-Zを用いた仕様記述と検証過程が解説されている。Zの概要の紹介では、Spiveyによる誕生日帳の例題を用いて、Zの基本的な使い方を解説している。具体的には誕生日システムを遷移システムとして定式化し、記述例した後にリファインメント、リファインメントの検証を行っている。 また、Zで書かれた仕様のための証明環境であるHOL-Zを用いた検証の概要についても記述されており、誕生日帳の検証の様子を示している。 本文献からはZの概要と証明環境HOL-Zの使い方についての情報が得られる。Zの周辺情報についても整理されている。 |
|
|
９ |
Alloy : 自動解析可能なモデル規範形式仕様言語, 中島 震, 鵜林 尚靖, |
|
文献情報 |
仕様記述言語Zと証明環境Isabelle/HOL-Z, 来間 啓伸, Burkhart WOLFF, David BASIN, 中島 震, コンピュータ ソフトウェア, Vol. 24 (2007), No. 2,2_21-2_26 |
|
入手先 |
|
|
対象手法 |
Alloy |
|
想定読者 |
Z記法について概略的な知識を有し、Alloyの概観を理解したい人 |
|
概要： 仕様記述言語Zの自動解析可能なサブセットであるAlloyについて、その概要が示されている。Alloyの歴史的経緯やその特徴について解説されており、Alloyについての文献についての紹介もある。具体的な応用例として、モデル規範形式仕様の標準的な例題である「誕生日帳」のAlloy記述例が紹介され、関係論理の考え方、解析の方法が示されている。筆者による利用経験や、Alloyの周辺についての研究動向と関連事情、その位置づけについての記述がある。Z記法についての知識を持った人を対象にしており、そのサブセットであるAlloyの情報を得ることができる。 |
|
|
10 |
CafeOBJ入門(1) 形式手法とCafeOBJ 二木 厚吉, 緒方 和博, 中村 正樹、コンピュータ ソフトウェア Vol. 25 (2008) , No. 2 |
|
文献情報 |
CafeOBJを用いたシステムの振舞の仕様記述・検証, コンピュータ ソフトウェア, Vol. 24 (2007), No. 2,2_21-2_26 |
|
入手先 |
http://www.jstage.jst.go.jp/browse/jssst/25/2/_contents/-char/ja/ |
|
対象手法 |
CafeOBJ |
|
想定読者 |
プログラミング（関数プログラミングであればなおよい、ただし、高階関数は必要ない）の経験があり、数学的帰納法による証明に触れたことのある方 |
|
概要： 本文献は、６編から構成されるCafeOBJ(代数仕様言語・処理系)入門の第１編である。CafeOBJ入門は、読み進めると同時に処理系と対話することで、CafeOBJをシステムの振舞の仕様記述・検証へ応用できる力を養うことを目的としている。CafeOBJのウェブサイト（http://www.ldl.jaist.ac.jp/cafeobj/）から、処理系およびCafeOBJ入門で使われている例題（仕様書等）を入手可能である。第１編では、簡単な例題を用いて、システムの振舞のモデル化（状態機械の作成）、状態機械のCafeOBJによる記述方法、および、状態機械が望みの性質を有すことの検証方法について簡潔に説明してある。第１編を読むだけで、CafeOBJを用いたシステムの振舞の仕様記述・検証の概略を把握できる。さらに、処理系と対話しながら、第６編までとおして読むことで、背景にある基礎技術から応用力まで身につけることができる。 |
|
【総合】
|
５ |
中島震，ソフトウェア工学の道具としての形式手法 |
|
文献情報 |
ソフトウェア工学の道具としての形式手法, 中島震, コンピュータ ソフトウェア, NII Technical Report ISSN 1346-5597 |
|
入手先 |
http://research.nii.ac.jp/TechReports/07-007J.pdf |
|
対象手法 |
形式手法全般(VDM、Z記法、Bメソッド、OCLとAlloy等) |
|
想定読者 |
形式手法について興味を持つ人、前提知識不要 |
|
概要： 形式手法全般について、その歴史と現在の動向について筆者の経験を元に記述されている文書。形式手法全般に関する知識と代表的な形式手法についての知識、実際の利用に関する筆者のアドバイスが掲載されている。 ソフトウェア開発における、形式手法によって可能となる設計記述の正しさを証明する手段、概略を説明している。また、代表的な形式手法をその特徴に従って分類し、VDM、Z記法、Bメソッド、OCLとAlloyといった例について解説を行っている。形式手法の組織・個人への導入・習得について整理がされている。上記に挙げた形式手法に関する参考文献や、実際の利用に関する注意点などについても言及されており、形式手法について興味をもつ初心者向けの文書である。 |
|
学習参考書として代表的なものを以下に示します。
これらは網羅的ではありませんが、カタログとして追加させていきます。
【モデル検査】
|
文献 |
中島震, ”SPINモデル検査,” 近代科学社, 2008. |
|
概要 |
SPINの使い方やモデリングの考え方を分かりやすく説明している。 |
|
文献 |
M. Ben-Ari, “Principles of the SPIN model checker,” 邦訳 オーム社, 2010年出版予定 |
|
概要 |
プログラムの設計検証に関して具体的なSPINのコードを使いながら分かりやすく説明している。 |
|
文献 |
萩谷昌巳監修, “SPINによる設計モデル検査”, 近代科学社, 2008 |
|
概要 |
SPINによる設計モデル検査について分かりやすく体系的に整理している。 |
|
文献 |
米田友洋, 梶原誠司, 土屋達弘, "ディペンダブルシステム," 共立出版, 2005. |
|
概要 |
モデル検査の理論を簡潔にまとめ、具体例としてSPINおよびCTLに基づくモデル検査としてSMVを解説している。 |
【その他】
|
文献 |
荒木啓二郎, 張漢明, “プログラム仕様記述論,” オーム社, 2002. |
|
概要 |
プログラム検証の入門、プログラム検証に特化した論理、VDM、Ｚなどについて分かりやすく説明している。 |
|
文献 |
荒木啓二郎, 張漢明, 荻野隆彦, 佐原伸, 染谷誠（訳）, “ソフトウェア開発のモデル化技法,” 岩波書店, 2003. |
|
概要 |
モデリングの基本的な概念や考え方について詳しく説明している。 |
|
文献 |
佐原伸, “形式手法の技術講座,”SRC, 2008. |
|
概要 |
ソフトウェア開発現場を想定読者とし、VDM++のためのツールVDMToolsを中心として、形式手法の概要および適用の第一歩となる形式仕様記述言語について解説している。 |
|
文献 |
玉井哲雄, "ソフトウェア工学の基礎," 岩波書店, 2004. |
|
概要 |
「モデル化」の基本的な考え方とその個別技術に重点をおき「ソフトウェア工学」全般を解説している。 |
|
文献 |
栗田 太郎，荒木啓二郎, モデル規範型形式手法VDMと仕様記述言語VDM++－高信頼性システムの開発に向けて－, 日本信頼性学会誌「信頼性」2009年9月 |
|
概要 |
VDM++をベースとして、その言語仕様の概略およびモデリングの考え方について解説している。 |