Summary of Research Project Results Under the JSPS FY2000
"Research for the future Program"



1.Research Institution Japan Advanced Institute of Science and Technology
 
2.Research Area Physical and Engineering Science
 
3.Research Field Intelligent Information and Advanced Information Processing
 
4.Term of Project FY1996〜FY2000
 
5.Project Number 96P00504
 
6.Title of Project Software Development Methodology

7.Projetct Leader
Name Institution,Department Title of Position
Katayama, Takuya JAIST, School of Information Science Professor

8.Core Members

Names Institution,Department Title of Position
Futamura, Yoshihiko Waseda University, School of Science and Engineering Professor
Yonezaki, Naoki Tokyo Institute of Technology, Graduate School of Information Science and Engineering Professor
Yonezawa, Akinori University of Tokyo, School of Science Professor

9.Cooperating Researchers

Names Institution,Department Title of Position
Glueck, Robert University of Copenhagen, Dept. of Computer Science Associate Professor
Aoki, Toshiaki JAIST, School of Information Science Associate
Kobayashi, Naoki Tokyo Institute of Technology, Graduate School of Information Science and Engineering Associate Professor

10.Summary of Research Results

The following research has been done aiming at establishing scientific and formal methodologies for software development.
1. Evolutionary Software Development Methodologies: Works have been done to put object-oriented methodologies on formal foundations. We mainly worked on the analysis phase and obtained a unification mapping and consistency verification of analysis models using theorem proving approach. We also worked on the mathematical principles and mechanisms for software evolution.
2. Software Development Algorithm: Tools for developing very efficient programs are developed based on generalized partial evaluation. The environment called WSDFU has been constructed for the purpose, together with random data generator for evaluating efficiency and reliability of programs. Also, automatic program execution time estimator has been implemented.
3. Formal Techniques and Environment for Software Development: Several logical systems for specifying and verifying reactive systems have been studied. Also a specification language for reactive systems has been designed based on the logics. Provers for the logics have been designed and implemented and their optimization has been studied, and environment for verifying specification in the language has been constructed.
4. Open Parallel and Distributed Software: Theories and languages for designing and implementing mobile software on the basis of safe mobile codes have been studied. We obtained an efficient procedural language and implemented its language system. Using the language, software dispatching system over the Internet has been constructed.

11.Key Words

(1)software development、(2)software evolution、(3)object-oriented methodologies
(4)theorem proving、(5)algorithm、(6)program optimization
(7)partial evaluation、(8)verification、(9)mobile code

12.References

[Reference Articles]
Author Title of Article
Takuya Katayama A Theoretical Framework of Software Evolution
Journal Volume Year Pages Concerned
IWPSE'98   1998 1-5

Author Title of Article
Nobukazu Yoshioka Incremental Software Development Method based on Abstract Interpretation
Journal Volume Year Pages Concerned
IWSSD'98   1998 126-134

Author Title of Article
Toshiaki Aoki Formal Model Approach for Reliable Object-Oriented Information System Design
Journal Volume Year Pages Concerned
Sci/ISAS'98   1998 228-235

Author Title of Article
Toshiaki Aoki Unification and Consistency Verification of Object-Oriented Analysis Models
Journal Volume Year Pages Concerned
ASPEC'98   1998 296-303

Author Title of Article
Toshiaki Aoki How to support verification object-oriented analysis models using HOL
Journal Volume Year Pages Concerned
Sci/ISAS'99   1999 525-532

Author Title of Article
Takaaki Tateishi An Axiomatic System For Verifying The Object-Oriented Analysis Model
Journal Volume Year Pages Concerned
SCI2000   2000 662-667

Author Title of Article
Kei Itou Evolution of Object System by Rewriting Behavior Expressions
Journal Volume Year Pages Concerned
IWPSE'99   1999 113-117

Author Title of Article
Kei Itou A Characterization of Inter-Object Behavior for High Reliability Systems
Journal Volume Year Pages Concerned
ISAS'99 Vol.1 1999 554-561

Author Title of Article
Kei Itou Evolutionary Development of Object Behaviors
Journal Volume Year Pages Concerned
ISPE2000   2000 65-74

Author Title of Article
Adel Cherif A Replication Technique Based on a Functional and Attribute Grammar Computation Model
Journal Volume Year Pages Concerned
ISSRE'96   1996 266-273

Author Title of Article
Adel Cherif A Nobel Replication Technique for Detecting and Masking Failures For Parallel Software: Active Parallel Replication
Journal Volume Year Pages Concerned
IEICE Transactions on Information and Systems E80-D,No.9 1997 886-892

Author Title of Article
Adel Cherif Replica Management for Fault-Tolerant Systems
Journal Volume Year Pages Concerned
IEEE Micro Special Issue on Fault Tolerance Vol.18,Num.5 1998 54-65

Author Title of Article
Yoshihiko Futamura Partial Evaluation of Computation Process - An approach to a Compiler-Compiler
Journal Volume Year Pages Concerned
Higher-Order and Symbolic Computation Vol.12 1999 381-391

Author Title of Article
Yoshihiko Futamura Partial Evaluation of Computation Process Revisited
Journal Volume Year Pages Concerned
Higher Order and Symbolic Computation Vol.12 1999 377-380

Author Title of Article
Song Litong Loop Quasi-Invariance Code Motion
Journal Volume Year Pages Concerned
IEICE Transactions on Information & System Vol.E83-D,No.10 2000 1841-1850

Author Title of Article
Pavlin Ivanov Radslavov An Algorithm for Cost-Delay Balanced Trees and Its Application to Wide Area Network Multicast
Journal Volume Year Pages Concerned
Lecture Notes in Computer Science 1274 1997 294-308

Author Title of Article
Yoshiaki Minamisawa A New semantics for Linear Logic and its Completeness
Journal Volume Year Pages Concerned
Information modeling and knowledge bases VIII 1997 155-166

Author Title of Article
Shigeki Hagihara A Connection based proof method for Modal logic restricted to Discrete frames
Journal Volume Year Pages Concerned
Poster Session Abstracts, Fifteenth International Joint Conference on, Artificial Intelligence   1997 43

Author Title of Article
Shigeki Hagihara Resolution Method for Modal Logic with Well-founded Frames
Journal Volume Year Pages Concerned
Proc. of the Annual Conference of the European Association for Computer Science Logic (CSL'99), Lecture note in Computer   1999 277-291

Author Title of Article
Sima Asgari A general Object-Oriented Model for Spatial Data
Journal Volume Year Pages Concerned
Third International Conference on Perspectives of System Informatics   1999 245-250

Author Title of Article
Takenobu Aoshimna An efficient tableau-based verification method with partial evaluation for reactive system specifications
Journal Volume Year Pages Concerned
Proc. of The 10th European-Japanese Conf. on Information Modelling and Knowledge Bases   2000 337-348

Author Title of Article
Noriaki Yoshiura Program synthesis for stepwise satisfiable specification of reactive system
Journal Volume Year Pages Concerned
International Sympo. on Principles of Software Evolution ISPSE2000   2000 55-64

Author Title of Article
Kazuyoshi Negishi Verification method for possibility of parallel attack on multiple sessions with the same principals in a security protocol
Journal Volume Year Pages Concerned
Informal proceeding of Formal Method on Computer Security 2000   2000 109-120

Author Title of Article
Motoshi Saeki Supporting Tool for Assembling Software Specification and Design Methods
Journal Volume Year Pages Concerned
Proc. of the 24th Annual International Computer Software & Applications Conference (COMPSAC00)   2000 419-428

Author Title of Article
Tatsuro Sekiguchi A Calculus with Code Mobility
Journal Volume Year Pages Concerned
In Proceedings of Second IFIP International Conference on Formal Methods for Open Object-based Distributed Systems   1997 21-36

Author Title of Article
Naoki Kobayashi A Partially Deadlock-Free Typed Process Calculus
Journal Volume Year Pages Concerned
In ACM Transactions on Programming Languages and Systems vol.20,no.2 1998 436-482

Author Title of Article
Naoki Kobayashi Distributed Concurrent Linear Logic Programming
Journal Volume Year Pages Concerned
In Theoretical Computer Science (Special Issues on Linear Logic) vol.227 1999 185-220

Author Title of Article
Tatsuro Sekiguchi A Simple Extension of Java Language for Controllable Transparent Migration and its Portable Implementation
Journal Volume Year Pages Concerned
In Proceedings of 4th International Conference on Coordination Languages and Models (COODINATION99) vol.1594 of Springer LNCS 1999 221-226

Author Title of Article
Naoki Kobayashi Quasi-Linear Types
Journal Volume Year Pages Concerned
In Proceedings of ACM Conference on Principles of Programming Languages (POPL'99)   1999  

Author Title of Article
Masatomo Hashimoto A Typed Context Calculus
Journal Volume Year Pages Concerned
Technical Report, Research Institute for Mathematical Science, To appear in TCS no.RIMS-1908 1996  

Author Title of Article
Takahiro Sakamoto Bytecode Transformation for Portable Thread Migration in Java
Journal Volume Year Pages Concerned
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  

Author Title of Article
Masatomo Hashimoto MobileML:A Programming Language for Mobile Computation
Journal Volume Year Pages Concerned
In Proceedings of 4th International Conference on Coordination Languages and Models (COORDINATION 2000) vol.1906 of Springer LNCS 2000 198-215

Author Title of Article
Hiroshi Yamauchi Wrapping Class Libraries for Migration-Transparent Resource Access by Using Compile-Time Reflection
Journal Volume Year Pages Concerned
In Proceedings of Workshop on Reflective Middleware 2000      

Author Title of Article
Atsushi Igarashi Type Reconstruction for Linear Pi-Calculus with I/O Subtyping
Journal Volume Year Pages Concerned
In Information and Computation vol.161 2000 1-44

Author Title of Article
Naoki Kobayashi An Implicity-Typed Deadlock-Free Process Calculus
Journal Volume Year Pages Concerned
In Proceedings of CONCUR2000 vol.1877 of Springer LNCS 2000 489-503

Author Title of Article
Tatsurou Sekiguchi Portable Implementation of Continuation Operators in Imperative languages by Exception Handling
Journal Volume Year Pages Concerned
Advances in Exception Handling Techniques (to appear) Springer LNCS 2001  

[Reference Books]
Author Title of Book
Adel Cherif Kluwer Academic Publishers, Fault Tolerant Parallel and Distributed Systems
Publisher Year Pages
A Novel Replication Technique for Implementing Fault-Tolerant Parallel Software, Chapter 22 1998  

Author Title of Book
Masumi Toyoshima Kluwer Academic Publishers, Dependable Network Computing
Publisher Year Pages
Implementing Fault Tolerant Software In Distributed Environment, Chapter 15 2000  


back