並列システムの仕様記述、デザインのためのGPAMソフトウェア・ツール

点击翻译按钮获取中文摘要

本研究では、プロセス代数の動作的定義に一般的に用いられる構造的操作意味定義(Structural Operational Somantics)を拡張し、SOS定義の構文に対してSOS定義が導くラベル付遷移システムの動作の代数的性質を保証する条件を提案する。この条件を検証することで、妥当な動作的性質を持つプロセス代数の系統的な設計手法を示し、実際の言語設計ツール構築を目的とする。前年度までに導入した順序付きSOS定義に対して、本年度は時間の概念を導入することで、より実際的なモデル化を可能とした。本年度は以下の項目について研究を行った。・順序付SOS定義に対してEager Rooted双模倣意味論による合同性条件を与えた。・SOS定義に対して、離散時間単位を表わす特別なラベルσを導入し、Eager Rooted双模倣意味論を時間に対して拡張した。・SOS定義に対して、σによる遷移が離散時間のモデルとして良定義であるための条件を提案した。・国内の他の研究者と共同して、時間拡張の条件をチェックするツールの基本的な設計を行った。これらの成果により、実際のGPAMソフトウェア・ツールの設計のためのノウハウが蓄積できたと考えている。今後は、さらに時間を導入したTest前順序意味論に対しても検討を加えることにより、統一的な設計手法が提案できるようになり、ツールの作成が可能となる。