Department of Computer Science

HVC case study - verification using PRISM


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.

Department of Computer Science
Deramore Lane, University of York, Heslington, York, YO10 5GH, UK
Tel: 01904 325500
University of York legal statements