Some of the most exciting cyber technologies on the research horizon involve sophisticated digital systems that interact with the physical world. Examples include remote surgery, physical manipulation of nano-structures, autonomous (ground and air) vehicular travel, and space and terrestrial exploration. Because such applications interact directly with the physical world, it is imperative their physical safety be assured. This project is developing a comprehensive formal framework for producing controllers for cyber-physical systems, with machine checkable proofs of their physical safety. The project brings together ideas from control theory, language design, program verification, program generation, software engineering, and real-time and embedded systems to build a framework that can be applied to challenging applications. The framework promotes an efficient, rigorous engineering process for producing embedded controllers, incorporating explicit models not only of the controller itself, but also of the physical context in which it operates, the required stability conditions, the platform on which it will run, and the associated real-time constraints. The results of the project are being demonstrated and evaluated in the context of a tele-surgery application. This application is currently being developed at the Mechatronics and Haptic Interfaces Lab in the Mechanical Engineering Department at Rice University.
