Modeling and Analysis of Probabilistic Timed Systems

Author

Dubey, Abhishek ; Riley, Derek ; Abdelwahed, Sherif ; Bapty, Ted

Author_Institution

Inst. for Software Integrated Syst., Vanderbilt Univ., Nashville, TN

fYear

2009

fDate

14-16 April 2009

Firstpage

69

Lastpage

78

Abstract

Probabilistic models are useful for analyzing systems which operate under the presence of uncertainty. In this paper, we present a technique for verifying safety and liveness properties for probabilistic timed automata. The proposed technique is an extension of a technique used to verify stochastic hybrid automata using an approximation with Markov Decision Processes. A case study for CSMA/CD protocol has been used to show case the methodology used in our technique.

Keywords

Markov processes; approximation theory; decision theory; formal verification; probabilistic automata; stochastic automata; systems analysis; Markov decision process; approximation theory; liveness property verification; probabilistic timed automata; probabilistic timed system analysis; safety property verification; stochastic hybrid automata; Access protocols; Automata; Biological system modeling; Biological systems; Firewire; Multiaccess communication; Performance analysis; Probability distribution; Real time systems; Uncertainty; Probabilistic Systems; Timed Automata; Verification;

fLanguage

English

Publisher

ieee

Conference_Titel

Engineering of Computer Based Systems, 2009. ECBS 2009. 16th Annual IEEE International Conference and Workshop on the

Conference_Location

San Francisco, CA

Print_ISBN

978-0-7695-3602-6

Type

conf

DOI

10.1109/ECBS.2009.44

Filename

4839233