国内
日立ソリューションズ - 入退室管理システム
|
ドメイン |
|
|
開発対象 |
|
|
国 |
|
|
開発組織 |
|
|
形式手法（言語、ツール） |
|
|
適用範囲・規模（形式手法） |
|
|
適用対象のソフト種別 |
|
|
適用目的・工程 |
|
|
実装言語 |
|
|
実装規模 |
|
|
効果 |
|
詳細情報
検証内容
- 待合室に入室した人は、いつか必ず案内される
- 閲覧室に案内された人だけが、タッチパネル脇ID端末で、いつか必ず認証OKとなる
- 閲覧室から退出した閲覧者は、いつか必ず待機者リストから削除される
- 閲覧室に案内されていない人が、タッチパネル脇ID端末で認証を行っても、常に認証をパスしない
- 閲覧室Xが空室のとき以外、常に案内は変更されない
- 待機者リストは常にオーバーフローすることはない
検証規模
要求仕様７件のうち４件検証。その他設計関連の性質２件検証。
期間
判断
形式手法を利用した動機
要求仕様の妥当性、運用上の条件などを明確化する。制御アルゴリズムの正しさを検証する。
手法・ツール選択理由
制御系の検証を行うためSPINを用いた。また妥当性確認のためVDM++を使った。
障害と工夫
時間に関わる性質は扱えなかった。状態爆発が発生したためメッセージの送信のみを行うプロセスを統合するなどして、並行プロセスの数を減らした。
組織
体制
システム分析、設計の分析は日立ソフトウェアが実施し、SPIN形式記述によるモデリングおよび検証はMRIが実施した。VDM++の妥当性確認はNIIで実施した。
教育
SPINに関する和書のテキストを２冊程度精読した。
その他
NII等からモデリングにおいて助言を得たことが効果的であった。
情報源
入退出管理システムに関するモデル検証の一例、赤井健一郎 (株式会社三菱総合研究所) 石黒 正揮 (株式会社三菱総合研究所) 中島 震 (国立情報学研究所) 田中 一之 (株式会社日立ソリューションズ)
このページの先頭へ戻る