Challenges and Opportunities in Model Checking Large-scale Distributed Systems

Many modern distributed systems are required to scale in terms of their support for processes, resources, and users. Moreover, a system is often also required to operate across the Internet and across different administrative domains. These scalability requirements lead to a number of well-known challenges in which distribution transparency needs to be traded off against loss of performance. We concentrate on two major challenges for which we claim there is no easy solution. These challenges originate from the fact that users and system are becoming increasingly integrated and are effectively leading us to large-scale socio-technical distributed systems. We identify the design of such integrated systems as one challenge, in particular when it comes to placing humans in the loop as a necessity to proper operation of the system as a whole. As users are so tightly integrated into the overall design, and systems naturally expand through composition, we will be facing problems with respect to long-term management, which we identify as another major challenge.