Refinement Calculusに基づく用語辞書からのフォーマルなモデル構成  [in Japanese] Formal Model Generation from Requirement Dictionary Based on Refinement Calculus  [in Japanese]

Search this Article


    • 大森洋一
    • 九州大学大学院システム情報科学研究院 Faculty of Information Science and Electrical Engineering, Kyushu University
    • 荒木啓二郎
    • 九州大学大学院システム情報科学研究院 Faculty of Information Science and Electrical Engineering, Kyushu University


フォーマルな用語辞書は,通常の用語辞書に加えて,自然言語によるキーフレーズとそのキーフレーズのフォーマルメソッドを用いた意味定義の写像を与える.用語辞書を用いることにより,ソフトウェア開発プロジェクトにおいて各キーフレーズの意味の一貫性をフォーマルメソッドを用いて保証可能となり,さらに同じドメインにおいてキーフレーズとその意味定義の集合が再利用可能なドメイン知識となる.しかし,保守工程や新規のプロジェクトにおいて,既存の用語辞書を再利用して,仕様としてのフォーマルなモデルを記述するする場合,環境の違いによりキーフレーズの意味に一貫性があるとは限らない.本研究では,用語辞書を数理的に定義し,用語辞書に含まれる各キーフレーズのフォーマルな制約に基づいて,意味の一貫性が保たれるための条件を明らかにする.このために,用語辞書におけるフォーマルな要素の意味論,不整合が発生する条件を Refinement Calculus で定義し,そうした不整合を起こさない枠組みを提案する.

A formal requirement dictionary extends existing requirement dictionary to give the map of the key phrase by natural language and its semantics definition using the mathematical logic. The consistency of the semantics of each key phrase can be guaranteed in a software development project by using a formal requirement dictionary. The dictionary can be reused as a set key phrases and corresponding formal definitions in the same domain. However, the semantics of the key phrase in the reused dictionary, which had been constructed during the developing phase of a software project, does not necessarily have consistency in the different environments, such as in maintenance phase or a new project. This paper formally defines the formal requirement dictionary and clarifies the conditions for the consistent semantics of the key phrases by their formal restrictions. We propose that definitions of the semantics of formal elements in the requirement dictionary and the conditions for inconsistency based on Refinement Calculus, and a framework which does not cause such inconsistency.


  • IPSJ SIG Notes

    IPSJ SIG Notes 2014-SE-184(10), 1-7, 2014-05-12

    Information Processing Society of Japan (IPSJ)



  • NII Article ID (NAID)
  • Text Lang
  • Data Source
Page Top