ソフトウェア開発の形式的な発展手法

软件开发的形式化开发方法

• 批准号: 10139236
• 负责人: 劉 少英
• 金额: $ 1.28万
• 依托单位: Hiroshima City University
• 依托单位国家: 日本
• 项目类别: Grant-in-Aid for Scientific Research on Priority Areas (A)
• 财政年份: 1998
• 资助国家: 日本
• 起止时间: 1998 至 1999
• 项目状态: 已结题
• 来源: https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-10139236/
• 关键词: ソフトウェア発展; 形式的手法; 形式的仕様; SOFL; オブジェクト指向設計; 形式的検証; 一致性と有効性; 形式的仕様のテスト

本プロジェクトの目的は、品質と信頼性の高いソフトウェアを開発するための実用的及び形式的な発展手法(evolution approach)に関する研究を行なうことである。当初の研究計画の実現に向けて,平成10年度は,以下の研究を遂行した.1. 形式的仕様を求精する既存なルールを検討し、ソフトウェア発展のためのルールを提案した。このルールでソフトウェアを漸増的に発展することの検証ができる。さらに、このルールと既存な求精のルールの関係も検討して確立した。本研究に関して,以下の論文を発表した.“An Evolution Approach for Software Development Using SOFL Methodology",in Proceedings of International Workshop on Software Evolution Process.2. SOFLという形式的仕様言語で鉄道の踏切制御システムの仕様書を作成した.このシステムは,直接,人命に係るために,絶対的な信頼性を要求される安全性が必須な(Safety Critical)システムである.これらの応用事例に適用した結果に基づき,SOFL言語及び,SOFL方法論のソフトウェア発展に関する部分を改良し、実用的な方法論を確立した。本研究に関して,以下の論文を発表した.“Applying SOFL to Specify A Railway Crossing Controller for Industry",in Proceedings of WIFT'98.3. ソフトウェア発展の一つ有効な方法は部品に基ずく(component-based)開発方法である。部品を使ってより複雑な部品を構成する手法及び作成した新しい部品の正しさを検証するルールを研究した。本研究に関して,以下の論文を発表した.“Interacting Frameworks for Catalysis",in Proceedings of Second IEEE International Conference on Formal Engineering Methods.4. ソフトウェア発展の一つ重要なことは、発展した仕様又は設計の無矛盾及び有効性の検証である。形式的証明とプログラムテストの技術を結合し、仕様又は設計の以上の二つ性質を検証する有効的な「仕様テスト」という方法を提案した。本研究に関して,以下の論文を投稿した.“Verifying Consistency and Validity of Formal Specifications by Testing",Formal Methods Congress'99.

The purpose of this paper is to conduct research on the development of practical and multi-form evolution approaches for high quality and reliability. The following research projects have been carried out since 2000:1. The form of the official refinement of the existing group to discuss, improve its development and group proposal This is the first time that the United States has made such a move. The relationship between the existing group and the existing group is established. In this paper, the following papers are presented.“An Evolution Approach for Software Development Using SOFL Methodology",in Proceedings of International Workshop on Software Evolution Process.2. SOFL is the official language of the railway and the official language of the railway. This category is direct, life-related, and absolutely reliable. Safety Critical category is required. The application of SOFL to practical applications is based on SOFL language and SOFL methodology. In this paper, the following papers are presented.“Applying SOFL to Specify A Railway Crossing Controller for Industry",in Proceedings of WIFT'98.3. A component-based approach to development of software development. Part of the composition and production of new parts of the study In this paper, the following papers are presented.“Interacting Frameworks for Catalysis",in Proceedings of Second IEEE International Conference on Formal Engineering Methods.4. The development of software is important, and the development of software is important, and the design is not contradictory and effective. The proof of the form and the technology of the design are combined, and the method of the design is proposed. The following papers were submitted for this study.“Verifying Consistency and Validity of Formal Specifications by Testing",Formal Methods Congress'99.

项目成果

Shaoying Liu: "An Evolution Approach for Software Development Using SOFL Methodology" Proceedings of International Workshop on Principles of Software Evolution,ACM Press. (1999)

刘少英：“An Evolution Approach for Software Development using SOFL Methodology”国际软件演化原理研讨会论文集，ACM出版社。

Shaoying Liu,Masahi Asuka,Kiyotoshi Komaya,Yasuaki Nakamura: "Applying SOFL to Specify A Railway Crossing Controller for Industry" Proceedings of 1998 IEEE Workshop on Industrial-strength Formal specification Techniques. (1998)

Shaoying Liu、Masahi Asuka、Kiyotoshi Komaya、Yasuaki Nakamura：“应用 SOFL 指定工业铁路道口控制器”1998 年 IEEE 工业强度正式规范技术研讨会论文集。

Kung-Kiu Lau,Shaoying Liu,Mario Ornaghi,Alan Wills: "Interacting Frameworks for Catalysis" Proceedings of Second IEEE International Conference on Formal Engineering Methods. 110-119 (1998)

Kung-Kiu Lau、Shaoying Liu、Mario Ornaghi、Alan Wills：第二届 IEEE 形式工程方法国际会议“催化的交互框架”论文集。