Tool orchestration for modeling, verification and analysis of collaborating autonomous machines

System-of-systems (SoS) is a collective of multiple system units that have a common purpose. In this thesis, the Volvo Electric Site is investigated as an example case study in which safety and performance properties of collaborating autonomous machines are evaluated and analyzed. Formal methods in software engineering aim to prove the correctness of the system by evaluating its mathematical model. We use an actor-based framework, AdaptiveFlow, for modeling system functionalities and timing features. The aim is to link an abstract model evaluation and a simulation of real-world cases that are deployed in the VCE Simulator. In addition, it is necessary to make sure that AdaptiveFlow provides correct-by-design scenarios. The verification is conducted by developing an orchestration method between the AdaptiveFlow framework and the VCE Simulator. A tool named VMap is developed throughout this thesis for automated mapping of the input models of AdaptiveFlow and the VCE Simulator to make the orchestration possible. Furthermore, AdaptiveFlow is perceived in two different ways, as a design tool, and as an analysis tool. The models created in AdaptiveFlow are directly mapped to the VCE Simulator by using the VMap tool where the VCE Simulator is used as a testbed for checking these models. The outcome of this thesis is reflected in the establishment of a mapping pattern between AdaptiveFlow inputs and VCE simulator by developing the VMap tool for automatic mapping. It was shown that there is a natural mapping between the AdaptiveFlow models and VCE simulator inputs. By using VMap, we can quickly get to the desired scenarios. Through the development of three different cases, the results show that it is possible to design safe and optimal scenarios by orchestrating the AdaptiveFlow and the VCE Simulator using the VMap tool as well as the correlation between results from AdaptiveFlow and VCE Simulator