• 研究課題をさがす
  • 研究者をさがす
  • KAKENの使い方
  1. 課題ページに戻る

2001 年度 研究成果報告書概要

機能に基づく仕様のコンポーネント化を可能とする形式仕様言語の開発

研究課題

研究課題/領域番号 10558043
研究種目

基盤研究(B)

配分区分補助金
応募区分展開研究
研究分野 計算機科学
研究機関北陸先端科学技術大学院大学

研究代表者

二木 厚吉  北陸先端科学技術大学院大学, 情報科学研究科, 教授 (50251971)

研究分担者 緒方 和博  北陸先端科学技術大学院大学, 情報科学研究科, 助手 (30272991)
渡部 卓雄  東京工業大学, 情報理工学研究科, 助教授 (20222408)
研究期間 (年度) 1998 – 2001
キーワードコンポーネント / 高信頼 / 支援ツール / CafeOBJ / モジュールシステム / 仕様 / 分散(実時間)システム / 検証
研究概要

本研究では、仕様のコンポーネント化を支援するための諸機能を有する仕様記述言語CafeOBJを基盤ツールとして用いた。CafeOBJは、研究代表者を中心に開発を続けている代数仕様言語で、抽象データ型のみならず、オブジェクト指向におけるオブジェクトや抽象機械の記述にも適しており、仕様のコンポーネント化を支援する強力なモジュールシステムを有するのも特徴の一つである。
具体的には以下のことを行った。
・検証実験:鉄道の信号システム、航空管制システム、病院における患者監視システム等、人命に多大な影響を及ぼし得るシステムは、並列分散(実時間)システムであることが多い。これらシステムをCafeOBJ支援のもとで検証する方法を整理、提案し、いくつかの事例研究をとおして提案手法の有効性を確認した。
・ツールの設計および作成:コンポーネントを組み上げて高品位のソフトウェアを作成するための基礎理論を作り、その理論に基づいてソフトウェアを作成するツールの設計および作成を行った。

  • 研究成果

    (12件)

すべて その他

すべて 文献書誌 (12件)

  • [文献書誌] 松本充広, 二木厚吉: "高信頼コンポーネントソフトウェアの開発ツール"電子情報通信学会論文誌D-I. J84.D-I・6. 736-744 (2001)

    • 説明
      「研究成果報告書概要(和文)」より
  • [文献書誌] T.Seino, K.Ogata, K.Futatsugi: "Specification and verification of a single-track railroad signaling in CafeOBJ"IEICE Transactions on Fundamentals of Electronics, Communications and Computer Science. E84-A・6. 1471-1478 (2001)

    • 説明
      「研究成果報告書概要(和文)」より
  • [文献書誌] K.Futatsugi, K.Ogata: "Rewriting can verify distributed real-time systems"Proc. PRC '01. 60-79 (2001)

    • 説明
      「研究成果報告書概要(和文)」より
  • [文献書誌] K.Ogata, K.Futatsugi: "Modeling and verification of distributed real-time systems based on CafeOBJ"Proc. of ASE '01. 185-192 (2001)

    • 説明
      「研究成果報告書概要(和文)」より
  • [文献書誌] K.Ogata, K.Futatsugi: "Formally modeling and verifying Ricart & Agrawala distributed mutual exclusion algorithm"Proc. of the Second Asia-Pacific Conference on Quality Software (APAQS'01). 357-366 (2001)

    • 説明
      「研究成果報告書概要(和文)」より
  • [文献書誌] K.Ogata, K.Futatsugi: "Formal analysis of Suzuki & Kasami distributed mutual exclusion algorithm"Proc. of the IFIP TC6/WG6.1 Fifth Int'l Conference on Formal Methods for Open Object-Based Distributed Systems. (2002)

    • 説明
      「研究成果報告書概要(和文)」より
  • [文献書誌] M. Matsumoto, K. Futatsugi: "The tool that supports highly reliable component-based software development"IEICE Transactions on Information & Systems. J84DI-6. 736-744

    • 説明
      「研究成果報告書概要(欧文)」より
  • [文献書誌] T. Seino, K. Ogata, K. Futatsugi: "Specification and verification of a single-track railroad signaling in CafeOBJ"IEICE Transactions on Fundamentals of Electronics, Communications and Computer Science. E84A-6. 1471-1478 (2001)

    • 説明
      「研究成果報告書概要(欧文)」より
  • [文献書誌] K. Futatsugi, K. Ogata: "Rewriting can verify distributed real-time systems"Proc. Of RPC'01. 60-79 (2001)

    • 説明
      「研究成果報告書概要(欧文)」より
  • [文献書誌] K. Ogata, K. Futatsugi: "Modeling and verification of distributed real-time systems based on CafeOBJ"Proc. Of ASE'01. 185-192 (2001)

    • 説明
      「研究成果報告書概要(欧文)」より
  • [文献書誌] K. Ogata, K. Futatsugi: "Formally modeling and verifying Ricart&Agrawala distributed mutual exclusion algorithm"Proc. Of APAQS'01. 357-366 (2001)

    • 説明
      「研究成果報告書概要(欧文)」より
  • [文献書誌] K. Ogata, K. Futatsugi: "Formal analysis of Suzuki&Kasami distributed mutual exclusion algorithm"Proc. Of FMOODS'02. (2002)

    • 説明
      「研究成果報告書概要(欧文)」より

URL: 

公開日: 2003-09-17  

サービス概要 検索マニュアル よくある質問 お知らせ 利用規程 科研費による研究の帰属

Powered by NII kakenhi