状態遷移表設計の形式検証ツール「Garakabu」 システムの「仕様」「設計モデル」において、システム上あってはならない状態と事象の組合せへの到達ルート(不具合)を100%検出・防止!数学的な証明がツールで可能!