WEKO3
アイテム
形式的検証機能を備えたインターネットエージェントプログラミングシステム
https://ipsj.ixsq.nii.ac.jp/records/17154
https://ipsj.ixsq.nii.ac.jp/records/17154b43b8195-c33b-465a-9744-bd2b4f9c4160
| 名前 / ファイル | ライセンス | アクション |
|---|---|---|
IPSJ-TOM4714010.pdf (194.7 kB)
|
Copyright (c) 2006 by the Information Processing Society of Japan
|
|
| オープンアクセス | ||
| Item type | Trans(1) | |||||||
|---|---|---|---|---|---|---|---|---|
| 公開日 | 2006-10-15 | |||||||
| タイトル | ||||||||
| タイトル | 形式的検証機能を備えたインターネットエージェントプログラミングシステム | |||||||
| タイトル | ||||||||
| 言語 | en | |||||||
| タイトル | An Internet Agent Programming System with a Formal Verification Facility | |||||||
| 言語 | ||||||||
| 言語 | jpn | |||||||
| キーワード | ||||||||
| 主題Scheme | Other | |||||||
| 主題 | オリジナル論文 | |||||||
| 資源タイプ | ||||||||
| 資源タイプ識別子 | http://purl.org/coar/resource_type/c_6501 | |||||||
| 資源タイプ | journal article | |||||||
| 著者所属 | ||||||||
| 日本電信電話株式会社NTTコミュニケーション科学基礎研究所 | ||||||||
| 著者所属(英) | ||||||||
| en | ||||||||
| NTT Communication Science Laboratories, Nippon Telegraph and Telephone Corporation | ||||||||
| 著者名 |
櫟粛之
× 櫟粛之 |
|||||||
| 著者名(英) |
Tadashi, Araragi
× Tadashi, Araragi
|
|||||||
| 論文抄録 | ||||||||
| 内容記述タイプ | Other | |||||||
| 内容記述 | 本論文では，形式的検証機能を備えたエージェントプログラミングシステムを提案する．その言語は，if-thenルールに基づく単純なセマンティクスを持ち，またインターネットエージェントの動作を記述するには十分な，いくつかのエージェントのアクションが与えられている．形式的検証に関しては，CTLのモデルチェックアルゴリズムを利用する．その入力として，エージェントシステムの振舞いの論理的記述が必要であり，従来はこの記述を人手により作成していたが，ここで導入される言語では，それを自動的に合成することが可能になる．また，検証すべき要求仕様に対して，その仕様に関連するプログラムの部分だけを自動的に抽出する方法を導入し，自動合成される状態遷移の論理的記述を簡約化することも可能にした．この言語に対する処理系は，Java上のインタプリタとして実装されており，Jadeなどの他のエージェント開発・実行環境にひけをとらない実行スピードを実現している． | |||||||
| 論文抄録(英) | ||||||||
| 内容記述タイプ | Other | |||||||
| 内容記述 | In this paper, we present an Internet agent programming system with a formal verification facility for the agent programs. The language has a simple semantics of “if-then rule” and a few selected actions of agents which are enough to describe agents' behavior working in the Internet. For the verification, we employ the model checking algorithm of CTL as the base engine. The language is designed so that a logical representation of behavior of agents, an input of a CTL model checker, which was manually created by programmers, is automatically derived from the programs. We also introduce a method of reducing the logical representation of behavior by extracting a part of programs which is essentially related to a given requirement specification to be verified. This system is implemented on Java and shows practical speed of execution compared with other agent systems such as Jade. | |||||||
| 書誌レコードID | ||||||||
| 収録物識別子タイプ | NCID | |||||||
| 収録物識別子 | AA11464803 | |||||||
| 書誌情報 |
情報処理学会論文誌数理モデル化と応用（TOM） 巻 47, 号 SIG14(TOM15), p. 80-92, 発行日 2006-10-15 |
|||||||
| ISSN | ||||||||
| 収録物識別子タイプ | ISSN | |||||||
| 収録物識別子 | 1882-7780 | |||||||
| 出版者 | ||||||||
| 言語 | ja | |||||||
| 出版者 | 情報処理学会 | |||||||
