本日のお買い上げ

組込みプレス Vol.10

特集記事に「形式手法」が取り上げられていたので購入。モデル検査の適用例が紹介されていたけれど、やっぱり比較的単純なモデルでしか使えないらしい。これから仕様を決めて新規に作るソフトならともかく、数百万行にも及ぶ既存のソースコードを相手にする場合、検証に使うモデルの作成が一番ネックになってしまう。満足な資料も残っていないソースコードに対して、チマチマとモデルを作って検証していくのは現実的ではないよね。実際の検証は範囲を限定するとしても、モデルの作成だけは何とかして欲しい。この辺の課題をクリアできない限り、開発の現場で実用にはならないのではないだろうか？雑誌等で紹介される例は小規模なものが多く、今ひとつという感じ。大規模な開発に応用した例が有れば、是非とも参考にしたいのだが。