Department of Computer Science

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

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