第 191 回 PTT のお知らせ

日時: 1993年 11月 25日 (木) 18:30 から
場所: 慶應義塾大学理工学部 25-601 教室 東横線日吉駅慶応大学側の出口(東側)を出て，東横線 に沿って左(渋谷方向)へ行く． 仲の谷という交差点 (仏具屋が目印)を右に(中華料理屋と民家の間の道)曲 がり，2〜3分で理工学部の表札が見えるので，そこの 左手の坂を登る．教室は25棟の6階．
話者： 佐藤 一郎（慶大・理工・計算機科学）
題目： プロセス代数をもちいた並行・分散システムの記述と証明
概要： 既存のプロセス代数に関する概説を行ない、つぎにプロセス代数に基 づく分散計算のための形式系と，これに基づくプロセスの等価関係を提案する．

分散システムの動作内容と時間性を記述・解析するための形式系を提案する． この形式系は，分散システム特有の時間的特性である局所的時間性(時計)に関 する概念を，既存のプロセス計算の枠組みに埋め込んだものである．これによ り，局所的時計の誤差や相違による分散システムの動作内容と時間的特性への 影響が明示的に解析できるようになる．さらにこの形式系に基づいて局所的時 間性を導入した双模倣性を定式化する．これは，不正確な時計に従う分散プロ セスや，非厳密な時間的制約をもつ実時間プロセスの時間的・動作的検証を可 能にするものである．
食事: 今回もありません． 
次々回: 1993年 12月 16日 (木) 東工大 (予定)

	      葉書の残りは   枚です

差出人(幹事):
113  東京都文京区弥生 2-11-16
     東京大学教育用計算機センター 岩崎英哉
     03-3812-2111  ext. 3020
     iwasaki@rds.ecc.u-tokyo.ac.jp

第 191 回 PTTメモ

日時: 1993年11月25日
場所: 慶應義塾大学理工学部 25-601 教室
題目: プロセス代数をもちいた並行・分散システムの記述と証明
話者: 佐藤 一郎(慶大・理工・計算機科学)
出席者: 岩崎英哉, 下國治, 神南吉宏, 立山義祐, 田中哲朗, 寺田実, 山本具英, 木下毅, 和田英一 (東大), 脇田健 (東工大), 小出洋, 茅野剛史, 中山奉一, 益田典明 (電通大), 並木美太郎 (農工大), 石畑清(明大), 飯島正, 馬場博樹 (慶大), 倉部淳, 伊知地 宏 (富士ゼロックス),
質疑応答:

並行計算モデルの一つであるプロセス代数 (CSP,CCS,pi-calculus)に関す る一般的な概説を行った後、時間的特性を拡張したプロセス代数体系である RtCCSとDtCCSを提案し、さらにプロセスの等価関係をもとにした解析・検証技 法について紹介した。

プロセス代数は、プロセスの並行実行や通信に関して優れた表現性を持っ ているが、時間的概念がなく実行時間や通信のタイミングを含むシステムの正 当性や効率の解析には十分ではなかった。そこで、CCS に全域的な時間経過を 表すアクションと、タイムアウト処理に準じた演算子を導入することにより、 並行・通信システムの動作内容と時間的特性を同時に表現・解析できる形式系 を構築する。また、それの検証技法としてプロセスの実行タイミングを考慮し たプロセスの等価関係を与えた。

一方 DtCCSは、分散システムにおける全域的な時間基準の非存在を考慮 し、RtCCS に局所的時間(時計)の相違や誤差の表現性を導入したもので ある。これにより、全域的時間に従う並行システム以外に不正確な時計 に従う分散プロセスが取り扱えるようになる。

発表では、提案した形式系それ自体と、実際のシステムの親和性に関し て数多くの有意義な質問・助言があり講演者自身にとっても得ることが 多かった。

報告者:  慶応義塾大学 大学院 理工学研究科
         計算機科学専攻  所 研究室  博士課程

          佐藤一郎  ( satoh@mt.cs.keio.ac.jp)