国内

日立ソリューションズ - 入退室管理システム

ドメイン
    その他(入退室管理)
開発対象
    入退室管理システム
    日本
開発組織
    日立ソリューションズ
形式手法(言語、ツール)
    SPIN, VDM++
適用範囲・規模(形式手法)
    入退室管理システムの制御アルゴリズム
適用対象のソフト種別
    制御系
適用目的・工程
    制御アルゴリズムの検証、要求の妥当性確認
実装言語
    C
実装規模
    30kLOC
効果
    待合室待ちリストのオーバーフローの可能性の発見。

詳細情報

検証内容

  • 待合室に入室した人は、いつか必ず案内される
  • 閲覧室に案内された人だけが、タッチパネル脇ID端末で、いつか必ず認証OKとなる
  • 閲覧室から退出した閲覧者は、いつか必ず待機者リストから削除される
  • 閲覧室に案内されていない人が、タッチパネル脇ID端末で認証を行っても、常に認証をパスしない
  • 閲覧室Xが空室のとき以外、常に案内は変更されない
  • 待機者リストは常にオーバーフローすることはない

検証規模

    要求仕様7件のうち4件検証。その他設計関連の性質2件検証。

期間

    2009年6月~2010年3月

判断

形式手法を利用した動機

    要求仕様の妥当性、運用上の条件などを明確化する。制御アルゴリズムの正しさを検証する。

手法・ツール選択理由

    制御系の検証を行うためSPINを用いた。また妥当性確認のためVDM++を使った。

障害と工夫

    時間に関わる性質は扱えなかった。状態爆発が発生したためメッセージの送信のみを行うプロセスを統合するなどして、並行プロセスの数を減らした。

組織

体制

    システム分析、設計の分析は日立ソフトウェアが実施し、SPIN形式記述によるモデリングおよび検証はMRIが実施した。VDM++の妥当性確認はNIIで実施した。

教育

    SPINに関する和書のテキストを2冊程度精読した。

その他

    NII等からモデリングにおいて助言を得たことが効果的であった。

情報源

    入退出管理システムに関するモデル検証の一例、赤井健一郎 (株式会社三菱総合研究所) 石黒 正揮 (株式会社三菱総合研究所) 中島 震 (国立情報学研究所) 田中 一之 (株式会社日立ソリューションズ)

このページの先頭へ戻る