WEKO3
アイテム
Occamプログラム検証への時相論理の応用
https://ipsj.ixsq.nii.ac.jp/records/31039
https://ipsj.ixsq.nii.ac.jp/records/310395a650ea5-aaaf-4f8b-a852-a1f8090746c1
| 名前 / ファイル | ライセンス | アクション |
|---|---|---|
IPSJ-PRO88019007.pdf (816.5 kB)
|
Copyright (c) 1988 by the Information Processing Society of Japan
|
|
| オープンアクセス | ||
| Item type | SIG Technical Reports(1) | |||||||
|---|---|---|---|---|---|---|---|---|
| 公開日 | 1988-12-09 | |||||||
| タイトル | ||||||||
| タイトル | Occamプログラム検証への時相論理の応用 | |||||||
| タイトル | ||||||||
| 言語 | en | |||||||
| タイトル | Application of Temporal Logic to Verification of Occam Programs | |||||||
| 言語 | ||||||||
| 言語 | jpn | |||||||
| 資源タイプ | ||||||||
| 資源タイプ識別子 | http://purl.org/coar/resource_type/c_18gh | |||||||
| 資源タイプ | technical report | |||||||
| 著者所属 | ||||||||
| 九州大学工学部情報工学科 | ||||||||
| 著者所属 | ||||||||
| （株）安川電機製作所 | ||||||||
| 著者所属 | ||||||||
| 九州大学工学部情報工学科 | ||||||||
| 著者所属(英) | ||||||||
| en | ||||||||
| Kyushu University | ||||||||
| 著者所属(英) | ||||||||
| en | ||||||||
| YASKAWA Electrlc Mfg. co., Ltd | ||||||||
| 著者所属(英) | ||||||||
| en | ||||||||
| Kyushu University | ||||||||
| 著者名 |
佐藤, 賢二
× 佐藤, 賢二
|
|||||||
| 著者名(英) |
Kenji, Satou
× Kenji, Satou
|
|||||||
| 論文抄録 | ||||||||
| 内容記述タイプ | Other | |||||||
| 内容記述 | Occamで記述されたプログラムの検証を時相論理を用いて行う一手法を提案する．本手法では，制限されたOccamプログラムにいくつかの変換規則を適用することにより，簡単な文法を持つ別の言語に変換し，その後，時相論理を用いて各種性質を証明する．この変換を行うことで，一時的な並列実行という複雑な計算列が直列化され，時相論理による検証が可能になる．また，本手法では，Occamプログラムに存在する様々な形態のデッドロックを統一的に扱うことができる．尚，我々の目的の一つは，（株）安川電機製作所で開発された2腕衝突回避システムの検証を行うことである． | |||||||
| 書誌レコードID | ||||||||
| 収録物識別子タイプ | NCID | |||||||
| 収録物識別子 | AN10485570 | |||||||
| 書誌情報 |
情報処理学会研究報告プログラミング（PRO） 巻 1988, 号 94(1988-PRO-019), p. 59-68, 発行日 1988-12-09 |
|||||||
| Notice | ||||||||
| SIG Technical Reports are nonrefereed and hence may later appear in any journals, conferences, symposia, etc. | ||||||||
| 出版者 | ||||||||
| 言語 | ja | |||||||
| 出版者 | 情報処理学会 | |||||||
