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

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

研究課題

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

基盤研究(B)

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

研究代表者

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

研究分担者 緒方 和博  北陸先端科学技術大学院大学, 情報科学研究科, 助手 (30272991)
渡部 卓雄  東京工業大学, 情報理工学研究科, 助教授 (20222408)
ディアコネスク ラズウ゛ァ  北陸先端科学技術大学院大学, 情報科学研究科, 助手 (30293393)
研究期間 (年度) 1998 – 2001
研究課題ステータス 完了 (2001年度)
配分額 *注記
12,700千円 (直接経費: 12,700千円)
2001年度: 2,800千円 (直接経費: 2,800千円)
2000年度: 3,100千円 (直接経費: 3,100千円)
1999年度: 3,000千円 (直接経費: 3,000千円)
1998年度: 3,800千円 (直接経費: 3,800千円)
キーワードコンポーネント / 高信頼 / 支援ツール / CafeOBJ / モジュールシステム / 仕様 / 分散(実時間)システム / 検証 / 機能的性質 / 非機能的性質 / 代数仕様 / ソフトウェア発展 / 射影型振舞仕様 / 詳細化検証 / 木アーキテクチャ / オブジェクト指向 / 形式仕様 / 振舞い仕様 / 方法論 / 閲覧システム / 形式仕様言語 / 代数モデル / UML / 振舞仕様
研究概要

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

報告書

(5件)
  • 2001 実績報告書   研究成果報告書概要
  • 2000 実績報告書
  • 1999 実績報告書
  • 1998 実績報告書
  • 研究成果

    (35件)

すべて その他

すべて 文献書誌 (35件)

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

    • 説明
      「研究成果報告書概要(和文)」より
    • 関連する報告書
      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)

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

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

    • 説明
      「研究成果報告書概要(和文)」より
    • 関連する報告書
      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)

    • 説明
      「研究成果報告書概要(和文)」より
    • 関連する報告書
      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)

    • 説明
      「研究成果報告書概要(和文)」より
    • 関連する報告書
      2001 研究成果報告書概要
  • [文献書誌] M. Matsumoto, K. Futatsugi: "The tool that supports highly reliable component-based software development"IEICE Transactions on Information & Systems. J84DI-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. E84A-6. 1471-1478 (2001)

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

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

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

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

    • 説明
      「研究成果報告書概要(欧文)」より
    • 関連する報告書
      2001 研究成果報告書概要
  • [文献書誌] 松本充広, 二木厚吉: "高信頼コンポーネントソフトウェアの開発ツール"電子情報通信学会論文誌 D-1. J84-D-I・6. 736-744 (2001)

    • 関連する報告書
      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)

    • 関連する報告書
      2001 実績報告書
  • [文献書誌] K.Futatsugi, K.Ogata: "Rewriting can verify distributed real-time systems"Proc. of the Int 1 Workshop on Rewriting in Proof and Computation (RPC 01). 60-79 (2001)

    • 関連する報告書
      2001 実績報告書
  • [文献書誌] K.Ogata, K.Futatsugi: "Modeling and verification of distributed real-time systems based on CafeOBJ"Proc. of the 16^<th> IEEE Int 1 Conference on Automated Software Engineering (ASE 01). 185-192 (2001)

    • 関連する報告書
      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)

    • 関連する報告書
      2001 実績報告書
  • [文献書誌] K.Ogata, K.Futatsugi: "Formal analysis of Suzuki & Kasami distributed mutual exclusion algorithm"Proc. of the IFIP TC6/WG6.1 Fifth Int' 1 Conference on Formal Methods for Open Object-Based Distributed Systems. (2002)

    • 関連する報告書
      2001 実績報告書
  • [文献書誌] Iida,S.,Futatsugi,K.: "Formal approach for handing software evolution in component-based software developments"Proc.of Int'l Symposium on Principles of Software Evolution 2000. (2000)

    • 関連する報告書
      2000 実績報告書
  • [文献書誌] 飯田周作,二木厚吉: "形式仕様を用いたシステムの非機能的性質記述の試み-コンポーネントに基づくソフトウェア開発への応用-"ソフトウェア・シンポジウム2000. (2000)

    • 関連する報告書
      2000 実績報告書
  • [文献書誌] 飯田周作,二木厚吉: "振舞仕様に基づく仕様コンポーネント化技術の発展可能ソフトウェアへの応用"コンピュータソフトウェア別冊ソフトウェア発展. 30-45 (2001)

    • 関連する報告書
      2000 実績報告書
  • [文献書誌] Matsumoto,M.,Futatsugi,K.: "Higly reliable component-based software development by using algebraic behavioral specification"Proc.of 3rd IEEE Int'l Conference on Formal Engineering Methods (ICFEM'2000). 35-43 (2000)

    • 関連する報告書
      2000 実績報告書
  • [文献書誌] Matsumoto,M.,Futatsugi,K.: "The support tool for highly reliable component-based software development"Proc.of 7th Asia-Pacific Software Engineering Conference (APSEC'2000). 172-179 (2000)

    • 関連する報告書
      2000 実績報告書
  • [文献書誌] Seino,T.,Ogata,K.,Futatsugi,K.: "Specification and verification of a single-track railroad signaling in CafeOBJ"Proc.of 2000 Int'l Technical Conference on Circuits/Systems,Computers and Communications(ITC-CSCC 2000). 268-273 (2000)

    • 関連する報告書
      2000 実績報告書
  • [文献書誌] R.Diaconescu,K.Futatsugi,S.Iida: "Component-based algebraic specification and verification in CafeOBJ"Lecture Notes in Computer Science. 1709. 1644-1663 (1999)

    • 関連する報告書
      1999 実績報告書
  • [文献書誌] C.Matsumiya,S.Iida,K.Futatsugi: "A component-based algebraic specification of ODP trading function and the interactive browsing environment"Proc.of OBJ/CafeOBJ/Maude at Fprmal Methods'99. 227-241 (1999)

    • 関連する報告書
      1999 実績報告書
  • [文献書誌] M.Matsumoto,K.Futatsugi: "Object composition and refinement by using non-observable projection operators: a case study of the automated teller machine system"Proc.of OBJ/CafeOBJ/Maude at Fprmal Methods'99. 133-157 (1999)

    • 関連する報告書
      1999 実績報告書
  • [文献書誌] M.Matsumoto,K.Futatsugi: "Simply Observable Behavioral Specification"Proc.of Asia-Pasific Software Engineering Conference. 460-467 (1999)

    • 関連する報告書
      1999 実績報告書
  • [文献書誌] 清野貴博,緒方和博,二木厚吉: "代数仕様言語CafeOBJによる鉄道信号システムの記述と検証"ソフトウェア工学の基礎VI(日本ソフトウェア科学会FOSE'99). 180-187 (1999)

    • 関連する報告書
      1999 実績報告書
  • [文献書誌] 飯田、二木、渡部: "CafeOBJによる分散システムの形式仕様作成法" コンピュータソフトウェア. 15・1. 34-49 (1998)

    • 関連する報告書
      1998 実績報告書
  • [文献書誌] 飯田、二木: "代数モデルによるUMLの意味論-形式仕様に基づくコンポーネント設計の視覚化を目指して-" ソフトウェア工学の基礎V(レクチャノート/ソフトウェア工学). 20. 151-156 (1998)

    • 関連する報告書
      1998 実績報告書
  • [文献書誌] 海野、松本、飯田、二木: "振舞仕様に基づくシステムの記述方法" 信学技報. 98・230. 1-8 (1998)

    • 関連する報告書
      1998 実績報告書
  • [文献書誌] Iida,Futatsugi,Diaconescu: "Component based algebtaic epecification-behaviousal specification for component based software engineering-" Proc.of 7th OOPSLA Workshop on Behavioral Semantics of OOBusiness and System Specifiation. 167-182 (1998)

    • 関連する報告書
      1998 実績報告書
  • [文献書誌] 五百蔵、緒方、二木: "CafeOBJのモジュールシステムの設計およびCafeOBJによる検証" ソフトウェア工学の基礎V(レクチャノート/ソフトウェア工学). 20. 209-218 (1998)

    • 関連する報告書
      1998 実績報告書
  • [文献書誌] Ogata,Ioroi,Futatsugi: "Optimixing teim rewriting using discrimination nets with specialization" Proc.of the 1999 ACM Symposium on Appllied Capoting. (1999)

    • 関連する報告書
      1998 実績報告書

URL: 

公開日: 1998-04-01   更新日: 2016-04-21  

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

Powered by NII kakenhi