一覧に戻る

タイトル
  • Component-based algebraic specification and verification in cafeOBJ
作成者
    • Diaconescu, Razvan
    • Futatsugi, Kokichi
    • Iida, Shusaku
内容注記
  • Other We present a formal method for component-based system specification and verification which is based on the new algebraic specification language CafeOBJ, which is a modern successor of OBJ incorporating several new developments in algebraic specification theory and practice. We first give an overview of the origins and of the main features of CafeOBJ, including its logical foundations, and then we focus on the behavioural specification paradigm in CafeOBJ, surveying the object-oriented CafeOBJ specification and verification methodology based on behavioural. abstraction. The last part of this paper further focuses on a component-based behavioural specification and verification methodology which features high reusability of both specification code and verification proof scores. This methodology constitutes the basis for an industrial strength formal method around CafeOBJ.
  • Other リサーチレポート（北陸先端科学技術大学院大学情報科学研究科）
  • Other identifier:https://dspace.jaist.ac.jp/dspace/handle/10119/8385
出版者 北陸先端科学技術大学院大学情報科学研究科
日付
    Issued1999-05-06
言語
  • eng
資源タイプ technical report
出版タイプ VoR
資源識別子 URI http://hdl.handle.net/10119/8385
収録誌情報
    • ISSN 0918-7553
      • Research report (School of Information Science, Japan Advanced Institute of Science and Technology)
      • 巻IS-RR-99-0020S 開始ページ1 終了ページ20
ファイル
コンテンツ更新日時 2021-04-14