ソフトウェア仕様の安全性検査とソフトウェアの自動合成
キーワード： 仕様 検証 ソフトウェア 自動合成 安全性
飛行機の制御プログラムや銀行のATM など社会インフラであるソフトウェアは、ユーザとやりとりをしながらサービスを提供するシステムです。このようなシステムはリアクティブシステムと呼ばれています。 リアクティブシステムの構築や検証にはその設計図となる仕様が重要です。仕様通りにソフトウェアが稼働するかを検証することでソフトウェアの安全性を確保します。しかし、仕様自体に不備や不整合があると、検証自体無駄になってしまいます。そこで、仕様自体に誤りがないかを調べる研究を行っています。特に、仕様に様々なソフトウェアに対する要求が含まれてしまうと、ソフトウェアが存在しないこともあります。そこで、仕様通りに稼働するソフトウェアが存在するかを調べる研究も行っています。 その発展として、仕様からソフトウェアを自動合成する研究も行なっています。自動合成することで効率的に安全なソフトウェアを作ることができます。
- 企業：埼玉大学 オープンイノベーションセンター
- 価格：応相談
