PRTS: An approach for model checking probabilistic real-time hierarchical systems
Model Checking real-life systems is always difficult since such systems usually have quantitative timing factors and work in unreliable environment. The combination of real-time and probability in hierarchical systems presents a unique challenge to system modeling and analysis. In this work, we deve...
محفوظ في:
| المؤلفون الرئيسيون: | , , , , |
|---|---|
| التنسيق: | text |
| اللغة: | English |
| منشور في: |
Institutional Knowledge at Singapore Management University
2011
|
| الموضوعات: | |
| الوصول للمادة أونلاين: | https://ink.library.smu.edu.sg/sis_research/5029 https://ink.library.smu.edu.sg/context/sis_research/article/6032/viewcontent/prts.pdf |
| الوسوم: |
إضافة وسم
لا توجد وسوم, كن أول من يضع وسما على هذه التسجيلة!
|
| الملخص: | Model Checking real-life systems is always difficult since such systems usually have quantitative timing factors and work in unreliable environment. The combination of real-time and probability in hierarchical systems presents a unique challenge to system modeling and analysis. In this work, we develop an automated approach for verifying probabilistic, real-time, hierarchical systems. Firstly, a modeling language called PRTS is defined, which combines data structures, real-time and probability. Next, a zone-based method is used to build a finite-state abstraction of PRTS models so that probabilistic model checking could be used to calculate the probability of a system satisfying certain property. We implemented our approach in the PAT model checker and conducted experiments with real-life case studies. |
|---|