HVC case study - verification using PRISM

Introduction

The RoboChart model for this High Voltage Controller (HVC) case study is not a probabilistic model. In addition to verify it using FDR, we also analyse it using PRISM throught its support in RoboTool.

Please find its RoboChart model on RoboStar website or on Github. Its verification using FDR is discussed in the paper “Safety Assurance of a High Voltage Controller for an Industrial Robotic System” and the verification results using PRISM is shown on Github.