Autonomous Systems to Formal Models (AS2FM) =============================================== This is the documentation of the AS2FM tools from the `CONVINCE project's <https://convince-project.eu/>`_ toolbox. Besides illustrative :doc:`tutorials <../tutorials>` on how to use the provided scripts, their :doc:`API <../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 <https://www.behaviortree.dev/docs/learn-the-basics/xml_format>`_ and :ref:`High-Level (HL)-SCXML<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 <https://github.com/convince-project/smc_storm>`_ for verifying JANI models and `SCAN <https://github.com/convince-project/SCAN>`_ to verify plain SCXML models.. .. image:: graphics/as2fm_overview.drawio.svg :alt: How AS2FM works :align: center A tutorial on how to use the conversion script can be found in the :doc:`tutorial section <../tutorials>`. Contents -------- .. toctree:: :maxdepth: 2 installation tutorials howto scxml-jani-conversion api contacts