This project develops a theoretical framework as well as software tools to support testing and verification of a Cyber-Physical System (CPS) within a Model-Based Design (MBD) process. The theoretical bases of the framework are stochastic optimization methods, and robustness notions of formal specification languages. The project's research comprises three components: development of conditions on the algorithms and on the structure of the CPS for inferring finite-time guarantees on the randomized testing process; the study of testing methods that can support modular and compositional system design; and investigation of appropriate notions of conformance between two system models and between a model and its implementation on a computational platform. All of these components are needed to support testing and verification in all the stages of an MBD process as well as to support component reuse, incremental system improvements and modular design. The evaluation of the framework is driven by the problems of verifying automotive control systems and medical devices. As safety-critical CPS become ubiquitous, the need for design methods that guarantee correct system functionality and performance becomes more urgent. Certification and government agencies need dependable testing and verification tools to incorporate in certification standards and procedures. The concrete benefits to the society are both in terms of reduced catastrophic design errors in new products and in terms of reduced economic costs for new product development. The former increases the confidence in new technologies while the latter improves the competitiveness of the companies that utilize such technologies. The theoretical results of this project are being incorporated into software tools for testing, verification and validation of complex CPS. The evaluation focus of the project on verifying infusion pumps and automotive control software ultimately helps in avoiding harmful losses due to errors in these safety-critical systems. The use of any software tool that is based on formal or semi-formal methods requires engineers with solid training on these technologies. This proposal puts forward an education curriculum for developing new courses that introduce formal and semi-formal methods for CPS at all levels of higher education, i.e., undergraduate, graduate and continuing education. Particular attention is devoted into on-line continuing education of practicing engineers who must acquire new MBD skills.

The objective of this project is to create a focused cyber-physical design environment to accelerate the development of miniature medical devices in general and swallowable systems in particular. The project develops new models and tools including a web-based integrated simulation environment,capturing the interacting dynamics of the computational and physical components of devices designed to work inside the human body, to enable wider design space exploration, and, ultimately, to lower the barriers which have thus far impeded system engineering of miniature medical devices. Currently, a few select individuals with deep domain expertise create these systems. The goal is to open this field to a wider community and at the same time create better designs through advanced tool support. The project defines a component model and corresponding domain-specific modeling language to provide a common framework for design capture, design space exploration, analysis and automated synthesis of all hardware and software artifacts. The project also develops a rich and extensible component and design template library that designers can reuse. The online design environment will provide early feedback and hence, it will lower the cost of experimentation with alternatives. The potential benefit is not just incremental (in time and cost), but can lead to novel ideas by mitigating the risk of trying unconventional solutions. Trends in consumer electronics such as miniaturization, low power operation, and wireless technologies have enabled the design of miniature devices that hold the potential to revolutionize medicine. Transformational societal public health benefits (e.g., early diagnosis of colorectal cancer or prevention of heart failure) are possible through less invasive and more accurate diagnostic and interventional devices. By eliminating large incisions in favor of natural orifices or small ports, these medical devices can increase diagnostic screening effectiveness and reduce pain and recovery time. Furthermore, if successful, the proposed scientific approach can be extended to any other application, wherever size, power efficiency, and high confidence are stringent requirements. The educational plan of the project is centered on the web-based design environment that will also contain an interface for high school students to experiment with medical cyber-physical devices in a virtual environment. Students will be able to build medical devices from a library of components, program them using an intuitive visual programming language and operate them in various simulated environments. A Summer Camp organized in the framework of this project will enhance students learning experience with real hands-on experimentation in a lab.