Ｒｅｐｏｒｔ〜トヨタが「形式手法」採用へ　要求仕様の検証ツールを自社開発
日経コンピュータ　第821号　2012.11.8

　トヨタ自動車は、自動車の電子制御ユニットの組み込みソフトウエア開発に「形式手法」を適用する。ソフトの仕様を厳密に記述することで、矛盾や漏れがないかを確認する手法である。　２０１３年４月から製品開発の一部に適用する。適用対象は未定だが、ブレーキ制御など高い信頼性が求められるシステムになりそうだ。その後、効果を検証しながら適用範囲を広げていく。　形式手法を採用するために、トヨタはオープンソースの検証…