平成１２年度未来開拓学術研究推進事業研究成果報告書概要


１．研究機関名　北陸先端科学技術大学院大学
　
２．研究領域　理工
　
３．研究分野　知能情報・高度情報処理
　
４．研究期間　平成8年度〜平成12年度
　
５．研究プロジェクト番号　96P00504
　
６．研究プロジェクト名　ソフトウェア開発方法論

７．プロジェクト・リーダー
プロジェクト・リーダー名 フリガナ 所属部局名 職名
片山　卓也 カタヤマ　タクヤ 情報科学研究科 教授

８．コア・メンバー

コア・メンバー名 フリガナ 所属研究機関名・所属部局名 職名
二村　良彦 フタムラ　ヨシヒコ 早稲田大学・理工学部 教授
米崎　直樹 ヨネザキ　ナオキ 東京工業大学・大学院情報理工学研究科 教授
米澤　明憲 ヨネザワ　アキノリ 東京大学・大学院理学系研究科 教授

９．研究協力者

研究協力者名 フリガナ 所属研究機関名・所属部局名 職名
Robert Glueck ロバート　グリュック コペンハーゲン大学・計算機科学部 助教授
青木　利晃 アオキ　トシアキ 北陸先端科学技術大学院大学・情報科学研究科 助手
小林　直樹 コバヤシ　ナオキ 東京工業大学・大学院情報理工学研究科 助教授

１０．研究成果の概要

本プロジェクトでは科学的・形式的手法にもとづくソフトウェア開発方法論をに焦点をあて以下の研究を行なった。
　「発展的ソフトウェア開発方法論」オブジェクト指向分析を形式的基盤のうえに展開するための研究を行ない、形式的分析モデルと統合モデル、統合モデル実行システム、定理証明システムによる分析モデル一貫性検証に関して、先進的な研究成果を得た。また、構成されたソフトウェアの発展や、ソフトウェアを発展的に構成するための原理やメカニズムについて、代数的な束による発展原理を発見し、また、抽象解釈にもとづく新しい発展メカニズムを得た。
　「ソフトウェア開発アルゴリズム」効率の良いプログラムを開発するためのプログラム開発ツール、プログラミング方法論およびプログラム評価システムを部分計算機構に基づき開発することを目的として、プログラムの自動超高速化システムWSDFUの開発に成功した。また、プログラムの性能および信頼性を評価するためのテストデータの自動生成ソフトウェア、プログラムの計算時間を自動評価するソフトウェア等を開発し、WWW上で公開した。
　「ソフトウェア開発における形式化技術と環境」リアクティブシステムでは、その仕様の検証が極めて重要である。本研究では、検証の基礎となる論理体系、このよな体系を用いて仕様の様々な検証を行なうための検証技法とその理論的裏付け、実際の問題がこのような形式言語で記述可能となるよう仕様記述言語の設計、この言語構造を基にした効率的検証方法・システムの構築を行なった。
　「解放性をもつ並行・分散ソフトウェア」移動コード技術に基づいた安全なモバイルソフトウェアを効率的に開発するためのプログラミング言語系の理論・実装技術の研究を行なってきた。従来型の言語系による効率的な開発は困難とされてきたが、本研究の成果として、安全なモバイルソフトウェアを効率的に開発するための新しい言語系を構成した。さらにその成果を応用し、次世代ソフトウェア配信システムの開発に成功した。

１１．キーワード

(1)ソフトウェア開発方法論、(2)ソフトウェア発展、(3)オブジェクト指向方法論
(4)定理証明、(5)アルゴリズム、(6)プログラム最適化
(7)部分評価、(8)検証、(9)移動コード

１２．研究発表（印刷中も含む）

[雑誌論文]
著者名 論文標題
Takuya Katayama A Theoretical Framework of Software Evolution
雑誌名 巻 発行年 ページ
IWPSE'98 　 1998 1-5

著者名 論文標題
Nobukazu Yoshioka Incremental Software Development Method based on Abstract Interpretation
雑誌名 巻 発行年 ページ
IWSSD'98 　 1998 126-134

著者名 論文標題
Toshiaki Aoki Formal Model Approach for Reliable Object-Oriented Information System Design
雑誌名 巻 発行年 ページ
Sci/ISAS'98 　 1998 228-235

著者名 論文標題
Toshiaki Aoki Unification and Consistency Verification of Object-Oriented Analysis Models
雑誌名 巻 発行年 ページ
ASPEC'98 　 1998 296-303

著者名 論文標題
Toshiaki Aoki How to support verification object-oriented analysis models using HOL
雑誌名 巻 発行年 ページ
Sci/ISAS'99 　 1999 525-532

著者名 論文標題
Takaaki Tateishi An Axiomatic System For Verifying The Object-Oriented Analysis Model
雑誌名 巻 発行年 ページ
SCI2000 　 2000 662-667

著者名 論文標題
Kei Itou Evolution of Object System by Rewriting Behavior Expressions
雑誌名 巻 発行年 ページ
IWPSE'99 　 1999 113-117

著者名 論文標題
Kei Itou A Characterization of Inter-Object Behavior for High Reliability Systems
雑誌名 巻 発行年 ページ
ISAS'99 Vol.1 1999 554-561

著者名 論文標題
Kei Itou Evolutionary Development of Object Behaviors
雑誌名 巻 発行年 ページ
ISPE2000 　 2000 65-74

著者名 論文標題
Adel Cherif A Replication Technique Based on a Functional and Attribute Grammar Computation Model
雑誌名 巻 発行年 ページ
ISSRE'96 　 1996 266-273

著者名 論文標題
Adel Cherif A Nobel Replication Technique for Detecting and Masking Failures For Parallel Software: Active Parallel Replication
雑誌名 巻 発行年 ページ
IEICE Transactions on Information and Systems E80-D,No.9 1997 886-892

著者名 論文標題
Adel Cherif Replica Management for Fault-Tolerant Systems
雑誌名 巻 発行年 ページ
IEEE Micro Special Issue on Fault Tolerance Vol.18,Num.5 1998 54-65

著者名 論文標題
Yoshihiko Futamura Partial Evaluation of Computation Process - An approach to a Compiler-Compiler
雑誌名 巻 発行年 ページ
Higher-Order and Symbolic Computation Vol.12 1999 381-391

著者名 論文標題
Yoshihiko Futamura Partial Evaluation of Computation Process Revisited
雑誌名 巻 発行年 ページ
Higher Order and Symbolic Computation Vol.12 1999 377-380

著者名 論文標題
Song Litong Loop Quasi-Invariance Code Motion
雑誌名 巻 発行年 ページ
IEICE Transactions on Information & System Vol.E83-D,No.10 2000 1841-1850

著者名 論文標題
Pavlin Ivanov Radslavov An Algorithm for Cost-Delay Balanced Trees and Its Application to Wide Area Network Multicast
雑誌名 巻 発行年 ページ
Lecture Notes in Computer Science 1274 1997 294-308

著者名 論文標題
Yoshiaki Minamisawa A New semantics for Linear Logic and its Completeness
雑誌名 巻 発行年 ページ
Information modeling and knowledge bases VIII 1997 155-166

著者名 論文標題
Shigeki Hagihara A Connection based proof method for Modal logic restricted to Discrete frames
雑誌名 巻 発行年 ページ
Poster Session Abstracts, Fifteenth International Joint Conference on, Artificial Intelligence 　 1997 43

著者名 論文標題
Shigeki Hagihara Resolution Method for Modal Logic with Well-founded Frames
雑誌名 巻 発行年 ページ
Proc. of the Annual Conference of the European Association for Computer Science Logic (CSL'99), Lecture note in Computer 　 1999 277-291

著者名 論文標題
Sima Asgari A general Object-Oriented Model for Spatial Data
雑誌名 巻 発行年 ページ
Third International Conference on Perspectives of System Informatics 　 1999 245-250

著者名 論文標題
Takenobu Aoshimna An efficient tableau-based verification method with partial evaluation for reactive system specifications
雑誌名 巻 発行年 ページ
Proc. of The 10th European-Japanese Conf. on Information Modelling and Knowledge Bases 　 2000 337-348

著者名 論文標題
Noriaki Yoshiura Program synthesis for stepwise satisfiable specification of reactive system
雑誌名 巻 発行年 ページ
International Sympo. on Principles of Software Evolution ISPSE2000 　 2000 55-64

著者名 論文標題
Kazuyoshi Negishi Verification method for possibility of parallel attack on multiple sessions with the same principals in a security protocol
雑誌名 巻 発行年 ページ
Informal proceeding of Formal Method on Computer Security 2000 　 2000 109-120

著者名 論文標題
Motoshi Saeki Supporting Tool for Assembling Software Specification and Design Methods
雑誌名 巻 発行年 ページ
Proc. of the 24th Annual International Computer Software & Applications Conference (COMPSAC00) 　 2000 419-428

著者名 論文標題
Tatsuro Sekiguchi A Calculus with Code Mobility
雑誌名 巻 発行年 ページ
In Proceedings of Second IFIP International Conference on Formal Methods for Open Object-based Distributed Systems 　 1997 21-36

著者名 論文標題
Naoki Kobayashi A Partially Deadlock-Free Typed Process Calculus
雑誌名 巻 発行年 ページ
In ACM Transactions on Programming Languages and Systems vol.20,no.2 1998 436-482

著者名 論文標題
Naoki Kobayashi Distributed Concurrent Linear Logic Programming
雑誌名 巻 発行年 ページ
In Theoretical Computer Science (Special Issues on Linear Logic) vol.227 1999 185-220

著者名 論文標題
Tatsuro Sekiguchi A Simple Extension of Java Language for Controllable Transparent Migration and its Portable Implementation
雑誌名 巻 発行年 ページ
In Proceedings of 4th International Conference on Coordination Languages and Models (COODINATION99) vol.1594 of Springer LNCS 1999 221-226

著者名 論文標題
Naoki Kobayashi Quasi-Linear Types
雑誌名 巻 発行年 ページ
In Proceedings of ACM Conference on Principles of Programming Languages (POPL'99) 　 1999 　

著者名 論文標題
Masatomo Hashimoto A Typed Context Calculus
雑誌名 巻 発行年 ページ
Technical Report, Research Institute for Mathematical Science, To appear in TCS no.RIMS-1908 1996 　

著者名 論文標題
Takahiro Sakamoto Bytecode Transformation for Portable Thread Migration in Java
雑誌名 巻 発行年 ページ
In Proceedings of Second International Symposium on Agent Systems and Applications and Fourth International Symposium on Mobile Agents (ASA/MA2000) vol.1882 of Springer LNCS 2000 　

著者名 論文標題
Masatomo Hashimoto MobileML:A Programming Language for Mobile Computation
雑誌名 巻 発行年 ページ
In Proceedings of 4th International Conference on Coordination Languages and Models (COORDINATION 2000) vol.1906 of Springer LNCS 2000 198-215

著者名 論文標題
Hiroshi Yamauchi Wrapping Class Libraries for Migration-Transparent Resource Access by Using Compile-Time Reflection
雑誌名 巻 発行年 ページ
In Proceedings of Workshop on Reflective Middleware 2000 　 　 　

著者名 論文標題
Atsushi Igarashi Type Reconstruction for Linear Pi-Calculus with I/O Subtyping
雑誌名 巻 発行年 ページ
In Information and Computation vol.161 2000 1-44

著者名 論文標題
Naoki Kobayashi An Implicity-Typed Deadlock-Free Process Calculus
雑誌名 巻 発行年 ページ
In Proceedings of CONCUR2000 vol.1877 of Springer LNCS 2000 489-503

著者名 論文標題
Tatsurou Sekiguchi Portable Implementation of Continuation Operators in Imperative languages by Exception Handling
雑誌名 巻 発行年 ページ
Advances in Exception Handling Techniques (to appear) Springer LNCS 2001 　

[図書]
著者名 出版者
Adel Cherif A Novel Replication Technique for Implementing Fault-Tolerant Parallel Software, Chapter 22
書名 発行年 総ページ数
Kluwer Academic Publishers, Fault Tolerant Parallel and Distributed Systems 1998 　

著者名 出版者
Masumi Toyoshima Implementing Fault Tolerant Software In Distributed Environment, Chapter 15
書名 発行年 総ページ数
Kluwer Academic Publishers, Dependable Network Computing 2000 　

戻る