ProHVer

 

Subproject

S3

Categories

Model checker for hard & soft real-time systems, Model checker / solver for probabilistic systems, Model checker / solver for hybrid systems

Overview

ProHVer is a tool to handle systems which feature both discrete and continuous behaviour, and also involves randomness. ProHVer is capable of computing the unbounded reachability probability for a very general class of probabilistic hybrid automata.

Publications

M. Fränzle, E.M. Hahn, H. Hermanns, N. Wolovick, and L. Zhang. Measurability and safety verification for stochastic hybrid systems. In 13th International Conference on Hybrid Systems: Computation and Control (HSCC 2011), 2011. To appear.

L. Zhang, Z. She, S. Ratschan, H. Hermanns, and E. Hahn. Safety verification for probabilistic hybrid systems. In Tayssir Touili, Byron Cook, and Paul Jackson, editors, Computer Aided Verification, volume 6174 of Lecture Notes in Computer Science (LNCS), pages 196-211, 2010.

E.M. Hahn, G. Norman, D. Parker, B. Wachter, and L. Zhang. Game-based Abstraction and Controller Synthesis for Probabilistic Hybrid Systems. In 8th International Conference on Quantitative Evaluation of SysTems (QEST), 2011. To appear

Benchmarks

See depend.cs.uni-saarland.de/tools/prohver/casestudies/

Download

See depend.cs.uni-saarland.de/tools/prohver/

Manual

See depend.cs.uni-saarland.de/tools/prohver/

Status

Stable