Publication Type

Conference Proceeding Article

Version

publishedVersion

Publication Date

10-2011

Abstract

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.

Keywords

Model Check, Mutual Exclusion, Linear Temporal Logic, Process Construct, Symbolic Model Check

Discipline

Programming Languages and Compilers | Software Engineering

Research Areas

Software and Cyber-Physical Systems

Publication

Proceedings of the 13th International Conference on Formal Engineering Methods, ICFEM 2011, Durham, UK, October 26-28

First Page

147

Last Page

162

ISBN

9783642245589

Identifier

10.1007/978-3-642-24559-6_12

Publisher

Springer Link

City or Country

Durham, UK

Additional URL

https://doi.org/10.1007/978-3-642-24559-6_12

Download

Share

COinS