内容説明
オープンソースの広がりにより、多様な機能を実現することは以前と比較すると驚くばかりに容易になっている。しかし、このような開発法ではスケーラビリティと高信頼性を同時に保証することはできない。機能の実現や追加が比較的安易にできる時代になったからこそ、成長し続けるシステム全体の正常な動作を保証しうる開発検査手法の必要性が増している。 本書では、優れた開発者として最先端の理論やツールと使ってソフトウェア開発をするために必要な基礎知識である、論理学、並行システム、オートマトン、モデル検査のアルゴリズムや実装技術、モデル検証ツールをまとめて解説する。
目次
第0章 これから技術者をめざすひとのために
第1章 論理―正しいと考えられる事柄から正しい事柄を新たに導く
第2章 集合―多様な構造や構成の方法を知る
第3章 並行プログラム―並行性に特有の概念と知識を学ぶ
第4章 時相論理―システムやプログラムの動的な性質を記述する
第5章 検証性質の記述―一般の技術者がシステムの性質を記述する
第6章 オートマトン―コンピュータの動作を形式的に表現する
第7章 モデル検査基礎―並行システムのモデル検査を行う
第8章 モデル検査実装―検証モデル記述のノウハウを利用する
第9章 抽象解釈―モデル検査の複雑さを軽減する
第10章 モデル検査ツール―SPIN，SMV，LTSA，UPPAALを使う
感想・レビュー
※以下の感想・レビューは、株式会社ドワンゴの提供する「読書メーター」によるものです。
閑居
9
いささか名前負けしている感は否めない。ソフトウェア科学基礎と言いつつも、品質分析に必要な統計学もなければ、見積もりに必要な代数学もない。トップエスイーシリーズの他書の例に漏れず、形式手法に主眼を置き、論理学に特化している。たしかに、本書の特色はソフトウェアへの応用例を示しつつ、古典論理から時相論理までを数学的に解説しているでんであろう。その手の本は、確かに多くない。しかし、一階述語論理を超えると決定不能になることが数学的にわかっている形式手法に、どれほどの応用的価値があるのか、は疑問だ。2022/07/24
ひで
0
NK（自然演繹）の特徴の1つは「仮定を落とす」という概念を導出したことである。いくつかの推論規則では、その前提部の論理式を導くために使われた仮定が［・］によって示されているものがある。仮定は、文字通り一時的な仮の条件であって、推論の過程で、「したがってこの過程は否定される」「いずれこの仮定の場合もこれが成り立つ」などの結果を得た後は、仮定としての役割を終える。このようなとき、仮定が落ちるという。2012/04/04
