www.prismmodelchecker.org
[MFH+14] Anitha Murugesan, Lu Feng, Mats Per Erik Heimdahl, Sanjai Rayadurgam, Michael W. Whalen and Insup Lee. Exploring the Twin Peaks using Probabilistic Verification Techniques. In Proc. 4th International Workshop on Twin Peaks of Requirements and Architecture (TwinPeaks'14), ACM. 2014. [Uses probabilistic verification and PRISM as part of an approach to analyse the co-evolution of system requirements and system architecture/design.]
Links: [Google] [Google Scholar]

Publications