Open Automata (OA) are symbolic and parameterized models for open concurrent systems, where open means partially specified systems, which can be instantiated or assembled to build bigger systems. In previous work, a notion of equivalence named FH-Bisimulation was defined for OA, coming with both Strong and Weak flavors, where Weak means ignoring internal moves when they do not affect the external behavior. Both flavors have been proven to be congruent for the OA’s composition. In this paper, we propose a new definition of (weak) OA, that is both more expressive for encoding the behavior of parameterized systems and suitable as a finite encoding of weak OA. We name this meta (weak) OA and provide two methods to check their equivalence, either explicitly building the meta-WOA, or constructing their meta open transitions on-demand. The last strategy has better termination properties.

Every day, numerous VMs are migrated inside a datacenter to balance the load, save energy or prepare production servers for maintenance. Although VM placement problems are carefully studied, the underlying migration schedulers rely on vague adhoc models. This leads to unnecessarily long and energy-intensive migrations. We present mVM, a new and extensible migration scheduler. To provide schedules with minimal completion times, mVM parallelizes and sequentializes the migrations with regards to the memory workload and the network topology. mVM is implemented as a plugin of BtrPlace and its current library allows administrators to address temporal and energy concerns. Experiments on a real testbed shows mVM outperforms state-of-the-art migration schedulers. Compared to schedulers that cap the migration parallelism, mVM reduces the individual migration duration by 20.4 percent on average and the schedule completion time by 28.1 percent. In a maintenance operation involving 96 VMs migrated between 72 servers, mVM saves 21.5 percent Joules against BtrPlace. Compared to the migration model inside the cloud simulator CloudSim, the prediction error of the migrations duration is about 5 times lower with mVM. By computing schedules involving thousands of migrations performed over various fat-tree network topologies, we observed that the mVM solving time accounts for about 1 percent of the schedule execution time.

This article studies Parameterised Networks of Automata (pNets) from a theoretical perspective. We illustrate the expressiveness of pNets by showing how to express a wide range of classical constructs of (value-passing) process calculi, but also how we can easily encode complex interaction patterns used in modern distributed systems. Our framework can model full systems, using (closed) hierarchies of pNets, we can also build (open) pNet systems expressing composition operators. Concerning more fundamental aspects, we define a strong bisimulation theory specifically for the pNet model, prove its properties, and illustrate it on some examples. One of the original aspects of the approach is to relate the compositional nature of pNets with the notion of bisimulation, this is exemplified by studying the properties of a flattening operator for pNets.