2004年
Deductive probabilistic verification methods for embedded and ubiquitous computing
EMBEDDED AND UBIQUITOUS COMPUTING, PROCEEDINGS
- ,
- 巻
- 3207
- 号
- 1
- 開始ページ
- 183
- 終了ページ
- 195
- 記述言語
- 英語
- 掲載種別
- 出版者・発行元
- SPRINGER-VERLAG BERLIN
Many people have studied formal specification and verification methods of embedded and ubiquitous computing systems all over the world. We can specify real-time systems using timed automata, and verify them using model-checking. Especially, recently, probabilistic timed automata and their model-checking have been developed in order to express the relative likelihood of the distributed real-time systems 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 systems by generalizing probabilistic timed automata, and propose deductive verification rules of probabilistic real-time linear temporal logic over probabilistic timed transition systems. As our proposed probabilistic timed transition system is a general computational model, we have developed general verification methods.
- リンク情報
- ID情報
-
- ISSN : 0302-9743
- Web of Science ID : WOS:000223635900018