Occamプログラム検証への時相論理の応用

• 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 Electric Mfg. Co., Ltd
• 著者所属(英): en
• 著者所属(英): YASKAWA Electric Mfg. Co., Ltd
• 著者名: 佐藤, 賢二; 元村, 直行; 荒木, 啓二郎
• 著者名(英): Kenji, Satou; Naoyuki, Motomura; Keijiro, Araki
• 論文抄録 / 内容記述タイプ: Other
• 論文抄録 / 内容記述: Occamで記述されたプログラムの検証を時相論理を用いて行う一手法を提案する．本手法では，制限されたOccamプログラムにいくつかの変換規則を適用することにより，簡単な文法を持つ別の言語に変換し，その後，時相論理を用いて各種性質を証明する．この変換を行うことで，一時的な並列実行という複雑な計算列が直列化され，時相論理による検証が可能になる．また，本手法では，Occamプログラムに存在する様々な形態のデッドロックを統一的に扱うことができる．尚，我々の目的の一つは，（株）安川電機製作所で開発された2腕衝突回避システムの検証を行うことである．
• 論文抄録(英) / 内容記述タイプ: Other
• 論文抄録(英) / 内容記述: A verification technique for Occam programs using temporal logic is presented. In this technique, first, some transformation rules are applied to restricted Occam programs so that these programs may be transformed into another language which has a simple syntax. Then, program properties are proved by temporal logic. This transformation serializes complex execution sequences such as temporary parallelism, and makes it possible to verity Occam programs using temporal logic. In this technique, various forms of deadlocks existing in Occam programs can be uniformly dealt with. One of our purposes is the verification of the transputer system which operates two robots without a collision. This system is developed in YASKAWA Electric Mfg. Co., Ltd.
• 書誌レコードID / 収録物識別子タイプ: NCID
• 書誌レコードID / 収録物識別子: AN10485570
• 書誌情報: 情報処理学会研究報告プログラミング（PRO）; 巻 1988, 号 94(1988-PRO-027), p. 59-68, 発行日 1988-12-09
• Notice: SIG Technical Reports are nonrefereed and hence may later appear in any journals, conferences, symposia, etc.
• 出版者 / 言語: ja
• 出版者: 情報処理学会