Last Update ($Date: 2015/09/14 04:58:05 $)
吉浦研究室は、理論計算機科学、特に、論理学をベースにした ソフトウェア工学へのアプローチを行っています。 また、理論的な研究だけではなく、 コンピュータネットワーク、コンピュータセキュリティ、 コンピュータを応用した情報システムなどの 実用面を重視した研究を行っています。 以下が、現在、吉浦研究室で行っている研究内容です。
一方、社会インフラとなっているソフトウェアのほとんどはリアクティブシステムと呼ばれるシステムに関するソフトウェアです。リアクティブシステムとは飛行機の制御プログラム、オペレーティングシステム、銀行のATMなど、ユーザとインタラクションをしながらサービスを提供し動作するシステムの総称です。
リアクティブシステムの構築やその検証のためには仕様が重要であり、仕様を形式的言語で記述することでプログラムの合成や検証を形式的手法により行うことができます。その形式的言語の1つとして時間論理があり、SMVやSPINなど時間論理に基づいたプログラムの検証ツールが提案されています。
現在、SMVやSPINでプログラムの検証を行うための仕様は簡単なものが対象です、今後複雑な記述で表現される仕様を検証する場合、仕様自体に誤りがないかを判定することが重要となります。特に、仕様を満たすプログラムが存在しない場合、プログラムが仕様を満たすか否かを検証すること自体が無駄になってしまいます。
一方、時間論理により記述されたリアクティブシステム仕様を満たすプログラムが存在するか否か(プログラム化可能性)の判定やプログラムの合成の研究が行われており、Lilyなどのツールが提案されています。数値計算プログラムと異なり、リアクティブシステムの制御プログラムの場合、ユーザとのインタラクションを伴って動作し、さらに、ユーザの動作を制御することができないため、仕様を安易に記述すると、仕様を満たすプログラムが存在しないことが容易に起きてしまいます。簡単な例を一つ上げます。リアクティブシステムの1つであるエレベータの仕様が以下の要件を持つ場合、仕様を満たすプログラムは存在しません。
どのようなプログラムでもこの仕様を満たすためには、「ドアを開くボタン」を利用者が押し続ける場合、エレベータは動くことができず、5階にいる利用者が「下がるボタン」を押しても5階にエレベータが到着することはなく、結局仕様を満たすことができません。この仕様には「ドアを開くボタン」が押され続けることがないという暗黙の前提があり、仕様には明確に記述されていません。このように仕様がプログラム化可能であるか否かを判定することは仕様の不備や暗黙の前提を見つけることでもあり、仕様からプログラムを合成するためにも必要です。
仕様のプログラム化可能性を判定する方法やプログラムを合成する方法は既に提案されています。しかし、これらの方法はオートマトン理論に基づいており、膨大な計算時間とメモリを必要とし、実用的とは言えません。吉浦研究室では、プログラムの存在判定の高速化を行い実用的なものに近づけることを目指しています。
具体的には、時間論理で記述されたリアクティブシステム仕様を満たすプログラムが存在するか否か、つまりリアクティブシステム仕様(以後、仕様)のプログラム化可能性を高速で判定するための方法を構築し、仕様からのプログラムの合成の方法を構築することを目指しています。より詳細に述べると、以下のような研究を行っています。
そこで、吉浦研究室では、検索エンジンの傾向分析について研究しています。これまでに、検索エンジンの検索結果の分析に関する研究は、複数の検索エンジン間の検索結果の違いの比較により、日本国内で、Googleにより検索対象外となったWebページを発見するシステムの開発などを行ってきました。
しかし、検索エンジンの傾向を分析するためには、他のエンジンとの比較によるだけでは十分とは言えません。そこで、検索エンジンをどのようにすれば分析できるかという言に取り組んでいます。そのため、Webに関する様々な研究を行っています。例えば、Webページの特徴や独自性を発見するシステムの開発を行っています。
そこで、吉浦研究室では群馬大学の藤井研究室などと共同で、被撮影者のプライバシー保護機能を持つ監視カメラの開発を行っており、一部は製品化されています。 また、監視カメラの開発や関連技術の特許出願もしています。 詳しくは、吉浦が副理事長を務めているe自警ネットワーク研究会のホームページをご覧ください。
国内に1000万灯あると言われる街路灯のうち、多くが、照度センサのみで制御され、閑静な住宅街等においても終夜、点灯している。特に、深夜以降、歩行者・車の通行が皆無に近い状態になる住宅街等でこのような街路灯が使われていることは、省エネルギーの観点から、膨大なエネルギーの無駄使いと言えます。
そこで、吉浦研究室では群馬大学の藤井研究室などと共同で、省エネ街路灯の開発や関連技術の特許出願もしています。