マルチスレッドプログラミングや組込みシステムのように，複数のコンポーネントが並行に動作するシステムの設計は難しいといわれています．このセミナーでは並行に動作するコンポーネントからなるシステム（並行システム）の設計を支援する理論と設計検証の基礎について，ツールを使いながら学びます．
このセミナーで習得できる技術は設計検証の技術です．設計した並行システムが期待した振る舞いをもっていること，つまり要求や仕様を満たしているということをツールを使って設計段階で検証する技術を学ぶことができます．
「手を動かせば理解は後からついてくる」というコンセプトで進めます．まずはツール上で手を動かし，視覚的なフィードバックを得ることが理解への早道であると考えます．ポイントごとに理論的な説明を行いますが，概念の獲得というのは時間のかかるものです．もし理解に不安が生じても，ツール上で確認する手段を持っていれば確信をもって自分の考えを進めることができるでしょう．
基礎とするのはプロセス代数と呼ばれる分野に属する CSP (Communicating Sequential Processes) という理論です．CSP は クイックソートの発明やプログラムの検証理論である Hoare 論理で有名な Tony Hoare さんによって提唱された理論です．テキストでは数学的になりがちな CSP の理論を，ほとんど数式を使わずに正確に解説します．さらにツールを使って視覚的に体験することで理解を深めることができます．
CSP に基づくシステムの振る舞いの記述は形式仕様記述の一種になります．広く知られている状態に基づいた仕様記述とは少し異なり，状態遷移に付随する相互作用の方に力点を置く記述方法になります．これを体験するとシステムの振る舞いに対する新たな視点を手に入れることができます．対象とするシステムの性質によって適切な記述形式を選択する自由度を増やすことができるでしょう．
※ 進捗に応じて，一部内容をスキップさせていただく場合があります．
前提として必要な知識は，プログラミングの知識と状態遷移モデル（オートマトン）の知識です．マルチスレッド（プロセス・タスク）のプログラムを書いたことがあるという程度の知識を仮定します．排他制御といった概念やミューテックス，セマフォといった同期のための機構についての知識を仮定します．
一部，発展的な内容に関する部分では，高校で習う程度の集合の記法（要素 x ∈ A，部分集合 A ⊆ B など）を使います．
CSP 理論に基づいたモデリングと検査が可能な SyncStitch というツールを使用します．このツールで学んだ考え方と記法は他のツール（FDR, PAT, LTSA, ProB）でも活用できます（※これらのツール間でも細かい差異はあります）．