Towards a Model-Based Verification Methodology for Complex Swarm Systems

The recent advances with respect to the costs, size, and power consumption of electronic components paved the way for System of Systems (SoS), Cyber-Physical Systems (CPS), or the Internet of Things (IoT). As a next stage, these developments currently motivate the consideration of Complex Swarm Systems (CSS), i. e., continuously running systems that will dynamically change after deployment and are connected by heterogeneous components which can join and leave the system at any time. Due to this dynamic nature and the constant reconfigurations, it is not possible to completely verify those systems with conventional verification methods anymore. Therefore, we propose a new methodology which follows a different scheme: Instead of trying to verify all possible behavior of a CSS (which, due to the vast number of possible instantiations or connections of the heterogeneous components, becomes an impracticable task anyway), we aim for verifying that, at least, no scenario which violates certain (safety-critical) forbidden actions is possible. To this end, solutions for model-based verification are employed. By means of a case study, the feasibility and promises of the proposed methodology are illustrated.