Tutorial: probabilistic verification in RoboTool
This is a tutorial about how to use RoboTool for probabilistic verification with the PRISM model checker.
Prerequisites
- Install Eclipse 2019-03 and choose Eclipse IDE for Java Developers
- Install RoboTool plugins: [Eclipse > Help > Install New Software …], add “https://www.cs.york.ac.uk/robostar/robotool/update”, and then select
- “RoboChart Ecore Modelling”,
- “RoboChart Textual Editor”,
- “RoboChart Graphical Editor”,
- “RoboChartPRISMGenerator”,
- and “Assertions Editor”.
- Install Epsilon plugins: [Eclipse > Help > Install New Software …], add “http://download.eclipse.org/epsilon/updates”, and then select
- “Epsilon Core”,
- “Epsilon Core Development Tools”,
- and “Epsilon Development Tools for EMF” under “Epsilon EMF Integration”.
- Install the PRISM model checker in your system and add its /pathToPrism/bin to PATH
Tutorial
Download the RoboChart model from here, then follow the video to verify a very simple RoboChart model.
References