1994 Fiscal Year Annual Research Report
ペトリネット型実行制御部をもつ代数的仕様記述の検証と分散実行系
| Project/Area Number |
06680320
|
|---|
| Research Institution | Osaka University |
|---|
Principal Investigator |
谷口 健一 大阪大学, 基礎工学部, 教授 (00029513)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
岡野 浩三 大阪大学, 基礎工学部, 助手 (70252632)
北道 淳司 大阪大学, 基礎工学部, 助手 (20234271)
松浦 敏雄 大阪大学, 情報処理教育センター, 助教授 (40127296)
東野 輝夫 大阪大学, 基礎工学部, 助教授 (80173144)
|
|---|
| Keywords | 代数的手法 / ペトリネットモデル / 検証 / プログラム自動合成 / 分散実行 |
|---|
| Research Abstract |
1.本研究では,複数の処理の並列実行や同期等が表現できる記述モデルとして次のモデルを考案した.実行制御をペトリネットで記述する.内部データを自然に扱えるよう,内部レジスタを有限個持つ.ト-クンの配置(マ-キング)だけでなく,内部レジスタ値に依存して次の動作が選択でき,また,一つの動作で,外部とのデータの入出力,及び,内部レジスタ値の更新ができる.(ICDCS'95)
2.本モデルで記述した分散システムの全体仕様から,ネットワーク上で分散実行するプログラム群を自動導出する方法を考案した.得られるプログラム群では,動作効率の向上のため,ペトリネットモデルの利点を活かし,同時に発火可能なトランジションが複数並列に配置され,実行ステップ数が少なくなっている.また,プログラム間で交換されるメッセージ総数を,我々の過去の研究では一トランジションごと少なくしていたが,さらに,隣接する複数のトランジションの動作に着目し不必要なメッセージの削除を行なう工夫をしている.(信学論E77A-10,情処研報94-DPS65-27)また,本モデルのサブクラスであるステートマシンモデルに対する分散実行を視覚的に行なえる実行系を開発した.この実行系は同データ,音声等も扱え,グループウェアへの応用も可能となっている.(情処論文誌(採録))
3.Kellnerのソフトウェアプロセスが本モデルで自然に記述できることを確かめた.また,この例題に対し,人間が効率を考慮に入れながら導出したものと比べ,本導出方法で遜色のない分散実行プログラムを得られることを確認した.(信学技報94-SS38)
4.上述のステートマシンモデルの代数的な記述に対し,処理の正しさを証明する方法を考案した.また,整数上のある論理式の真偽判定法を利用する検証法を考案し,この真偽判定法を我々の検証システムに組み込んだ.(信学論SI(採録),TPCD'94)
5.今後の課題として,本モデル上での安全性や生存性等の動的性質の検証方法と実行系の扱うクラスの拡張について検討したい.
|
-
[Publications] 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)
-
[Publications] 山口 弘純,岡野 浩三,東野 輝夫,谷口 健一: "レジスタを持つペトリネットで記述された分散システムの要求仕様から各ノードの動作仕様の導出" 情報処理学会研究会報告. 94-OS-64 94-DPS-65. 157-162 (1994)
-
[Publications] 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)
-
[Publications] 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)
-
[Publications] 岡野 浩三,東野 輝夫,谷口 健一: "あるスタイルに基づく順序機械型記述における詳細化の正しさの証明方法" 電子情報通信学会論文誌. D-I(採録決定). (1995)
-
[Publications] 伊東 達雄,今城 広志,岡野 浩三,松浦 敏雄,東野 輝夫,谷口 健一: "グループワークを考慮に入れた協調計算システムにおける動作プログラム群の生成と分散実行" 情報処理学会論文誌. (採録決定). (1995)
-
[Publications] 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)
