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

ペトリネット型実行制御部をもつ代数的仕様記述の検証と分散実行系

研究課題

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

一般研究(C)

配分区分補助金
研究分野 計算機科学
研究機関大阪大学

研究代表者

谷口 健一  大阪大学, 基礎工学部, 教授 (00029513)

研究分担者 岡野 浩三  大阪大学, 基礎工学部, 助手 (70252632)
北道 淳司  大阪大学, 基礎工学部, 助手 (20234271)
松浦 敏雄  大阪大学, 情報処理教育センター, 助教授 (40127296)
東野 輝夫  大阪大学, 基礎工学部, 助教授 (80173144)
研究期間 (年度) 1994
研究課題ステータス 完了 (1994年度)
配分額 *注記
1,400千円 (直接経費: 1,400千円)
1994年度: 1,400千円 (直接経費: 1,400千円)
キーワード代数的手法 / ペトリネットモデル / 検証 / プログラム自動合成 / 分散実行
研究概要

1.本研究では,複数の処理の並列実行や同期等が表現できる記述モデルとして次のモデルを考案した.実行制御をペトリネットで記述する.内部データを自然に扱えるよう,内部レジスタを有限個持つ.ト-クンの配置(マ-キング)だけでなく,内部レジスタ値に依存して次の動作が選択でき,また,一つの動作で,外部とのデータの入出力,及び,内部レジスタ値の更新ができる.(ICDCS'95)
2.本モデルで記述した分散システムの全体仕様から,ネットワーク上で分散実行するプログラム群を自動導出する方法を考案した.得られるプログラム群では,動作効率の向上のため,ペトリネットモデルの利点を活かし,同時に発火可能なトランジションが複数並列に配置され,実行ステップ数が少なくなっている.また,プログラム間で交換されるメッセージ総数を,我々の過去の研究では一トランジションごと少なくしていたが,さらに,隣接する複数のトランジションの動作に着目し不必要なメッセージの削除を行なう工夫をしている.(信学論E77A-10,情処研報94-DPS65-27)また,本モデルのサブクラスであるステートマシンモデルに対する分散実行を視覚的に行なえる実行系を開発した.この実行系は同データ,音声等も扱え,グループウェアへの応用も可能となっている.(情処論文誌(採録))
3.Kellnerのソフトウェアプロセスが本モデルで自然に記述できることを確かめた.また,この例題に対し,人間が効率を考慮に入れながら導出したものと比べ,本導出方法で遜色のない分散実行プログラムを得られることを確認した.(信学技報94-SS38)
4.上述のステートマシンモデルの代数的な記述に対し,処理の正しさを証明する方法を考案した.また,整数上のある論理式の真偽判定法を利用する検証法を考案し,この真偽判定法を我々の検証システムに組み込んだ.(信学論SI(採録),TPCD'94)
5.今後の課題として,本モデル上での安全性や生存性等の動的性質の検証方法と実行系の扱うクラスの拡張について検討したい.

報告書

(1件)
  • 1994 実績報告書
  • 研究成果

    (7件)

すべて その他

すべて 文献書誌 (7件)

  • [文献書誌] Hirozumi YAMAGUCHI,Kozo OKANO,Teruo HIGASHINO and Kenichi TANIGUCHI: "Synthesis of Protocol Specifications from Service Specifications of Distributed Systems in a Marked Graph Model" 電子情報通信学会論文誌. Vol E77-A,No.10,. 1623-1633 (1994)

    • 関連する報告書
      1994 実績報告書
  • [文献書誌] 山口 弘純,岡野 浩三,東野 輝夫,谷口 健一: "レジスタを持つペトリネットで記述された分散システムの要求仕様から各ノードの動作仕様の導出" 情報処理学会研究会報告. 94-OS-64 94-DPS-65. 157-162 (1994)

    • 関連する報告書
      1994 実績報告書
  • [文献書誌] Hirozumi YAMAGUCHI,Kozo OKANO,Teruo HIGASHINO and Kenichi TANIGUCHI: "Software Process Description in a Petri Net Model and its Distributed Execution" 電子情報通信学会技術報告. 94-SS-38. 25-32 (1994)

    • 関連する報告書
      1994 実績報告書
  • [文献書誌] Hirozumi YAMAGUCHI,Kozo OKANO,Teruo HIGASHINO and Kenichi TANIGUCHI: "Synthesis of Protocol Entities'Specifications from Service Specifications in a Patri Net Model with Registers" 15th International Conference on Distributed Computing Systems(ICDCS'95). (採録決定). (1995)

    • 関連する報告書
      1994 実績報告書
  • [文献書誌] 岡野 浩三,東野 輝夫,谷口 健一: "あるスタイルに基づく順序機械型記述における詳細化の正しさの証明方法" 電子情報通信学会論文誌. D-I(採録決定). (1995)

    • 関連する報告書
      1994 実績報告書
  • [文献書誌] 伊東 達雄,今城 広志,岡野 浩三,松浦 敏雄,東野 輝夫,谷口 健一: "グループワークを考慮に入れた協調計算システムにおける動作プログラム群の生成と分散実行" 情報処理学会論文誌. (採録決定). (1995)

    • 関連する報告書
      1994 実績報告書
  • [文献書誌] Junji KITAMICHI,Sumio MORIOKA,Teruo HIGASHINO and Kenichi TANIGUCHI: "Automatic Correctness Proof of Implementation of Synchronous Sequential Circuits Using Algebraic Approach" Proc.of the 2nd Int.Conf.on Theorem Proves in Circuit Design(TPCD'94). 249-268 (1994)

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

URL: 

公開日: 1994-04-01   更新日: 2017-10-10  

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

Powered by NII kakenhi