Robots are increasingly changing how we work and play, but the way software is developed to control these machines is costly, because it involves so much trial and error. The RoboStar group, involving researchers in York, Sheffield, and several other institutions around the world, is designing a model-based approach for validation, verification, and automatic generation of code and tests. The mathematical underpinning of the techniques provides assurance of soundness of all artefacts. The goal is to enable development of control software for robotics of better quality at a lower cost. In this talk, we will give an overview of our motivation, approach, and current and future work.