Autonomous Systems to Formal Models (AS2FM)
This is the documentation of the AS2FM tools from the CONVINCE project’s toolbox. Besides illustrative tutorials on how to use the provided scripts, their API is documented to foster contributions from users outside of the core project’s team.
Overview
The purpose of the provided components is to convert all specifications of components of the robotic system under investigation into a format which can be given as input to model checkers for verifying the robustness of the system functionalities.
AS2FM focuses on converting the model of the system, provided as a combination of Behavior Tree (BT) XML and High-Level (HL)-SCXML into a format that can be used by model checking tools (i.e. JANI or plain SCXML). A full robotic system and the information needed for model checking consists of:
one or multiple ROS nodes in SCXML,
the environment model in SCXML,
the Behavior Tree in XML,
the plugins of the Behavior Tree leaf nodes in SCXML,
the property to check in temporal logic, currently given in JANI, later support for XML will be added.
We offer a push-button solution for the full bundle conversion of all of those input files into one model-checkable format. We suggest using smc_storm for verifying JANI models and SCAN to verify plain SCXML models..
A tutorial on how to use the conversion script can be found in the tutorial section.