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.
