This repository contains a RoboChart model for risk analysis of an agriculture robot providing UV light-treatment and a latest verification result in the folder prism-gen.
The model is probabilistic, and created in RoboTool. The properties to be verified are inside the folder Properties.
The model is also analysed in RoboTool by automatically
- translating it to a PRISM model,
- translating the properties to the PRISM properties,
- launching many PRISM model checker instances to verify properties, and
- collecting results (from log files such as this one) and generating a report.
Please refer to this paper "Probabilistic Modelling and Safety Assurance of an Agriculture Robot Providing Light-Treatment" for the details of this case study, and "Probabilistic modelling and verification using RoboChart and PRISM" for more information about the probabilistic modelling and verification for RoboChart.
The information about how to install RoboTool, open this model, and verify it in RoboTool can be found in the RoboTool manual. In particular, the plugins in the categories PRISM, RoboChart, RoboChart Generator, and Epsilon should be installed, and the chapter "Model Checking with PRISM" should be referred to.