MOdel COmpiler (MOCO)
This is the documentation of MOCO, a mantainability fork of AS2FM, originally developed from the CONVINCE project. Besides illustrative tutorials on how to use the provided scripts, the API is documented to foster contributions from users outside of the core project’s team.
Overview
The purpose of the provided program is to convert all specifications of components of the given robotic system into a format which can be given as input to model checkers for verifying the robustness of the system functionalities. It is intended for use with GRAPE and SCAN, respectively a development tool and a model checker.
MOCO focuses on converting the RoaML model of the system into a plain SCXML format that can be used by model checking tools such as SCAN. A full robotic system and the information needed for model checking consists of:
one or multiple ROS nodes in (A)SCXML,
the environment model in (A)SCXML,
the Behavior Tree in XML,
the plugins of the Behavior Tree leaf nodes in (A)SCXML
The full bundle of files is converted to an equivalent model in plain SCXML, which can be directly verified using model checkers such as SCAN.
A tutorial on how to use the conversion script can be found in the tutorial section.