1991 Fiscal Year Annual Research Report
様相構造記述言語を用いるリアクティブシステム構成法の研究
| Project/Area Number |
03680027
|
|---|
| Research Institution | Japan Advanced Institute of Science and Technology |
|---|
Principal Investigator |
米崎 直樹 北陸先端科学技術大学院大学, 情報科学研究科, 教授 (00126286)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
徳田 雄洋 東京工業大学, 工学部・情報工学科, 助教授 (30111644)
|
|---|
| Keywords | 仕様記述 / 定理証明 / オブジェクトベ-ス / 実行可能仕様 / 統一化 / 実現可能性 |
|---|
| Research Abstract |
実時間で外界の要求に応じて動作するリアクティブシステムの仕様獲得と、その実現について以下の研究成果を得た。
1仕様記述からのシステムの実現に関する研究
仕様記述は一般に不十分でまた矛盾を含み、そのままでは実現不能であることが多い。ここでは実現不能なシステムに関するクラス分けを行ないその階層構造を明らかにした。また実現可能なクラスの仕様に関してその実現を求める手続きを実現し、いくつかの仕様について実験を行なった。その結果効率改善の必要性を認識し、改善工夫を行なった結果、小規模の組み込みシステムについては本方式が実際的であることを確認した。
2様相論理定理証明方式の研究
様相構造を用いて記述されたシステムは、ある種の多重様相論理式としての表現に変化される。この様な表現を用いて形式的にシステムの無矛盾性等を検証するために、新しい効率的定理証明方法を与えた。すなわち様相記号列の統一化を用いる方法で式の重複を制限する手段として、ある制約された自己代入を許すことにより大幅に証明効率の改善が計れることを示した。またこのような自己代入の制約に関して証明システムが健全で完全であることの厳密な証明を与えた。
3仕様のデ-タベ-スに関する研究
仕様デ-タベ-スは通常のデ-タベ-スとは異なり、対話的な更新とその更新に従って関連するデ-タの変更が生じる点において通常のデ-タベ-スとは異なる。この点について必要な機能とその実現方法について検討を行なった。特にオブジェクトベ-スとしての機能が重要となるが、その効率的処理の現際的解決策として、既存の関係デ-タベ-ス技術を活用するために、オブジェクトベ-スから関係デ-タベ-スへの変換方式を与えた。
|
Research Products
(6 results)
-
[Publications] Naoki YONEZAKI: "Selfーsubstitution in Model unification" The second European Japanese Seminor on Information Modelling and Knowledge bases.
-
[Publications] Naoki YONEZAKI: "ID/LP Logic for Hierarchical Specification of Precedence Relation" Theoretical Foundation of Knowledge Information Processing;ASRーSESITY,INOGRA. 137-145 (1990)
-
[Publications] Naoki YONEZAKI: "Conceputual Modelling in MSL" Advances in Information Modeling and Knowledge Bases;IOS Press. 124-140 (1991)
-
[Publications] 宮川 晋: "MSLによる仕様記述のコンパイル方式" 日本ソフトウェア科学会第8回大会論文集. 329-332 (1991)
-
[Publications] Takehiro Tokuda: "Research Topics of Interactive Document Systems" Proc.of 3rd Symp.on Software Engineering and Computer Graphics,Univ.of Washington. 1-4 (1991)
-
[Publications] Rilada Tiranaswasdi: "A Method for Constructing Equivalent ObjectーOriented Databases from Existing Relational Databases" オブジェクトテクノロジ-の高度応用に関するワ-クショップ予稿集. 181-188 (1992)
