入出力関数を基礎とした形式的並行プロセス記述体系とその表示的意味論
スポンサーリンク
概要
- 論文の詳細を見る
並行システムの仕様記述・検証を目的として種々の形式的体系或は数学的モデルが提案されている.この内R.Milnerが提案したCCSは,外部から観測可能なインタラクションの時間的順序関係を記述するものであり,システムの必要十分な規定を可能とする点から評価が高い.一方通常の手続き型言語を基礎に並行動作記述機能を付加した言語(Ada,ISOのEsttelle等)による記述とCCSによる記述の対応関係(例えばEsttelleによる記述がCCSによって記述された仕様を満たすか否かの判定法等)は必ずしも明らかではない.本稿ではシステム仕様の記述・検証のための形式的理論として手続き型言語の主要な機能を含み,かつ仕様に対して観測可能なインタラクションの時間順序を導出可能とするような理論TCS(A Formal Theory of Communicating systems)を提案する.既に提案された同種の他の体系に比較して,TCSは再帰的定義が可能である等の点で強力であり,上記の対応付けをある程度可能とする理論となっている.TCSのサウンドネスについては,treeを用いてそのモデルを与えることにより示す.
- 一般社団法人情報処理学会の論文
- 1986-10-01