SPINによる設計モデル検証: モデル検査の実践ソフトウェア検証 (トップエスイー実践講座 3)

著者 : 吉岡信和 青木利晃 田原康之

• 近代科学社 (2008年9月1日発売)

作品紹介・あらすじ

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

感想・レビュー・書評

[北海道大学工学研究院中央図書室さんの感想 · 2020年3月16日]

【電子ブックへのリンク先】
https://kinoden.kinokuniya.co.jp/hokudai/bookdetail/p/KP00012218
※学外から利用する場合は、以下のアドレスからご覧ください。（要ログイン）
https://www.lib.hokudai.ac.jp/remote-access/?url=https://kinoden.kinokuniya.co.jp/hokudai/bookdetail/p/KP00012218

[kaizenさんの感想 · 2012年3月11日]

形式手法の教育を行う場合に、受講生は全部読んでいる必要はないという命題をたててみました。

というのは、トップエスイー実践講座３では、「高度な数学的知識を習得して、現実的なシステムの仕様記述に利用することは容易でははい。」「モデル検査は、検証に必要な証明の作業を完全に自動的に行うため、上述の形式検証技術一般の問題点を解決できる。」とあることにもとづいています。

ただし、講師になる人間は、全部読んでいる必要があると感じました。

本書を読む前に、「四日で学ぶモデル検証」を実際に動かした方がよいと感じています。
自分では、本書も先に目を通そうとしたことがありましたが、めげていました。

「四日で学ぶモデル検証」をやってからは、少なくとも動作させたことがある部分は、
読み進むことができました。

著者プロフィール

早稲田大学理工学術院総合研究所・上級研究員／研究院教授。1998年、北陸先端科学技術大学院大学情報科学研究科博士後期課程修了。博士（情報科学）。同年（株）東芝入社。2002-2021 年 国立情報学研究所、2007-2021年、総合研究大学院大学、2021年より現職。IEEE CS Japan/Tokyo Joint Chapter 役員。JST 未来社会創造事業機械学習を用いたシステムの高品質化・実用化を加速する""Engineerable AI"" 技術の開発（eAIプロジェクト） に参画し、eAIプロジェクトのフレームワーク、社会実装のための普及戦略や技術検証を担当。

「2023年 『AIプロジェクトマネージャのための機械学習工学』 で使われていた紹介文から引用しています。」