This entry documents the development of a model of a Osoyoo Segway robot. A full report is available.
A video of the robot in action can be seen below:
There are four versions of the RoboChart model, as documented in the report, available for download below.
This is a modified version of the Segway RoboChart model, which we refer to as Segway-Parallel. Here, we define each PID operation by a state machine. We enable a parallel description of the Segway model by allowing each PID to operate in any order. Each PID, however, can still only operate on specific update cycles, as indicated by the constants.
A version of the Segway RoboChart model that includes an artificial neural network component can be found in a repository. There, we also include artefacts related to the validation of the semantics of this version of the Segway model, and its verification with respect to the model(s) above. A report is available here.
Projects for the generation of mutants with Wodel and the comparison of mutants with the original model for the production of test traces are available below.
The automatically generated RoboSim model can be found in Segway-version4RC2RS.zip