| 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 |
| 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
| 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 | ||
| 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 | ||