研究課題

検証進化可能電子社会の実現のために，以下の研究を行う．

（1）法令文書の論理表現と推論（安心性要件の検証グループ）

電子社会の仕様が法令や規則よって与えられることに着目し，自然言語によって書かれた法令文からの法令論理表現への変換，論理表現からの推論と解析を通して，電子社会の形式仕様を獲得する研究を行う．条例や法令を対象にした「要件-効果」構造分析と様相記号を持つ論理への変換方法とその機械学習，法令の変更にともなう法令論理ベースの矛盾検出，論駁推論による矛盾の修正などの研究を併せて進める．

（2）形式推論機構（形式的仕様記述体系グループ）

形式検証のための推論機構について，その基礎および推論機構構築法に関する研究を行う．論理における証明の導出と代数における等式の導出が，代数化の概念で明確に関係付けられることを解明してきたが，証明論的方法と代数的方法の関係の研究を一層進める．また，古典論理的証明の構成的論理における証明への変換方方法のなどの研究を行う．それと同時に，定理証明技術などの推論機構の構成法や利用技術などの研究を行う．

（3）形式検証技術（検証方式グループ）

電子社会の基本構成要素であるポリシー，ドメイン，ワークフロー(プロセス)の形式記述と検証を，いくつかの重要な応用分野において展開し，包括的な検証技術を開発する．ポリシーに関しては，オブジェクト指向論理に基づくセキュリティポリシーの形式記述と検証，ドメインに関しては，電子取引ドメインのCafeOBJやVDMによる形式記述と検証，ワークフローに関しては，組織内ワークフローの規則・法令整合性，ワークフロー管理問題の形式記述と検証などの研究を行う．

（4）モデル化技術（モデル化と進化グループ）

電子社会システムを高度オブジェクト指向概念によりモデル化し，それにアカウンタビリティ機構や進化機構を組み込む研究を行う．法令文とシステム構成要素間の対応関係保持データベース，新旧法令間の整合性判定機構，法令改定のための版管理機構，多様な利害関係者からの質問に答える説明機構，説明機構をシステムに装着するアーキテクチャなどに関して，事例研究を行うと同時に理論的体系化を行う．

（5）安心基盤技術（安心要件の検証・検証方式・基盤グループ）

安心な電子社会情報システムを実現するための，種々の安心基盤技術の研究を行う．(a)暗号や電子署名などのセキュリティコア技術，特に，セキュリティシステム故障時の安全・安心技術や公開鍵暗号処理ハードウェア，(b)分散システムの耐故障技術，特に，誤りノード検出モジュール技術，インタネットシミュレータを用いたネットワーク安心性検証方式，(c)高信頼組込みソフトウェアのためのモデル検査技術やハードウェア自動合成，(d)安心ヒューマンインタフェース,　などの研究を行う．