プログラミングは
書いては間違いを見つけて直す、
の繰り返し。

ソフトウェア・エンジニアはバグとは無縁ではいられません。 ちょっとした書き間違いや、仕様の勘違い、いろいろな理由でソフトウェアにはバグが入り込みます。 ほんの僅かな間違いが、ソフトウェアのおかしな動作につながるかもしれません。 現実世界の虫と同じように、ソフトウェアのバグを見つけ出すのは難しいです。 モノづくりの時間の多くが、どこにあるかわからない、もしかすると、ないかもしれない、バグを探す作業に費やされてしまいます。

形式手法は、バグのないソフトウェアの開発のために、エンジニアを様々な面から支援します。 仕様記述言語は、ソフトウェアの複雑な仕様や曖昧な仕様を、より正確に書くための言語を提供します。 コンピュータがソフトウェアの仕様を網羅チェックして、いろいろなところに隠れているバグを見つけ出します。 プログラムを動かさなくても、仕様があれば検査ができます。 万能の技術というわけにはいきませんが、形式手法は開発技術、生産技術と一緒に使うことで相乗効果を発揮する「デキる」技術です。 先端技術研究所では、形式手法を支える技術の開発を日々進めています。

モデル検査がバグを見つける作業を請け負います。 コンピュータが仕様を自動的にチェックして、バグをピンポイントで見つけて教えます。 上流工程から下流行程まで、どこででも使うことができます。 検査技術そのものも日々進歩しています。 何でも調べられる、とはさすがにいきませんが、仕様のレビューやテストにプラスアルファをもたらします。 先端技術研究所では、モデル検査の技術的課題を解決する方法を模索して、カタチにしていく活動に取り組んでいます。