The formal modelling and verification of distributed systems represents a complex process in which multiple tools are involved. Rebeca is a language which is developed to make modelling and verification of distributed systems with asynchronous message passing easier. This chapter shows how different tool orchestration methods are used for developing different verification engines for Rebeca models. As the first step, the way of enabling performance evaluation for Rebeca models is shown. To this end, state spaces which are generated for Rebeca models are transformed to the input of a third party tool and the result of the verification is given to the modeller. The second one is developing a search-based optimisation for wireless sensors and actuators applications. Running the model checker in a loop with different input parameters helps in finding the optimum values for parameters with respect to a given optimisation goal. The third one is for safety verification and performance evaluation of collaborative autonomous machines of Volvo car. The verification is done through developing and evaluating models by the model checking tool and Volvo car simulator (VCE Simulator).