講演名 | 2000/1/18 論理的な仕様から分散システムを合成する方法の検討 磯部 祥尚, 大蒔 和仁, |
---|---|
PDFダウンロードページ | PDFダウンロードページへ |
抄録(和) | 本研究は逐次的な仕様から分散システムを合成する方法を確立することを目的としている。本稿では、分散システムを形式的に記述するためのプロセス代数CCS@と、要求を形式的に記述するためのプロセス論理PL@を定義し、プロセス論理で記述された仕様の充足可能を判定するために有効な定理を与える。充足可能性判定とは仕様を満たす分散システムが存在するかを判定することであり、合成方法を確立するために重要である。この定理は使用可能なアクション名の集合が無限である場合だけでなく、有限である場合も成り立つ。 |
抄録(英) | Our purpose is to give a syntheis method of a distributed system from sequential sepecifications. In this paper, we define a process algebra CCS@ and a process logic PL@ to formally express distributed systems and specifications respectively, and then present a useful theorem to check satisfiability of specifications expressed in PL,where a specification is satisfiable if and only if there is a system to satisfy it. This theorem does not only hold for infinite sets of action names, but also for finite sets. |
キーワード(和) | プロセス代数 / プロセス論理 / 充足可能性 / 分散システム |
キーワード(英) | process algebra / process logic / satisfiability / distributed system |
資料番号 | CST99-59 |
発行日 |
研究会情報 | |
研究会 | CST |
---|---|
開催期間 | 2000/1/18(から1日開催) |
開催地(和) | |
開催地(英) | |
テーマ(和) | |
テーマ(英) | |
委員長氏名(和) | |
委員長氏名(英) | |
副委員長氏名(和) | |
副委員長氏名(英) | |
幹事氏名(和) | |
幹事氏名(英) | |
幹事補佐氏名(和) | |
幹事補佐氏名(英) |
講演論文情報詳細 | |
申込み研究会 | Concurrent System Technology (CST) |
---|---|
本文の言語 | JPN |
タイトル(和) | 論理的な仕様から分散システムを合成する方法の検討 |
サブタイトル(和) | |
タイトル(英) | A Study on a Synthesis Method of a Distributed System from Logical Specifications |
サブタイトル(和) | |
キーワード(1)(和/英) | プロセス代数 / process algebra |
キーワード(2)(和/英) | プロセス論理 / process logic |
キーワード(3)(和/英) | 充足可能性 / satisfiability |
キーワード(4)(和/英) | 分散システム / distributed system |
第 1 著者 氏名(和/英) | 磯部 祥尚 / Yoshinao ISOBE |
第 1 著者 所属(和/英) | 電子技術総合研究所 情報アーキテクチャ部 Computer Science Division, Electrotechnical Laboratory |
第 2 著者 氏名(和/英) | 大蒔 和仁 / Kazuhito OHMAKI |
第 2 著者 所属(和/英) | 電子技術総合研究所 情報アーキテクチャ部 Computer Science Division, Electrotechnical Laboratory |
発表年月日 | 2000/1/18 |
資料番号 | CST99-59 |
巻番号(vol) | vol.99 |
号番号(no) | 539 |
ページ範囲 | pp.- |
ページ数 | 8 |
発行日 |