权益分类	功能权益	普通用户	{{item.name}}会员
{{category.name}}	{{benefitItem.name}}

現実的な形式的オブジェクト指向分析と計算機支援環境

现实的形式化面向对象分析和计算机辅助环境

基本信息

批准号：
14019044
负责人：
青木利晃
金额：
$ 2.05万
依托单位：
Japan Advanced Institute of Science and Technology
依托单位国家：
日本
项目类别：
Grant-in-Aid for Scientific Research on Priority Areas
财政年份：
2002
资助国家：
日本
起止时间：
2002 至无数据
项目状态：
已结题

来源：
https://kaken.nii.ac.jp/en/grant/KAKENHI-PROJECT-14019044/
关键词：
オブジェクト指向分析形式的手法検証計算機支援環境

项目摘要

高い信頼性を持つシステムを実現するためには、形式的手法の導入が必要であるが、冗長性などの問題が障壁となり、実際のシステム開発に適用されていない。そこで、本研究では、この問題点を(1)領域ライブラリの作成による再利用性の向上、(2)オブジェクト指向分析モデルの構文面の性質の自動検証、により解決する。(1)、(2)の成果は、それぞれ、以下のとおりである。(1)領域ライブラリの作成による再利用性の向上。本研究の成果として、領域ライブラリのためのモデル、公理系、定理証明システムHOLによる支援法について提案した。提案したモデルでは、対象領域に出現する概念をクラス図を用いてモデル化する。構築したモデルは、提案した公理系によりオブジェクト指向分析モデルの様々な性質の検証に用いることができる。また、公理系を、定理証明システムHOLにより取り扱い可能な形式に翻訳する手法を提案した。これにより、構築した領域ライブラリを用いて、定理証明システムHOL上でオブジェクト指向分析モデルの様々な性質を検証することが可能になった。領域ライブラリは、同一の性質を持つ複数のシステムに共通な概念をライブラリ化したものである。提案したこれらの成果を用いて検証のための領域ライブラリを作成することにより、コストが高く障壁となっていた検証に伴う証明の再利用性が向上し、形式的検証が現実的なものとなることが期待される。(2)オブジェクト指向分析モデルの構文面の性質の自動検証。本研究では、構築したモデルの構文面の性質を自動的に検証するツールを作成した。このツールでは、Rational Rose等の市販のツールにより構築したモデルをUMLXMI形式で読み込み、OCLにより記述した構文面の性質を自動検証する。このような構文面の性質は、(1)で提案した手法を適用するまでもなく、自動的に検証可能である。実際、他論文で提案されている構文面の性質を、提案したツールで自動的に検証可能であることを確認した。本研究により提案した(1)、(2)の手法を適切にシステム開発に適用することにより、検証コストを低く抑えることが可能になる。これにより、実際のシステム開発に形式的手法を導入することが可能になり、製品の信頼性の飛躍的な向上が期待される。

High reliability, high reliability, high This study focuses on the following issues: (1) the improvement of reusability in the field of production;(2) the automatic identification and solution of the properties of structural surfaces in the field of directional analysis. (1)(2) The results are as follows: (1)The reusability of the domain is upward. The results of this study include: domain classification, axiom system, theorem proof, support method, etc. Proposals can be implemented and concepts emerging in the target field can be used quickly. Construction of an axiom system for the analysis of the properties of a given object The axiom system, theorem proof, and method of obtaining the possible form are proposed. This is the first time that a person has ever been involved in a crime, and the first time he has ever been involved in a crime, he has been involved in a crime. The concept of domain identity is common to a number of species. The results of the proposal are expected to be available in the form of a high barrier to proof of reuse. (2)Automatic identification of the properties of the texture by means of the texture analysis. In this study, the structure of the structure is automatically verified. This article describes how to automatically verify the nature of the structure of the text in the form of UML XMI, OCL, Rational Rose, etc. The nature of this structure is (1) the method of proposal is applicable, and the automatic verification is possible. In the meantime, the nature of the structure of the proposal, the proposal and the automatic verification are confirmed. The methods proposed in this study (1) and (2) are applicable to the development of the system. Therefore, it is possible to introduce practical methods for system development, and we look forward to a leap in product reliability.