トップエスイー実践講座 ＳＰＩＮによる設計モデル検証―モデル検査の実践ソフトウェア検証

萩谷 昌己【監修】/吉岡 信和/青木 利晃/田原 康之【著】

近代科学社（2008/09発売）

• サイズ B5判／ページ数 226p／高さ 24cm
• 商品コード 9784764903548
• NDC分類 007.63
• Cコード C3350

内容説明

ＳＰＩＮを中心にモデル検査をいかにしてソフトウェア開発のプロセスの中に位置づけるかについて実例を通して詳説。

目次

第１章　設計モデル検証とモデル検査
第２章　モデル検査概論
第３章　モデル検査ツールＳＰＩＮ概要
第４章　ＳＰＩＮによるモデル検査
第５章　ＳＰＩＮによる設計モデルの検証プロセス
第６章　設計モデルの検証の実際
第７章　検証の実践：抽象化・効率化・デバッグ
付録

著者等紹介

萩谷昌己［ハギヤマサミ］
１９８２年東京大学大学院理学系研究科修士課程修了。現在、東京大学大学院情報理工学系研究科教授。理学博士。形式的手法、理論計算機科学の研究に従事

吉岡信和［ヨシオカノブカズ］
１９９８年北陸先端科学技術大学院大学情報科学研究科博士後期課程修了。１９９８年株式会社東芝。現在、国立情報学研究所准教授・総合研究大学院大学准教授。博士（情報科学）。ソフトウェア工学、形式手法、セキュリティソフトウェア工学、セキュリティパターンの研究・教育に従事

青木利晃［アオキトシアキ］
１９９９年北陸先端科学技術大学院大学情報科学研究科博士後期課程修了。現在、北陸先端科学技術大学院大学安心電子社会研究センター特任准教授。博士（情報科学）。ソフトウェア工学・科学、形式手法、形式検証の研究に従事

田原康之［タハラヤスユキ］
１９９１年東京大学大学院理学系研究科修士課程修了。１９９１年株式会社東芝。２００３年国立情報学研究所。現在、電気通信大学大学院情報システム学研究科准教授。博士（情報科学）。エージェント技術、ソフトウェア工学の研究に従事（本データはこの書籍が刊行された当時に掲載されていたものです）
※書籍に掲載されている著者及び編者、訳者、監修者、イラストレーターなどの紹介情報です。

感想・レビュー

※以下の感想・レビューは、株式会社ブックウォーカーの提供する「読書メーター」によるものです。

[明るいくよくよ人]

ぱらぱらと斜め読み。上流工程にモデル検査をどのように取り入れていくかに関して、ネットワーク家電の例で記載。例が簡単なのか、筆者がモデル検査を上流工程に適用する際の課題が、例の中でどのように解決されていくのかが今ひとつつかめなかった。ただ、具体的に適用の仕方が示されているので、この部分は有用だった。SPINに関しては、あまり実用を示した本がない（と思うので）、全体的に脱稿が多い（特に、図版とかが抜けてる。TeXとかではないのかな）のが残念。

2012/06/09

[Q]

モデル検査の解説書。SPINは古くからあるツールで、専用の仕様記述言語で振る舞いを記述し、C言語に変換した後、当該コードをコンパイルし実行することで、モデル検査を行なう。LTLも扱うことができ、本書ではLTLを一から説明してくれてわかり易かった。一方でUMLとオブジェクト指向言語とSPINを組み合わせた設計プロセスは運用するには重く、さらに既存実装に追加の機能要求があった場合にはちゃんとモデルから修正追従できるのかは疑問が残った。モデル検査は初期の基本設計の妥当性を担保するためにのみ有用なのではと感じた。

2019/03/14