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.
The project developed a framework to support the design of controllers for cyber-physical systems (CPS). Intellectual Impact The goal of this project was to develop a deeper understanding of the issues involved in designing novel cyber-physical systems with strong safety properties. The idea was to consider the behavior of an embedded (digital) controller in the context of the physical system it controls. Initial analysis of the CPS design process for robots revealed that modeling and simulation tools play a key role in this process. This analysis also identified ways in which current tools impede productivity. As a result, the project undertook several activities aimed at addressing these problems. The results of these activities can be classified into four broad categories: Establishing timing and schedulability bounds (under different constraints) for P-FRP, a functional, priority-based formalism for specifying discrete controllers. Developing an elegant functional model of hybrid systems (Yampa) that includes an equational theory for computing with the category-theoretic concept of arrows. Analysing case studies from robotic tele-operation and rigid-body dynamics. Rigid body dynamics is a representative example of a physical domain that exhibits key challenging features that arise in modeling and simulation of physical domains. Extending P-FRP with differential algebraic equations (DAEs) to create a unified modeling and simulation formalism for both discrete controllers and the physical processes that they control. Refining this formalism led to a more elegant core formalism (Acumen). The project generated numerous technical findings that were reported in scientific publications. Two key findings were that 1) raising the level of abstraction of modeling formalisms to mathematical equations can significantly improve the design process; and, more broadly, 2) the numerical methods used in mainstream simulation tools cast doubt on the utility of such simulations as valid virtual experiments. In future work, we expect that Acumen will be useful for exploring solutions to this problem. Broader Impact The project supported advanced education and mentoring for 12 graduate students and four undergraduate students, as well as one post-doctoral student. In addition to publications, dissemination activities of the project included several tours for K-12 students of the Mechatronics and Haptics Lab at Rice University. Finally, the modeling formalism integrating the various ideas developed under the project is published online as Free Software available from www.acumen-language.org
