形式手法による組み込みソフトウェア開発

摘要

要求問の関係が複雑だと，ーつの機能を実装するのに複数のクラスに影響があるなど，見通しが悪くなります.見通しの悪さを定量的に評価するために，これを行列で表してみます.また，前回紹介したLTSAで仕様をステート・マシンにして検証し，続々と問題が発覚するようすを見ていきます.