Case Studies

Below is a list of case studies considered in the context of RoboStar projects. They are grouped by category: RoboChart, RoboSim: control software modelling, and RoboSim: physical modelling. To see the full list of case studies under a particular category click on Show all.

RoboChart

Case studies with control software specified using RoboChart. The following models have been specified and analysed using RoboTool. The version of RoboTool used for each case study is linked.

Untimed and timed models (19)

Case studies with both untimed and timed aspects.

• Autonomous Chemical Detector

  Authors: A. Miyazawa and A. L. C. Cavalcanti
  RoboTool version: 3.0.0.202108031246

Alpha Algorithm

Authors: A. Miyazawa, P. Ribeiro and A. L. C. Cavalcanti
RoboTool version: 3.0.0.202108031246

Robot-assisted dressing

Authors: T. Wright


Firefighting UAV

Authors: A. Cavalcanti, P. Ribeiro and M. Windsor


Segway

Authors: Z. Atalla, J. Baxter, A. Cavalcanti and M. C. Filho


Sandwich Maker Arm

Authors: Sharar Ahmadi


ABB paint robot (High-Voltage Control system)

Authors: Y. Murray, M. Sirevåg, P. Ribeiro', D. A. Anisi and M. Mossige


SRanger

Authors: A. Miyazawa, P. Ribeiro, A. L. C. Cavalcanti, M. Windsor, J. Baxter and K. Ye


Autonomous Vehicle

Authors: W. Barnett, A. L. C. Cavalcanti and A. Miyazawa
RoboTool version: 1.0.0.201904021656

Exploration

Authors: P. Ribeiro and W. Li
RoboTool version: 1.0.0.201710231256

Solar Panel Vacuum Cleaner

Authors: Bianca Darolti
RoboTool version: 2.0.0.201907301544

Rescue Drone

Authors: A. L. C. Cavalcanti, J. Baxter, R. M. Hierons and R. Lefticaru
RoboTool version: >= 2.0.0

Environmental Sensing

Authors: W. Li and A. Miyazawa'
RoboTool version: 1.0.0.201709071350

Alpha Algorithm - Collection

Authors: A. Miyazawa, P. Ribeiro and A. L. C. Cavalcanti
RoboTool version: 1.0.0.201806131353

Transport

Authors: P. Ribeiro, W. Li, A. L. C. Cavalcanti and A. Sampaio
RoboTool version: 1.0.0.201710231256

Chemical Detector

Authors: A. Miyazawa and A. L. C. Cavalcanti
RoboTool version: 1.0.0.201709071350

Omega Algorithm

Authors: A. Miyazawa


Humanoid

Authors: A. Miyazawa


Aggregation

Authors: A. Miyazawa

1. Show all 19 case studies

Probabilistic models (9)

Case studies with probabilistic aspects.

• UVC case study - verification using PRISM

  Authors: K. Ye and J. Woodcock
  RoboTool version: >= 3.0.0.2021080312460 (show plug-in versions)
  • Metamodel version: 2.0.0.202101141039
    Textual version: 2.0.0.202012181050
    Graphical version: 2.0.0.202012181055
    CSP Generator version: 2.0.0.202102221504
    PRISM Generator version: 2.0.0.202103111643
    Assertion version: 2.0.0.202103110835

A simple bounded random walk - a probabilistic model

Authors: K. Ye and J. Woodcock
RoboTool version: >= 3.0.0.2021080312460 (show plug-in versions)

• Metamodel version: 2.0.0.202101141039
  Textual version: 2.0.0.202012181050
  Graphical version: 2.0.0.202012181055
  CSP Generator version: 2.0.0.202102221504
  PRISM Generator version: 2.0.0.202103111643
  Assertion version: 2.0.0.202103110835

HVC case study - verification using PRISM

Authors: K. Ye and J. Woodcock
RoboTool version: >= 3.0.0.2021080312460 (show plug-in versions)

• Metamodel version: 2.0.0.202101141039
  Textual version: 2.0.0.202012181050
  Graphical version: 2.0.0.202012181055
  CSP Generator version: 2.0.0.202102221504
  PRISM Generator version: 2.0.0.202103111643
  Assertion version: 2.0.0.202103110835

Simplified form of the RANSAC algorithm

Authors: K. Ye and J. Woodcock
RoboTool version: >= 2.0.0.202010050800 (show plug-in versions)

• Metamodel version: 2.0.0.202101141039
  Textual version: 2.0.0.202012181050
  Graphical version: 2.0.0.202012181055
  CSP Generator version: 2.0.0.202102221504
  PRISM Generator version: 2.0.0.202103111643
  Assertion version: 2.0.0.202103110835

Foraging Robot

Authors: K. Ye and J. Woodcock
RoboTool version: >= 2.0.0.202010050800 (show plug-in versions)

• Metamodel version: 2.0.0.202010051541
  Textual version: 2.0.0.202011171214
  Graphical version: 2.0.0.202010051549
  CSP Generator version: 2.0.0.202010051628
  PRISM Generator version: 2.0.0.202011230818
  Assertion version: 2.0.0.202010051551

Tutorial: probabilistic verification in RoboTool

Authors: K. Ye
RoboTool version: >= 2.0.0 (show plug-in versions)

• Metamodel version: 2.0.0.201908011257
  Textual version: 2.0.0.201908190859
  Graphical version: 2.0.0.201908190914
  CSP Generator version: 2.0.0.201908161629
  PRISM Generator version: 2.0.0.201908200950
  Assertion version: 2.0.0.201908191015

Six-sided Die

Authors: K. Ye
RoboTool version: >= 2.0.0.202010050800 (show plug-in versions)

• Metamodel version: 2.0.0.202010051541
  Textual version: 2.0.0.202011171214
  Graphical version: 2.0.0.202010051549
  CSP Generator version: 2.0.0.202010051628
  PRISM Generator version: 2.0.0.202011230818
  Assertion version: 2.0.0.202010051551

Random Walker

Authors: J. Woodcock and K. Ye
RoboTool version: >= 2.0.0.202010050800 (show plug-in versions)

• Metamodel version: 2.0.0.202101141039
  Textual version: 2.0.0.202012181050
  Graphical version: 2.0.0.202012181055
  CSP Generator version: 2.0.0.202102221504
  PRISM Generator version: 2.0.0.202103111643
  Assertion version: 2.0.0.202103110835

Internal Mail Delivery Robot

Authors: K. Ye
RoboTool version: >= 2.0.0.202010050800 (show plug-in versions)

• Metamodel version: 2.0.0.202101141039
  Textual version: 2.0.0.202012181050
  Graphical version: 2.0.0.202012181055
  CSP Generator version: 2.0.0.202102221504
  PRISM Generator version: 2.0.0.202103111643
  Assertion version: 2.0.0.202103110835
1. Show all 9 case studies

RoboSim: control software modelling

Case studies with control software specified using RoboSim.

• Segway

  Authors: Z. Atalla, J. Baxter, A. Cavalcanti and M. C. Filho
  

Sandwich Maker Arm

Authors: Sharar Ahmadi


SRanger

Authors: A. Miyazawa, P. Ribeiro, A. L. C. Cavalcanti, M. Windsor, J. Baxter and K. Ye


Transport

Authors: P. Ribeiro, W. Li, A. L. C. Cavalcanti and A. Sampaio
RoboTool version: 1.0.0.201710231256
1. Show all 4 case studies

RoboSim: physical modelling

Case studies with physical models specified using RoboSim.

• MarxBot: RoboSim Physical Model

  Authors: Alvaro Miyazawa
  

Robot-assisted dressing

Authors: T. Wright


Firefighting UAV

Authors: A. Cavalcanti, P. Ribeiro and M. Windsor


Sandwich Maker Arm

Authors: Sharar Ahmadi and Alvaro Miyazawa


SRanger

Authors: A. Miyazawa, P. Ribeiro, A. L. C. Cavalcanti, M. Windsor, J. Baxter and K. Ye


Two Link

Authors: Alvaro Miyazawa


Two Bodies

Authors: Alvaro Miyazawa


Solar Panel Vacuum Cleaner

Authors: Sharar Ahmadi
RoboTool version: 2.0.0.201907301544
1. Show all 8 case studies

RoboWorld

Case studies with environment assumptions specified using RoboWorld.

• Firefighting UAV

  Authors: A. Cavalcanti, P. Ribeiro and M. Windsor
  

SRanger

Authors: A. Miyazawa, P. Ribeiro, A. L. C. Cavalcanti, M. Windsor, J. Baxter and K. Ye


Rescue Drone

Authors: A. L. C. Cavalcanti, J. Baxter, R. M. Hierons and R. Lefticaru
RoboTool version: >= 2.0.0
1. Show all 3 case studies