状態遷移モデルに基づく設計と検証

組込みソフトウェア技術コンソーシアムの組込みシステム開発コースのひとつとして「状態遷移モデルに基づく設計と検証」というタイトルで講義・演習を実施しました。CATS株式会社のZIPCを使って，市販のストップウォッチのインタフェースの“動く仕様書（シミュレーション可能な仕様書）”を作る演習です。予め解答案としてこちらで状態遷移モデルを作ってみましたが、ストップウォッチ位のものでも詳細を洗い出してみると、結構複雑な状態遷移をしていることが分かります。予め検証してから実装に進めないと、すぐに手戻りしそうですね。