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

1993 年度 実績報告書

ストリーム並列実行モデルに基づく並行動作プログラムの形式的開発法

研究課題

研究課題/領域番号 04452196
研究機関奈良先端科学技術大学院大学

研究代表者

荒木 啓二郎  奈良先端科学技術大学院大学, 情報科学研究科, 教授 (40117057)

研究分担者 岡村 耕二  奈良先端科学技術大学院大学, 情報科学研究科, 助手 (70252830)
福田 晃  九州大学, 工学部, 助教授 (80165282)
キーワード並行動作システム / ストリーム並列 / 形式的仕様 / 実行可能仕様 / 仕様記述言語Z / 仕様スライス / 並列オペレーティングシステム / 分散処理システム
研究概要

本研究では,並行動作プログラムの開発における仕様記述,設計,テスト,デバッグを形式的手法に基づいて系統的に行なう方法の確立とそれを支援するシステムの開発を目的とする.今年度は,仕様記述および並行動作システムの実現方式などを中心に以下の成果を得た.
1.システム記述法
システムの記述には,当初,関数型プログラミング言語Mirandaを用いた.これは,形式性と実行可能性を備えた実行可能仕様と位置付けられ,ソフトウェアシステム開発の上流工程における有用性を確認できた.更に仕様記述のレベルにおいて各種の形式的論証を行うために,形式的仕様記述言語Zも利用して,その有用性に対する見通しを得た.
2.システム記述支援
形式的仕様を作成する際には,当然それまでに記述した仕様の修正や改良や再利用を伴う.本研究では,Zによる形式的仕様に対して,仕様のスライスを提案し,これを応用することによって仕様の修正や再利用を効率よく進めるための方法を提示した.
3.並行動作システムの実現方式
本研究では,それ自体十分に解明されているわけではない並行動作システムを対象としているために,開発対象である並行動作システムの構成や処理方式に関しても研究を行った.具体的には,並列オペレーティングシステムの構成および処理方式,分散オペレーティングシステムの構成および処理方式,分散処理システムの試作と評価,マルチメディア通信システムのプロトコルおよび実現方式,コンピュータネットワーク上での分散協調作業の分析と支援ツールに対する要求分析などに関する研究を行った.ここで得られた成果や知見は,本研究の主要な課題であるシステムのモデル化や記述法に反映される.

  • 研究成果

    (6件)

すべて その他

すべて 文献書誌 (6件)

  • [文献書誌] 福田晃: "並列オペレーティング・システム" 情報処理学会誌. Vol.34,No9. 1139-1149 (1993)

  • [文献書誌] Hiroshi Maruyama: "Type Checking Slicing" Proc.InfoScience'93. 418-424 (1993)

  • [文献書誌] Tomohiro Oda: "Specification Slicing in Formal Methods of Software Development" Proc.COMPSAC'93. 313-319 (1993)

  • [文献書誌] Tomohiro Oda: "Application of Slicing Technique to Formal Specifications" Proc.JCSE'93. 203-210 (1993)

  • [文献書誌] Koji Okamura: "Implementation and Study of ParaDisE on Distributed Environment" Proc.of the 8th Int'l Joint Workshop on Compuer Communication. C2-2-1-C2-2-6 (1993)

  • [文献書誌] 古木良子: "Human-Orientedな形式的仕様記述法" ソフトウェアシンポジウム'94. (1994)

URL: 

公開日: 1995-02-08   更新日: 2016-04-21  

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

Powered by NII kakenhi