講演名 2003/11/21
離散確率分布を持つリアルタイムシステムの確率時間時相論理式の演繹的検証手法
山根 智,
PDFダウンロードページ PDFダウンロードページへ
抄録(和) 最近, リアルタイムシステムの不確かな動作を表現するために, 離散確率分布を持つ確率時間オートマトンが開発されており, そのモデル検査手法や確率時間模倣検証手法も開発されている. 本論文では, 確率時間オートマトンを一般化することにより, 確率時間遷移システムを開発して, その上に確率時間時相論理の演繹的な検証規則を開発する. 確率時間遷移システムは離散確率分布を持つリアルタイムシステムの一般的な計算モデルであり, 従来よりも一般的な検証手法が確立できた.
抄録(英) Especially, recently, probabilistic timed automata and their model-checking have been developed in order to express the relative likelihood of the system exhibiting certain behavior. Moreover, model-checking and probabilistic timed simulation verification methods of probabilistic timed automata have been developed. In this paper, we propose probabilistic timed transition system by generalizing probabilistic timed automata, arid propose deductive verification rules of probabilistic timed temporal logic over probabilistic timed transition system. As our proposed probabilistic timed transition system is a general computational model, we have developed general verification method.
キーワード(和) リアルタイムシステム / 確率時間時相論理 / 演繹的検証
キーワード(英) real-time systems / probabilistic timed temporal logic / deductive verification
資料番号 SS2003-29,KBSE2003-32
発行日

研究会情報
研究会 KBSE
開催期間 2003/11/21(から1日開催)
開催地(和)
開催地(英)
テーマ(和)
テーマ(英)
委員長氏名(和)
委員長氏名(英)
副委員長氏名(和)
副委員長氏名(英)
幹事氏名(和)
幹事氏名(英)
幹事補佐氏名(和)
幹事補佐氏名(英)

講演論文情報詳細
申込み研究会 Knowledge-Based Software Engineering (KBSE)
本文の言語 JPN
タイトル(和) 離散確率分布を持つリアルタイムシステムの確率時間時相論理式の演繹的検証手法
サブタイトル(和)
タイトル(英) Deductive Verification Method of Probabilistic Timed LTL of Real-Time Systems with Discrete Probability Distributions(Knowledge-Based Software Engineering)
サブタイトル(和)
キーワード(1)(和/英) リアルタイムシステム / real-time systems
キーワード(2)(和/英) 確率時間時相論理 / probabilistic timed temporal logic
キーワード(3)(和/英) 演繹的検証 / deductive verification
第 1 著者 氏名(和/英) 山根 智 / Satoshi YAMANE
第 1 著者 所属(和/英) 金沢大学工学部情報システム工学科
Faculty of Engineering, Kanazawa University
発表年月日 2003/11/21
資料番号 SS2003-29,KBSE2003-32
巻番号(vol) vol.103
号番号(no) 484
ページ範囲 pp.-
ページ数 6
発行日