研究テーマ の変更点
Top/研究テーマ
- 追加された行はこの色です。
- 削除された行はこの色です。
- 研究テーマ へ行く。
* 研究テーマ [#y042e539]
//ソフトウェア科学、つまりプログラムの科学に興味があります。例えば、
「''誤りのない''」ソフトウェアを「''なるべく容易に''」作成するための方法について研究しています。例えば、
+ プログラムに誤りがないことをどう確かめたらよいか?
+ わかりやすい書き方で仕様を書けば、あとは自動的にプログラムを生成できないか?（あるいは、なるべく簡便な方法でプログラミングできないか?）
といった問題に最も興味があります。「''検証''」「''形式的仕様記述''」「''自動生成''」等がキーワードです。
実際は、プログラムの「正しさを保証すること」、プログラミングの「容易化」「自動化」、などに関係することは幅広く何でも研究テーマの候補と考えています。
//例えば「簡便なプログラミング」に関して、携帯電話機だけで操作できるプログラミング環境などにも興味があります。
#ref(researchtopics.png)
- [[検証について少し詳しく>研究テーマ/検証]]
//**専攻との関係 [#m7d4cffe]
//***コンピュータサイエンス専攻(CS) [#sbb62c5b]
//コンピュータにさせたい動作の仕様（つまりプログラム）をどのように記述するか、どのように実行するか、はコンピュータサイエンスの根本的問題の一つです。また、上記で挙げた問題は、オートマトン理論、形式言語理論、計算不可能性の理論などの基礎理論と深い関係にあり、これらの知識が問題を解くのにおおいに役立ちます。
//:キーワード|プログラム言語，言語処理系，形式言語理論，意味論，オートマトン，計算可能性，アルゴリズム，論理体系
//***情報通信専攻(CC) [#e75f8c3d]
//通信プロトコルの検証（デッドロックが発生しないか、等）は古くから研究されています。検証技術自体は基本的に、通信プロトコルに対しても通常のプログラムに対しても同じです。ただし、保証したい性質に合わせて検証方法も工夫する必要があります。
//また、分散処理プログラムの検証や自動生成にも興味があります。
//:キーワード|プロトコル，オートマトン，分散処理，検証
//***情報とメディア専攻(iMedia) [#e6a26151]
//プログラムに関する情報をわかりやすく提示したり、直感的な記述方法等を用いたりすることで、開発者を支援できないかと考えています。
//また、XML等の木構造データは形式言語理論にも関係が深く、「プログラムの検証法」を応用して「XMLを処理するアルゴリズム」が得られたり、その逆ができたりすることがあります。そのような、コンピュータサイエンスの基礎理論上の技術を使ってデータ（つまりメディア）を処理する方法についても興味があります。
//:キーワード|情報視覚化，ソフトウェア開発支援環境，XML(木構造データ)
//**広い意味でのプログラム [#m025dd83]
//通常の汎用プログラム言語によるプログラムだけでなく、以下のような広い意味での「プログラム」も対象としています。
//- ''XML''処理言語（XPath, XSLT）で書かれた問い合わせやデータ変換。
//- ''アクセス制御ポリシー''記述言語（XACMLなど）で書かれたポリシー。アクセス制御とは、例えば「読み出しは誰でもできるが、変更はデータ作成者にしかできない」のように、特定の操作を特定の人にだけ許可する機能のことです。どのようなときに許可するかという規則を書いたものをポリシーと言います。
//#br
//また、以下のような、汎用プログラム言語に対する新しい機能にも興味があります。
//- 実行履歴に基づくアクセス制御（''HBAC''）。特定のメソッドの実行を許すかどうかを、それまでの実行系列に基づいて判断するという仕組みのことです。例えばJavaのsandboxモデルは、HBACの一種である「スタック検査」という機能を使って実装されています。
//- ''アスペクト指向''プログラミング。複数のクラスにまたがる機能を簡潔に記述するために、「アスペクト」という新しい記述単位を用いるプログラミング技術です。
//#br
//上記のような、広い意味のプログラムや新しい機能を使ったプログラムに対して、「誤りなく」「簡便に」「自動的に」プログラミングする方法を研究しています。
* 卒業論文 [#p4e2bba5]
- [[卒業論文>./卒業論文]]
* 主な学外発表 [#o8356cf3]
- Lamilla Alvarez & Takata. A formal verification of a subset of information-based access control based on extended weighted pushdown system, IEICE Trans. Inf. & Syst., E97-D(5), 2014, to appear.
- Lamilla Alvarez & Takata. An HBAC-based approximation for IBAC programs, [[SIN 2013:http://dl.acm.org/citation.cfm?id=2523514]], 277--281.
-Takata & Seki. Automatic generation of history-based access control from information flow specification, ATVA 2010, Lecture Notes in Computer Science 6252, 259--275.
//- Takata & Seki. Comparison of the Expressive Power of Language-based Access Control Models, IEICE Trans. Inf. & Syst., E92-D(5), 2009, to appear.
- Takata & Seki. Formal language theoretic approach to the disclosure tree strategy in trust negotiation, IEICE Trans. Inf. & Syst., E92-D(2), 200-210, 2009.
- 高田, 王, 関. 実行履歴に基づくアクセス制御の形式モデルと検証, 信学論D, J91-D(4), 847-858, 2008.
- Yagi, Takata, & Seki. A labeled transition model A-LTS for history-based aspect weaving and its expressive power, IEICE Trans. Inf. & Syst., E90-D(5), 799--807, 2007.
- Yagi, Takata, & Seki. A static analysis using tree automata for XML access control, コンピュータソフトウェア, 23(3), 51--65, 2006.
- 高田, 中村, 関. XML文書に対するアクセシビリティガイドライン適合性検証, 信学論D, J89-D(4), 705--715, 2006.
//- 池田, 高田, 関. インタラクティブシステム設計法におけるタスク図の形式的定義と形式的検証への応用, コンピュータソフトウェア, 19(2), 19--34, 2002.