saidaiseeds2016-17

63/126

埼玉大学研究シーズ集2016-17■ 研究概要■ 産業界へのアピールポイント■ 実用化例・応用事例・活用例ソフトウェア設計図を検証して、ソフトウェア開発を効率化仕様検証、ソフトウェア検証、ソフトウェア自動合成、モデル検査キーワード【最近の研究テーマ】●プライバシーを考慮した監視カメラシステムの開発●ネットワーク管理システムの開発と検証●スマート街路灯システムの開発  http://www.fmx.ics.saitama-u.ac.jp/吉浦 紀晃　准教授情報メディア基盤センター（大学院理工学研究科　数理電子情報部門）飛行機の制御プログラム、オペレーティングシステム、銀行のATMなど社会インフラであるソフトウェアは、ユーザとやりとりをしながらサービスを提供するシステムです。このようなシステムはリアクティブシステムと呼ばれています。リアクティブシステムの構築や検証にはその設計図となる仕様が重要です。仕様通りにソフトウェアが稼働するか、重要な性質を満たしているかを自動で検証する方法があり、実際、ソフトウェア検証ツールも存在します。ソフトウェア検証ツールを利用する場合、検証したい仕様や性質自体に誤りがないことは重要です。特に、仕様を満たすプログラムが存在しない場合、検証は無駄になります。この無駄を回避するためには、仕様を書いたときに、その仕様を満たすプログラムが存在するかを判定する必要があります。この判定技術は、プログラムの自動合成や仕様自体の欠陥や誤りの検出に役に立ちます。この判定技術の実用化を目指しています。●ソフトウェア作成前にソフトウェア仕様を検証することにより、システム設計段階での仕様の不備や欠陥の検出し、ソフトウェア開発の効率化が可能となる。●ソフトウェア仕様からのソフトウェアの自動合成を行うことが可能となる。この自動合成により、ソフトウェアの生成コストを下げることできるとともに、ソフトウェアの検証を行う必要がなくなる。●仕様のプログラム化可能性判定システムの構築●仕様からのプログラム自動合成システムの構築情報通信技術56