Title :
Development of probabilistic timed CEGAR
Author :
Yamane, Satoshi ; Shimizu, Tsuyoshi
Author_Institution :
Kanazawa Univ., Kanazawa, Japan
Abstract :
In this paper, we present an efficient verification method for probabilistic timed automaton. This method based on predicate abstractions and refinements realizes effective automated verifications for real-time and probabilistic embedded systems.
Keywords :
embedded systems; formal verification; probabilistic automata; counterexample guided abstraction refinement; probabilistic embedded systems; probabilistic timed CEGAR; probabilistic timed automaton; real-time embedded systems; verification method; Abstracts; Automata; Clocks; Cost accounting; Markov processes; Probabilistic logic; Probability distribution; CEGAR(Counter Example Guided Abstraction Refinement); model checking; predicate abstraction; probabilistic timed automaton;
Conference_Titel :
Systems and Informatics (ICSAI), 2014 2nd International Conference on
Conference_Location :
Shanghai
Print_ISBN :
978-1-4799-5457-5
DOI :
10.1109/ICSAI.2014.7009336
