DOI: 10.5281/zenodo.3932004
title: Varanus: MASCOT Model and Data

description: MASCOT Model and Data Matt Luckcuck m.luckcuck@tutanota.com 2021-05-14 A Communicating Sequential Processes (CSP) model of the MASCOT v.6 Safety Sub-System and the response time data from checking various traces using FDR and our Runtime Verification toolchain Varanus. Description The CSP model was built from a natural-language report of the (proposed) safety sub-system for the tele-operated robotic system MASCOT. A set of traces were constructed to test the model: Stress-Testing: increasingly large, semi-random traces to test how model-checking/Varanus response times scale, and; Scenarios: different 'attempts' at a hypothetical mission, designed to test all of the safety functions in the model. Each trace was checked using FDR's API directly; and then using our Varanus toolchain for Offline RV. The check is to determine if the trace is a valid trace of the model. Further description of our toolchain and a link to relevant paper(s) can be found in the Varanus repository Scenarios Briefly, the scenarios are: Operator stays in hands on mode, speed stays below limit. Operator stays in hands on mode, speed exceeds limit and tries to continue (causes a failure). 2a Instead of the failure in Scenario 2, the system handles the broken speed limit, then resets, restarts, and finishes the mission. 2b Instead of the failure in Scenario 2, the system handles the broken speed limit, the safe state key is removed, to allow minor servicing to the system. Then the key is returned, the system is reset, restarted, and the mission is completed. Operator switches to autonomous mode after collecting tools, speed stays below limit. Operator switches to autonomous mode after collecting tools, speed exceeds limit and tries to continue (causes a failure). 4a Instead of the failure in Scenario 4, the system handles the broken speed limit, then resets, restarts, and finishes the mission. 4b Instead of the failure in Scenario 4, the system handles the broken speed limit, then safe state key is removed, to allow minor servicing to the system. Then the key is returned, the system is reset, restarted, and the mission is completed. The Safe State Key is used to trigger an emergency stop. Then the system is reset, restarted, and the mission is completed. System enters Master Commissioning Mode. After some unmonitored movements (not triggering protective stop), Safe State Key is used to enter Safe State, and system is reset. The Slave Commissioning Mode key is used to put the system into the Slave Commissioning Mode, where no speed events are registered. Then Slave Commissioning Mode is disabled, again using the Slave Commissioning Mode key. Structure data: the raw log files and a spreadsheet of the FDR API and Varanus results: <code>api-times</code> contains the results for using the FDR API directly, <code>offline-times</code> contains the results for using Varanus for Offline RV, <code>online-time</code> contains the results for using Varanus for Online RV on one scnerio only, <code>varanus-data.ods</code> contains the summary of the results for each stress-test or scenario model: the CSP model of the safety sub-system, including the stress-test (<code>scenarios-stress-tests.csp</code> and scenario (<code>scenarios.csp</code>) traces