OTS/CafeOBJ から OTS/Maude への仕様変換の研究 A complete specification transformation from OTS/CafeOBJ to OTS/Maude

Search this Article

Author(s)

    • 中村 正樹 NAKAMURA Masaki
    • 北陸先端科学技術大学院大学 情報科学研究科 School of Information Science, Japan Advanced Institute of Science and Technology
    • 孔 維強 KONG Weiqiang
    • 北陸先端科学技術大学院大学 情報科学研究科 School of Information Science, Japan Advanced Institute of Science and Technology
    • 緒方 和博 [他] OGATA Kazuhiro
    • 北陸先端科学技術大学院大学 情報科学研究科 School of Information Science, Japan Advanced Institute of Science and Technology
    • 二木 厚吉 FUTATSUGI Kokichi
    • 北陸先端科学技術大学院大学 情報科学研究科 School of Information Science, Japan Advanced Institute of Science and Technology

Abstract

代数仕様言語を用いて状態遷移機械を記述する手法に,振舞仕様に基づく観測遷移機械(OTS)による手法と書き換え論理に基づく書き換え仕様による手法がある.それぞれ記述言語としてCafeOBJおよびMaudeを持ち,各手法で異なる検証スタイルを持つ.本研究では,2つの異なる検証手法を統合した検証システムの構築のため,OTS/CafeOBJ仕様からMaude書き換え仕様への変換について考察する.

There are two ways to describe a state machine with algebraic specifications: observation transition systems on CafeOBJ and rewrite specifications on Maude. Each specification language has different verification techniques. In this study, to make a verification system obtained by combining each verification techniques, we propose a transformation method from CafeOBJ specifications to Maude specifications.

Journal

  • IEICE technical report

    IEICE technical report 106(120), 1-6, 2006-06-15

    The Institute of Electronics, Information and Communication Engineers

References:  5

Codes

  • NII Article ID (NAID)
    110004750956
  • NII NACSIS-CAT ID (NCID)
    AN10013287
  • Text Lang
    ENG
  • Article Type
    ART
  • ISSN
    09135685
  • NDL Article ID
    7977506
  • NDL Source Classification
    ZN33(科学技術--電気工学・電気機械工業--電子工学・電気通信)
  • NDL Call No.
    Z16-940
  • Data Source
    CJP  NDL  NII-ELS 
Page Top