¥4,180( 本体 ¥3,800 )
商品詳細
SPINの基礎から実際の利用方法までを具体的に解説する日本で初めての書籍
◆SPINとは？ 社会の様々なところにソフトウェアが組み込まれ、その規模が飛躍的に大きくなってきている中、従来その信頼性を確保するための手法であったテスト手法は、時間やコストなどの面で開発の現状に追いつけない状況が出てきている。 そのテスト手法に代わるものとして注目されてきているのが形式的手法による検証（モデル検査法）であり、その中の一つがSPINである。限られたテストケースでの誤りの無さを保障する従来のテスト手法に対して、数学的・論理的基盤に基づいて正しさを証明するモデル検査法は、無限に近い組合せに対しても正しさを保障できる手法であり、その中でもSPINは実際に産業界での適用事例も豊富で、その技術習得がソフトウェア技術者の必須要素として注目されてきている。
第1章 モデル検査とは―自動検証とモデル検査法
第2章 SPINを使ってみよう―Promelaの書き方とコマンドの使い方
第3章 性質を表現する―正しさの基準
第4章 対象を広げる―Promelaの実行規則
第5章 仕組みを理解する―SPINの検証法
第6章 ケーススタディ(1) ソフトウェアデザインを検証する―状態遷移ダイアグラムの解析
第7章 ケーススタディ(2) モデル検査を使い分ける―Java並行プログラムの解析
第8章 ケーススタディ(3) 組込みソフトウェアの解析に使う―システムソフトウェアへの適用
第9章 ケーススタディ(4) 検査対象の大きさを適切に保つ―抽象化の方法
第10章 ケーススタディ(5) デザイン検証の実際を知る―分散コンポーネントの振舞い検証
◆SPINとは？ 社会の様々なところにソフトウェアが組み込まれ、その規模が飛躍的に大きくなってきている中、従来その信頼性を確保するための手法であったテスト手法は、時間やコストなどの面で開発の現状に追いつけない状況が出てきている。 そのテスト手法に代わるものとして注目されてきているのが形式的手法による検証（モデル検査法）であり、その中の一つがSPINである。限られたテストケースでの誤りの無さを保障する従来のテスト手法に対して、数学的・論理的基盤に基づいて正しさを証明するモデル検査法は、無限に近い組合せに対しても正しさを保障できる手法であり、その中でもSPINは実際に産業界での適用事例も豊富で、その技術習得がソフトウェア技術者の必須要素として注目されてきている。
第1章 モデル検査とは―自動検証とモデル検査法
第2章 SPINを使ってみよう―Promelaの書き方とコマンドの使い方
第3章 性質を表現する―正しさの基準
第4章 対象を広げる―Promelaの実行規則
第5章 仕組みを理解する―SPINの検証法
第6章 ケーススタディ(1) ソフトウェアデザインを検証する―状態遷移ダイアグラムの解析
第7章 ケーススタディ(2) モデル検査を使い分ける―Java並行プログラムの解析
第8章 ケーススタディ(3) 組込みソフトウェアの解析に使う―システムソフトウェアへの適用
第9章 ケーススタディ(4) 検査対象の大きさを適切に保つ―抽象化の方法
第10章 ケーススタディ(5) デザイン検証の実際を知る―分散コンポーネントの振舞い検証
購入前の注意点
・3Dセキュア導入とクレジットカードによるお支払いについて
・この書籍はKinoppy for iOS、Kinoppy for Android、Kinoppy for Windows または Kinoppy for Mac（いずれも最新版）でお読みください。
・電子書籍は会員サービス利用規約に則してご利用いただきます。
・海外会員様にはプレゼントを贈れません。
・この書籍はKinoppy for iOS、Kinoppy for Android、Kinoppy for Windows または Kinoppy for Mac（いずれも最新版）でお読みください。
・電子書籍は会員サービス利用規約に則してご利用いただきます。
・海外会員様にはプレゼントを贈れません。
著者情報
中島震［ナカジマシン］
１９８１年東京大学大学院理学系研究科修士課程修了。現在、国立情報学研究所教授・総合研究大学院大学教授、学術博士（東京大学）。この間、科学技術振興機構さきがけ研究員（兼任）、北陸先端科学技術大学院大学客員教授を歴任。形式手法、自動検証、ソフトウェア・モデリングなどの研究に従事（本データはこの書籍が刊行された当時に掲載されていたものです）
１９８１年東京大学大学院理学系研究科修士課程修了。現在、国立情報学研究所教授・総合研究大学院大学教授、学術博士（東京大学）。この間、科学技術振興機構さきがけ研究員（兼任）、北陸先端科学技術大学院大学客員教授を歴任。形式手法、自動検証、ソフトウェア・モデリングなどの研究に従事（本データはこの書籍が刊行された当時に掲載されていたものです）
