ホーム

本サイトは近代科学社から出版されている本「並行システムの検証と実装」に関連する情報を掲載しています。

形式手法CSPに基づく高信頼並行システム開発入門 トップエスイーシリーズ 実践講座６
並行システムの検証と実装, 磯部祥尚（著）, 東野輝夫（監修）
近代科学社, 2012.12.26. [amazon]

[news]

• • [2023.02.05] FDRとJCSPについて

    • 2023年2月5日現在、モデル検査器 FDR の最新版は FDR4 であり、本書籍で紹介している FDR2 とはインターフェースが変更されていますが、FDR2の構文はFDR4でも有効であり、詳細化関係の検査も可能です。[FDR4のインストール方法（PDF）]

    • JavaのCSPライブラリ JCSP は2014年以降メンテされていないようですが、例えば、Go言語は並行処理モデルとしてCSPを採用しています。CSPによる形式化、FDRによる検証、Go言語による実装の例として、こちらのスライド「並行処理のモデル化、検証、実装の概要（PDF）」もご覧いただければ幸いです。

  • [2013.04.02] モデル検査器ProBのページとProB用のサンプルを追加しました。

[サブページ]

• • サンプルコード： 本書で使用しているFDRスクリプト、JCSPプログラムをダウンロードできます。

  • 訂正情報： 本書の間違いを訂正するための情報です。

  • リンク： 関連するウェブサイトのリンク集です。

  • ProB: FDRと互換性のあるモデル検査器です（フリー＆オープンソース、Windows版あり）

補足情報： 本書ではFDRというモデル検査器をもとに検証技術の紹介をしています。FDRは学術目的では無料ですが、産業目的では有料です。FDRスクリプトを検証可能な他のツールにProB（フリー＆オープンソース）があります。ProBのインストール方法はこちらをご覧ください。