58キーワード仕様検証、ソフトウェア検証、ソフトウェア自動合成、モデル検査、安全性■?研究概要飛行機の制御プログラム、オペレーティングシステム、銀行のATMなど社会インフラであるソフトウェアは、ユーザとやりとりをしながらサービスを提供するシステムです。このようなシステムはリアクティブシステムと呼ばれています。リアクティブシステムの構築や検証にはその設計図となる仕様が重要です。仕様通りにソフトウェアが稼働するか、重要な性質を満たしているかを自動で検証する方法があり、実際、ソフトウェア検証ツールも存在します。ソフトウェア検証ツールを利用する場合、検証したい仕様や性質自体に誤りがないことは重要です。特に、仕様を満たすプログラムが存在しない場合、検証は無駄になります。この無駄を回避するためには、仕様を書いたときに、その仕様を満たすプログラムが存在するかを判定する必要があります。この判定技術は、プログラムの自動合成や仕様自体の欠陥や誤りの検出に役に立ちます。この判定技術の実用化を目指しています。■?産業界へのアピールポイント●ソフトウェア作成前にソフトウェア仕様を検証することにより、システム設計段階での仕■?実用化例?応用事例?活用例●仕様のプログラム化可能性判定システムの構築●仕様からのプログラム自動合成システムの構築●仕様の不備の検出●プログラムや仕様の安全性の検証●ソフトウェア仕様からのソフトウェアの自動合成を行うことが可能となる。この自動合成により、ソフトウェアの生成コストを下げることできるとともに、ソフトウェアの検証を行う必要がなくなる。様の不備や欠陥の検出し、ソフトウェア開発の効率化が可能となる。吉浦?紀晃（ヨシウラ ノリアキ） 教授大学院理工学研究科 数理電子情報部門 情報領域【最近の研究テーマ】●暗号通貨の資金洗浄の追跡●匿名化ネットワークの利用先の特定ソフトウェア設計図を検証して安全なソフトウェア開発
元のページ ../index.html#65