氏名: 田中昭二 (m06744)
論文題目: 優先順序付き並行演算子を組み込んだCCSとその応用
論文概要
本研究では並行計算の形式的モデルであるCCS(Calculus of Communicating
Systems)に優先順序付き並行演算子を組み込んだ体系PCCS(CCS with
Priority)を提案する。PCCSでは、CCSにおける内部動作を単位時間経過と
みなし、並行計算に優先度を導入することによって、並行実時間システム
をモデル化している。本研究における優先度は、並行実時間システムの時
間制約の実現において、デッドラインがせまった処理については高い優先
度を与えるというものである。この手法を形式的にモデル化することによ
り、並行実時間システムの仕様記述・設計が形式的に行なえるようになり、
動作の検証・無矛盾性などの性質の解析が計算機で処理できるようになる。
本論文では、PCCSの動作式、動作式間の遷移関係を定義する操作的意味論
について議論し 、実時間スケジューリング、優先順序付き通信プロトコル
などの例により、PCCSによる並行実時間システム実現手法を示す。また、
CCSの実行解析ツールであるCWB(Concurrency WorkBench)を拡張することに
より、PCCSの実行系を計算機に実装する。そして、PCCSによる並行実時間
システムの記述例を解析し、動作の検証を行なう。また、PCCSの等価性モ
デルとして、強等価、弱等価、efficiency prebisimulationなどについて
考察を行ない、とくに強等価に対して、等式論理に基づく書き換えによっ
て等価性を判定する完全な公理系を構成する。
目次に戻る