新製品　組み込みソフト開発〜組み込みソフトの検証を　数学的な「形式手法」で大幅に効率化
日経ものづくり　第607号　2005.4.1

「ＳＣＡＤＥ」は，組み込みソフト開発時の検証作業に「形式手法」を用いたツール。生成したコード（Ｃ言語）と設計モデル（ソフトの基本的仕様を記述したモデル）の一致を証明する。テスト用入力データの必要がないのが特徴。「ブレーキが踏まれたら，クルーズ・コントロールは必ずオフになる」といった検証内容を，図形（ブロック・ダイヤグラム）で入力する。　「ＭＡＴＬＡＢ／Ｓｉｍｕｌｉｎｋ」と組み合わせることも可能。自…