# MASCOT Model and Data Matt Luckcuck 06-07-2020 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](https://cocotec.io/fdr/) and our Runtime Verification toolchain [Varanus](https://github.com/autonomy-and-verification-uol/varanus/tree/NFM-Data). ## 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](https://cocotec.io/fdr/), directly; and then using our [Varanus](https://github.com/autonomy-and-verification-uol/varanus/tree/iFM-Data) toolchain, both online and offline. 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]([Varanus](https://github.com/autonomy-and-verification-uol/varanus) ## Scenarios Briefly, the scenarios are: 1. Operator stays in hands on mode, speed stays below limit. 2. 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. 3. Operator switches to autonomous mode after collecting tools, speed stays below limit. 4. 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. 5. The Safe State Key is used to trigger an emergency stop. Then the system is reset, restarted, and the mission is completed. 6. 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. 7. 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 ('logs') and a spreadsheet of the FDR and Varanus results * model: the CSP model of the safety sub-system, including the stress-test ('scenarios-stress-tests.csp' and scenario ('scenarios.csp') traces


    Zugriff

    Download


    Exportieren, teilen und zitieren



    Titel :

    Varanus: MASCOT Model and Data


    Beteiligte:
    Luckcuck, Matt (Autor:in)

    Erscheinungsdatum :

    2020-07-06



    Medientyp :

    Forschungsdaten


    Format :

    Elektronische Ressource


    Sprache :

    Englisch


    Klassifikation :

    DDC:    629




    Varanus: MASCOT Model and Data

    Luckcuck, Matt | BASE | 2021

    Freier Zugriff

    MASCOT RETRACTION MECHANISM

    MOLYNEUX DAVID | Europäisches Patentamt | 2023

    Freier Zugriff

    Mascot retraction mechanism

    DAVID MOLYNEUX | Europäisches Patentamt | 2023

    Freier Zugriff

    Mascot retarction mechanism

    Europäisches Patentamt | 2019

    Freier Zugriff

    Mascot retraction mechanism

    MOLYNEUX DAVID / CROWE STEVE / WENTWORTH PAUL | Europäisches Patentamt | 2024

    Freier Zugriff