並行システムとは、マルチコアCPUを備えるPCやスマホのほか、組込み、スマートグリッドの処理にも欠かせないシステムである。本書は、その基礎理論（プロセス代数）であるCSPを用いた並行システムの構築方法や検証、実装の方法を概説。ソフトウェア開発者を中心に、並行プログラミングに挑戦したい人への一冊。

「リアルタイムシステム」（組込系など）への手法！
UPPAAL（ウパール）は，モデル検査ツールとしては比較的利用が容易ではあるが，実際の開発には多くのハードルがある．本書では，そのようなハードルを乗り越えるために必要な，UPPAALツール，時間オートマトン，検証したい性質を記述するための時間時相論理に関する知識，および実際の開発で検証の対象となるUML設計仕様のUPPAALによるモデル化方法など，具体的事例も交えてノウハウを解説している．

日本ソフトウェア科学会「ソフトウェア工学の基礎」研究会（FOSE)が主催する第18回ワークショップの論文集である。

会員600余社を超る情報サービス産業協会が送る業界基準書!!
　情報システムには、多様なステークホルダが関わるため、現場において要求工学を実践するためのガイドラインが求められている。
　本書は、要求工学のグローバル知識に基づき、現場視点から技術者が参画して、実践するガイドラインとして要求知識体系をまとめた。
　システム開発者、ユーザ、製品企画など「要求」に携わる方必携書。

品質向上に貢献する、要求獲得技法を詳解！
　ソフトウェアが社会に浸透すると供に、ソフトウェア開発の上流工程ではビジネスや運用環境の変化に即した要求の獲得・仕様化・確認・管理が求められている。要求工学では曖昧で変化しやすい要求を工学的に扱うことで、品質の高い要求仕様書を効率的に作成する各種の手法が開発されている。本書は、要求工学の基礎知識の理解と習得に役立つ1冊である。

　1979年に初版を発行して以来、時代と状況に合わせて改訂を重ねて使われ続けてきたシステム開発技法解説書の第5版。
　どんなことにも情報システムが欠かせない現代では、その開発環境も多様化し日々刻々と進化をしている。しかし、どんな環境で、誰が開発をしようとも、ユーザーの真のニーズをしっかりと把握し、それをシステム要件に反映すること、ユーザーの使い勝手の良いシステムを設計･開発することがシステム開発の原点である。
　本書は、そのような視点と、システム開発技法の歴史、著者の経験と研究を土台にして、開発者はもちろん、開発されたシステムを利用するユーザーにまでメリットをもたらす技法を余すことなく解説する。プロジェクトマネージャーや現場の開発者必携のバイブル。

ありそうで無かった解説書！机上の理論ではなく、開発の現場で活かせる実践的知識と理論の体系化！

■ソフトウェア開発の裏表を知り尽くした現役エンジニアが語る基本とエッセンス！
ソフトウェア工学は、ソフトウェア開発に内在する課題や問題を解決する土台となる基礎知識。しかし、様々な要素が複雑に絡まる開発現場では、抽象化された理論では対応しきれない面があることも否定できない。本書は著者が長く開発の第一線で活躍してきた中で、理論と経験を現場で活かせる知識として体系化した、実践に使えるソフトウェア工学の解説書。エンジニアの目からウロコの１冊です。

昨今、ソフトウェアの正しさを保証するソフトウェア検証の技術が重要視されているが、その中でも特にモデル検査が脚光を浴びている。それは数理論理学などに関する知識があまりない技術者にも、ソフトウェア開発の中で利用することが可能だからであろう。本書はSPINを中心にモデル検査をいかにしてソフトウェア開発のプロセスの中に位置づけるかについて実例を通して詳説している。

オープンソースの広がりにより、多様な機能を実現することは以前と比較すると驚くばかりに容易になっている。しかし、このような開発法ではスケーラビリティと高信頼性を同時に保証することはできない。機能の実現や追加が比較的安易にできる時代になったからこそ、成長し続けるシステム全体の正常な動作を保証しうる開発検査手法の必要性が増している。
　本書では、優れた開発者として最先端の理論やツールと使ってソフトウェア開発をするために必要な基礎知識である、論理学、並行システム、オートマトン、モデル検査のアルゴリズムや実装技術、モデル検証ツールをまとめて解説する。

SPINの基礎から実際の利用方法までを具体的に解説する日本で初めての書籍

◆SPINとは？
社会の様々なところにソフトウェアが組み込まれ、その規模が飛躍的に大きくなってきている中、従来その信頼性を確保するための手法であったテスト手法は、時間やコストなどの面で開発の現状に追いつけない状況が出てきている。
そのテスト手法に代わるものとして注目されてきているのが形式的手法による検証（モデル検査法）であり、その中の一つがSPINである。限られたテストケースでの誤りの無さを保障する従来のテスト手法に対して、数学的・論理的基盤に基づいて正しさを証明するモデル検査法は、無限に近い組合せに対しても正しさを保障できる手法であり、その中でもSPINは実際に産業界での適用事例も豊富で、その技術習得がソフトウェア技術者の必須要素として注目されてきている。