Modular self-reconfigurable robot (MSRR) systems consist of repeated robot elements (called modules) that connect together to form larger robotic structures (called configurations). Compared with conventional robot systems, MSRR systems are versatile, robust, and low cost. Especially their ability to self-reconfigure: changing the connective structure of the modules, allows them to gain new capabilities, adapt to new environments, and accomplish a wide range of tasks. However, the flexibility comes with challenges when controlling the modular robots: given a task, how does one select an appropriate configuration (robot shape) and behavior (controlling program) to accomplish it? This important problem is a significant barrier to the use of modular robots for solving real-world problems. The goal of this work is to develop a system to automatically generate correct-by-construction controllers for MSRR systems and accomplish high-level tasks in unknown environment using configurations and behaviors from a robot design library. In this work, I first present an end-to-end system that allows users to control a MSRR system to perform complex tasks specified in high-level instructions. At the low-level, the system allows users to create and organize a library of configurations and behaviors for modular robots. Each behavior is labeled with quantitative properties that specify the capability of the behavior. At the high-level, instead of selecting configurations and behaviors from the library to complete a robot task, users give high-level specification and describe desired actions using properties from the design library. By combining both low-level and high-level aspects, the system can control a MSRR system to achieve robot tasks by automatically choosing and composing configurations and behaviors. I then introduce concepts of environment properties and parametric behaviors to the system. Environment properties specify the environment constraints for correct execution of a behavior in the robot library. The system then selects appropriate behaviors based on the sensed environment to satisfy the task. The system also controls the MSRR system to automatically self-reconfigure, if a change of configuration is needed. Parametric behaviors are a set of behaviors whose commands are computed at run-time. Using robot perception information, the system can then generate reactive robot motions to traverse complex environment. The end-to-end system uses an existing discrete controller synthesis framework to generate controller from user tasks specifications. My last contribution presents a method to integrate continuous metrics to the controller synthesis framework. I defined a two dimensional cost metric that captures both the cost from robot actions and the cost due to adversarial environment. By assigning costs to transitions in the discrete controller and minimizing the overall costs, this method creates optimal robot actions with respect to given cost metrics. This contribution makes the controller synthesis framework more suitable for real world robot tasks.