DocumentCode
3477628
Title
Formal probabilistic refinement verification of embedded real-time systems
Author
Yamane, Satoshi
Author_Institution
Kanazawa Univ., Japan
fYear
2003
fDate
15-16 May 2003
Firstpage
79
Lastpage
82
Abstract
Generally, real-time systems have been specified using timed automata, and moreover model-checking methods of timed automata have been developed. On the other hand, recently, probabilistic timed automata have been developed in order to express the relative likelihood of the system exhibiting certain behavior. In this paper, we develop a verification method of the simulation relation of probabilistic timed automata, and apply this method into stepwise refinement developments of real-time systems.
Keywords
embedded systems; formal verification; probabilistic automata; refinement calculus; embedded real-time systems; formal verification; probabilistic timed automata; stepwise refinement; Automata; Cities and towns; Clocks; Context modeling; Cost accounting; Manuals; Probability distribution; Real time systems; Safety;
fLanguage
English
Publisher
ieee
Conference_Titel
Software Technologies for Future Embedded Systems, 2003. IEEE Workshop on
Print_ISBN
0-7695-1937-7
Type
conf
DOI
10.1109/WSTFES.2003.1201366
Filename
1201366
Link To Document