This report documents the RoboSim Models of the MarxBot; it includes the RoboSim Hardware Model, which was developed based on the paper “The marXbot, a miniature mobile robot opening new perspectives for the collective-robotic research” published here and a RoboSim Software Model. These models are avialalbe for download here. They have been formally verified using a variety of tools such as Isabelle/UTP, Flow*, Hyst, and SpaceEx, and the Analysis section summarises these results.
We have modelled three modules of the MarxBot, which are composed to form the robot.
The base module uses a Treel p-model to avoid duplication.
The Range and Bearings module uses indexed containment relations to avoid duplication as well.
Finally, the Rotating Scanner module defines a separate p-model for the long range infrared sensor, and composes it using indexed containments to include four copies in the p-model.
The SDF file can be downloaded here
The zipfile marxbot-verification.zip contains files establishing the verification of the property from section 7 of the paper “Verification with physical models in the loop”. It contains the following files and folders:
marxbot_model.thy - an Isabelle theory file containing mechanisations of the simplified semantics of the of the MarXbot d-model and the semantics of the MarXbot p-model
marxbot_equations.thy - an Isabelle theory file containing mechanisations of the equations of the MarXbot p-model
marxbot_proof.txt - a text file giving a proof of the property from the paper about the model encoded in Isabelle, supported by model checking using Flow*
marxbot_pmodel_monitor.xml - a model for the SpaceEx model checker written to check the main property within the proof to be used as input to Flow*
marxbot_pmodel_monitor.cfg - a SpaceEx configuration file, which contains values for the parameters of the model
marxbot_pmodel_monitor.model - a model for the Flow* model checker to check the property, created by translating from the SpaceEx model using the conversion tool Hyst, tuning the values of additional parameters required by Flow, since values for parameters like the time step are generated by Hyst from the SpaceEx configuration, but the values required for that are specific to the operation of Flow, and adding an unsafe set
marxbot_pmodel_evolution.model - a Flow* model containing a simplified version of marxbot_pmodel_monitor.model, used for determining the range of initial values to use in marxbot_pmodel_monitor.model
marxbot_monitor_output.txt - a file containing the terminal output from a run of Flow* on marxbot_pmodel_monitor.model, showing the result of Flow*’s safety checking
marxbot_evolution_output.txt - a file containing the terminal output from a run of Flow* on marxbot_pmodel_evolution.model
outputs - a folder containing output files generated by Flow* including .flow flowpipe files and .plt gnuplot plotting files
images - a folder containing encapsulated postscript images generated by running gnuplot on the .plt files from the outputs folder
The proof begins with an initial model created in Isabelle/UTP. This can be found in the files marxbot_equations.thy and marxbot_model.thy, and includes a mechanisation of the d-model and p-model semantics for the MarXbot, along with a mechanisation of the p-model equations. A proof is included that, with the addition of an equation T == 1/2mr^2*(d av/dt) to link the torque produced by the motor to the angular velocity of the wheel (based on the moment of inertia for a cylinder and ignoring friction on the wheels), the equations for the motors can be rearranged into a form more suitable for a model checker. The Isabelle/UTP files were produced using Isabelle2020, with a version of Isabelle/UTP taken from https://github.com/isabelle-utp/utp-main at commit c9122f143509aebc2ca273990a1e7c1a70609628.
The proof proceeds as shown in the file marxbot_proof.txt, starting with a refinement stating that the composition of the p-model and d-model refines the specification of the property given in the paper. The model is then manipulated by a series of reasoning steps to obtain the precondition at the start of the first execution of the ODEs, which is that LMotor_das and RMotor_das are both equal to lvel/0.025025, with lvel equal to 1 m/s in our case, and all other variables of the model equal to zero. These initial values are used as the initial values for evolution of the motor equations (in their rearranged form computed in marxbot_equations.thy) in marxbot_pmodel_evolution.model. The values for the constants used in the equations are Kp==1, Ki==0, Ke==0.0274, R==4, L==1E-3, Kt==0.0274, b==3.5077E-6, mass==0.0064925, radius==0.025025, which are given in the file marxbot_pmodel_monitor.cfg used in the conversion of the model using Hyst.
The plotting files produced from running marxbot_pmodel_evolution.model in Flow* provide the initial values for the checking of the property, since they represent the values taken by the variables during the initial acceleration of the robot, before it has detected an obstacle. The values produced for the torque, T, of the motors can be seen in Fig. 1. Replacing line 25 of marxbot_pmodel_evolution.model with “gnuplot octagon t,av” yields a plot of the values for the angular velocity, av, (Fig. 2), and similarly replacing it with “gnuplot octagon t,i” yields a plot of the values for the current, i, (Fig. 3). The range values obtained is 0 < av < 45 and -1 < i < 6, with the initial value for T computed from these values so as to better constrain the model.
The proof in marxbot_proof.txt proceeds by obtaining that the obstacle event occurs when an obstacle is in range of the robot’s sensor, and that causes the software to set the LMotor_das and RMotor_das to 0. The checking of the property that LMotor_T and RMotor_T get close to zero within maxTime is then achieved by running marxbot_pmodel_monitor.model in Flow* with the initial values computed from the previous steps. This model begins in the state Init, then computes the initial value for T and transitions to EvolvingPos or EvolvingNeg depending on whether the value is positive or negative. When the value of T gets close enough to zero from the direction it starts in, the model transitions to another state NearZero. If there is no transition to NearZero before the time becomes equal to maxTime, it transitions to a Timeout state. The Timeout state is marked as an unsafe state in the model, so Flow* checks that it is never reached. The result of this check can be seen at the end of the output in marxbot_monitor_output.txt, where the result is SAFE. The model was checked with eps = 0.000000001 and maxTime = 0.003, so this confirms that T comes within 1E-9 of zero before 0.003 seconds have elapsed.
This model was created using the RoboSim Physical Modelling Graphical Editor version 1.0.0.202009231212.
Department of Computer Science
Deramore Lane, University of York, Heslington, York, YO10 5GH, UK
Tel: 01904 325500
University of York legal statements