The methodology instantiates the white-box approach for adaptation, and has been developed to specify and analyze adaptive systems in Rewriting Logic. Validation has been performed for self-assembly strategies, a mechanism allowing groups of simple entities to act as a single complex entity exhibiting emergent behaviors. Notable examples include bacteria or insect swarms, modular and self-assembling robots, and software components with dynamic coupling mechanisms.

The distinguishing features of this approach are:

• adaptation based on the notion of control data;
• a hierarchical architecture to modularize the design;
• computational reflection as the main adaptation mechanism;
• probabilistic rule-based specifications and quantitative verification techniques to specify and analyze the adaptation logic.

The approach has been implemented in the Maude-based tool MESSI, which allows us to easily model robotic self-assembly strategies exploiting a predefined library of basic robotic controllers, debug and validate them via animated simulations, and estimate their quantitative properties via the statistical model checker MultiVeStA.

The picture concerns a scenario where robots self-assemble to cross a hole; it shows three states of a simulation (top), and the expected number of robots successfully crossing the hole with a varying of the number of robots and of the assembly strategy.

Further Information:

• User Guide
• Download