研究紹介
埼玉大学 工学部 情報システム工学科 吉浦研究室

Last Update ($Date: 2015/09/14 04:58:05 $)


吉浦研究室は、理論計算機科学、特に、論理学をベースにした ソフトウェア工学へのアプローチを行っています。 また、理論的な研究だけではなく、 コンピュータネットワーク、コンピュータセキュリティ、 コンピュータを応用した情報システムなどの 実用面を重視した研究を行っています。 以下が、現在、吉浦研究室で行っている研究内容です。

1. 仕様の検証

ソフトウェアが社会インフラとなっている今日では、不具合のないソフトウェアの構築やソフトウェアの不具合の検出は極めて重要です。ソフトウェアの不具合にはバッファオーバーフローなどのプログラミングが原因となるもののほかに、ソフトウェアの設計が原因になる場合もあります。例えば、DNS(Domain Name Service)におけるキャッシュポイズニングなどはプログラミングの問題ではなくプロトコルやソフトウェアの設計の問題といえます。ソフトウェアの設計は様々なレベルがありますが、ソフトウェア仕様がソフトウェアの基本設計書となります。

一方、社会インフラとなっているソフトウェアのほとんどはリアクティブシステムと呼ばれるシステムに関するソフトウェアです。リアクティブシステムとは飛行機の制御プログラム、オペレーティングシステム、銀行のATMなど、ユーザとインタラクションをしながらサービスを提供し動作するシステムの総称です。

リアクティブシステムの構築やその検証のためには仕様が重要であり、仕様を形式的言語で記述することでプログラムの合成や検証を形式的手法により行うことができます。その形式的言語の1つとして時間論理があり、SMVやSPINなど時間論理に基づいたプログラムの検証ツールが提案されています。

現在、SMVやSPINでプログラムの検証を行うための仕様は簡単なものが対象です、今後複雑な記述で表現される仕様を検証する場合、仕様自体に誤りがないかを判定することが重要となります。特に、仕様を満たすプログラムが存在しない場合、プログラムが仕様を満たすか否かを検証すること自体が無駄になってしまいます。

一方、時間論理により記述されたリアクティブシステム仕様を満たすプログラムが存在するか否か(プログラム化可能性)の判定やプログラムの合成の研究が行われており、Lilyなどのツールが提案されています。数値計算プログラムと異なり、リアクティブシステムの制御プログラムの場合、ユーザとのインタラクションを伴って動作し、さらに、ユーザの動作を制御することができないため、仕様を安易に記述すると、仕様を満たすプログラムが存在しないことが容易に起きてしまいます。簡単な例を一つ上げます。リアクティブシステムの1つであるエレベータの仕様が以下の要件を持つ場合、仕様を満たすプログラムは存在しません。

  1. 5階で利用者が「下がるボタン」を押したならば、いつかエレベータが5階に到着する。
  2. 利用者がエレベータ内の「ドアを開くボタン」を押したならば、ドアは開く。
  3. ドアが開いている間、エレベータは動かない。

どのようなプログラムでもこの仕様を満たすためには、「ドアを開くボタン」を利用者が押し続ける場合、エレベータは動くことができず、5階にいる利用者が「下がるボタン」を押しても5階にエレベータが到着することはなく、結局仕様を満たすことができません。この仕様には「ドアを開くボタン」が押され続けることがないという暗黙の前提があり、仕様には明確に記述されていません。このように仕様がプログラム化可能であるか否かを判定することは仕様の不備や暗黙の前提を見つけることでもあり、仕様からプログラムを合成するためにも必要です。

仕様のプログラム化可能性を判定する方法やプログラムを合成する方法は既に提案されています。しかし、これらの方法はオートマトン理論に基づいており、膨大な計算時間とメモリを必要とし、実用的とは言えません。吉浦研究室では、プログラムの存在判定の高速化を行い実用的なものに近づけることを目指しています。

具体的には、時間論理で記述されたリアクティブシステム仕様を満たすプログラムが存在するか否か、つまりリアクティブシステム仕様(以後、仕様)のプログラム化可能性を高速で判定するための方法を構築し、仕様からのプログラムの合成の方法を構築することを目指しています。より詳細に述べると、以下のような研究を行っています。

2. 検索エンジンの傾向分析やWebに関する研究

インターネット上の膨大な情報から取り出すために検索エンジンは今や必要不可欠であり、ビジネスにおいては、商品名の検索結果の上位に会社のホームページが表示されるかは死活問題です。このように検索結果の表示順序は現代社会において重要です。一方、検索エンジンは検閲だけではなく検索結果の表示順序を操作することで情報操作することが可能です。よって、検索エンジンの検索結果の表示順序をチェックすることは、テレビや新聞などのメディアが情報操作をしていないことをチェックすることと同様に重要です。

そこで、吉浦研究室では、検索エンジンの傾向分析について研究しています。これまでに、検索エンジンの検索結果の分析に関する研究は、複数の検索エンジン間の検索結果の違いの比較により、日本国内で、Googleにより検索対象外となったWebページを発見するシステムの開発などを行ってきました。

しかし、検索エンジンの傾向を分析するためには、他のエンジンとの比較によるだけでは十分とは言えません。そこで、検索エンジンをどのようにすれば分析できるかという言に取り組んでいます。そのため、Webに関する様々な研究を行っています。例えば、Webページの特徴や独自性を発見するシステムの開発を行っています。

3. 監視カメラシステムとプライバシー

監視カメラは広く普及しており、現在では犯罪捜査にとって必要不可欠になっている。今後、監視カメラは、街路灯と同程度かそれ以上の密度で設置されていくであろう。実際に、ロンドンなどでは相当数の監視カメラが設置されている。監視カメラは被撮影者の意思に関わらず撮影を行うが、被撮影者のプライバシーを守ることが監視カメラの課題です。

そこで、吉浦研究室では群馬大学の藤井研究室などと共同で、被撮影者のプライバシー保護機能を持つ監視カメラの開発を行っており、一部は製品化されています。 また、監視カメラの開発や関連技術の特許出願もしています。 詳しくは、吉浦が副理事長を務めているe自警ネットワーク研究会のホームページをご覧ください。

4. スマート街路灯

現在、街路灯は全世界で1億個あるとも、10億個あるとも言われているが、その正確な総数は知られていません。仮に1億個街路灯があり、すべてがLEDで1個当たり20Wを消費し、その1/2が常に点灯していると仮定すると、年間8760GWhの電力が消費されています。これは日本の年間消費量の約0.8% にあたります。今後、発展途上国において街路灯設置の需要が爆発的に増えていくことを考慮すれば、街路灯の省エネルギー化は温室効果ガスの削減に必要です。

国内に1000万灯あると言われる街路灯のうち、多くが、照度センサのみで制御され、閑静な住宅街等においても終夜、点灯している。特に、深夜以降、歩行者・車の通行が皆無に近い状態になる住宅街等でこのような街路灯が使われていることは、省エネルギーの観点から、膨大なエネルギーの無駄使いと言えます。

そこで、吉浦研究室では群馬大学の藤井研究室などと共同で、省エネ街路灯の開発や関連技術の特許出願もしています。

5. コンピュータネットワーク

インターネットは今や社会にとって必要不可欠なものとなっています。吉浦研究室では、その基盤となるコンピュータネットワークに関する研究を行っています。特に運用面に関する研究を行っています。最近では、OpenFlowなどSoftware Defined Networkingが話題となっていますが、これを利用したネットワーク運用の効率化や安定運用に関する研究を行っています。ここでは、次のような研究課題があります。

研究業績

ここを参考にしてください。
お問い合わせは、 wwwadmin@fmx.ics.saitama-u.ac.jpへお願いします。