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

（CSR--EHS/CPS）利用类型系统开发高保证的网络物理系统和应用程序

• 批准号: 0720604
• 负责人: Azer Bestavros
• 金额: $ 10万
• 依托单位: Trustees of Boston University
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2007
• 资助国家: 美国
• 起止时间: 2007-09-01 至 2011-08-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=0720604&HistoricalAwards=false
• 关键词: CSR; EHS; CPS; Leveraging; Type

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.

随着设备小型化和商品化的不断发展，新型嵌入式实时系统，包括我们所说的网络物理基础设施（CPI），越来越多地嵌入到家庭、工作、学校、商场、机场、医院等实体建筑中。凭借其类似实用程序的性质，CPI 可能会满足不同群体的需求，支持任意数量的应用程序， 其中一些可能是关键的，而另一些可能是选修的，甚至是娱乐性的。利用此类 CPI 的力量将取决于简化的流程，相对简单的程序员能够快速开发和部署应用程序，而无需了解或担心底层的、可能复杂的 CPI 资源和运行时支持，同时允许对开发的应用程序进行安全属性认证。该项目重点关注 CPI 应用程序编程和安全验证的集成方法，通过认识到“类型”和“类型系统”（已被证明在现代编程语言的发展中发挥着重要作用）可用于封装与 CPI 应用程序的性能和可靠性相关的安全属性。为此，该项目旨在开发能够支持CPI应用程序的实时和QoS属性的组合验证的类型系统，将这些新颖的类型系统合并到高级编程语言中，并在原型CPI应用程序的开发中使用这种语言来演示将安全性和正确性属性转换为类型的前提。