(CSR--EHS/CPS) Leveraging Type Systems for the Development of High-Assurance Cyber-Physical Systems and Appications

随着设备小型化和商品化的增加，新一代嵌入式实时系统，包括我们指定为网络物理结构（CPI）的系统，越来越多地嵌入到家庭、工作场所、学校、商场、机场、医院等的物理建筑中。由于其类似于公用事业的性质，CPI可能满足各种组成部分的需求，支持任何数量的应用，其中一些可能是关键的，而其他可能是可选的，甚至是娱乐性的。利用这样的CPI的力量将取决于一个精简的过程，相对简单的程序员能够快速开发和部署应用程序，而不必理解或担心底层的，可能复杂的CPI资源和运行时支持，同时允许对开发的应用程序进行安全属性的认证。该项目的重点是一个综合的方法来编程和安全验证的CPI应用程序，通过认识到“类型”和“类型系统”，这已被证明是有助于现代编程语言的发展，可用于封装安全属性相关的性能和可靠性的CPI应用程序。为此，本项目的目的是开发类型系统，能够支持CPI应用程序的实时和QoS属性的组合验证，将这些新的类型系统纳入高级编程语言，并在原型CPI应用程序的开发中使用这种语言，以证明铸造安全性和正确性属性作为类型的前提。

With increased device miniaturization and commoditization, a new breed of embedded real-time systems, comprising what we designate as Cyber-Physical Infrastructures (CPIs), are increasingly being embedded in physical buildings at home, work, schools, malls, airports, hospitals, etc. By virtue of its utility-like nature, a CPI is likely to cater to the needs of various constituents, supporting any number of applications, some of which may be critical whereas others may be elective or even recreational. Harnessing the power of such CPIs will hinge on a streamlined process whereby relatively unsophisticated programmers are able to rapidly develop and deploy applications without having to understand or worry about the underlying, possibly complex CPI resources and runtime support, while at the same time allowing for the certification of the developed application with respect to safety properties. This project focuses on an integrated approach to the programming and safety verification of CPI applications by recognizing that "types" and "type systems", which have proven to be instrumental in the evolution of modern programming languages, could be used to encapsulate safety properties related to the performance and reliability of CPI applications. To that end, this project aims to develop type systems that are able to support the compositional verification of real-time and QoS properties of CPI applications, the incorporation of these novel type systems into a high-level programming language, and the use of such a language in the development of prototype CPI application to demonstrate the premise of casting safety and correctness properties as types.