[MSHA17] Mujahid Mohsin, Muhammad Usama Sardar, Osman Hasan and Zahid Anwar. IoTRiskAnalyzer: A Probabilistic Model Checking Based Framework for Formal Risk Analytics of the Internet of Things. IEEE Access, IEEE. 2017. [Presents a framework for formally quantifying risk in Internet of Things applications, using PRISM as the underlying probabilistic model checker.]