Cyber-Physical Systems - Formal Modeling, Design, and Verification

动机 * 在我们的日常生活中，我们会遇到嵌入在我们使用的设备（如智能手机和汽车）中的无形计算机。这些计算机被称为嵌入式系统。人们已经认识到，为了更好地为社会服务，有必要将这种模式提升到更高的水平，其中嵌入式计算机网络可以通过反馈回路控制物理过程。Cyber-Physical Systems（CPS）就是指这样的系统。CPS的应用领域包括医疗保健、交通运输和关键基础设施管理。因为它们无处不在的性质影响着我们体验生活的方式，CPS必须被构建成可预测和可靠的。* 长期目标 * 物理定律，固有地包括连续时间和并发性，支配着真实的世界，而不是当前计算平台中的传统离散顺序计算。有必要创建一个统一的理论来处理异质性，不确定性，上下文控制和适应，同时保持人在回路中。为了实现和验证的目的，需要一个忠于理论的新计算模型。科学方法 * 该研究探索了一种整体方法，用于在不确定的环境中建立可预测的CPS。*1。不确定性可能由执行器、传感器、人类行为和损坏的通信介质引入，必须降低到可容忍的水平。时间的不确定性，这是当网络世界的离散时间满足物理世界的连续时间，必须加以克服。必须建立物理-网络实体的模型，描述它们的异质性特征及其在不确定性中的相互作用。2.一个基于组件的CPS的正式层次架构的设想驯服异构性和本地化的不确定性传播的设计。一个正式定义的组件类型将有接口类型来规范依赖于上下文的可靠交互。不同的相互作用类型，建议由真实的CPS的例子，将研究细化和丰富的接口类型。*3。一个上下文感知的标签转换系统，将被定义，将作为计算模型（MoC）的CPS组件和子系统。组合方法将受到组件接口处的契约类型和上下文情况的满足的约束。*工作的意义 * 世界各地的许多研究小组都积极参与CPS研究。我相信，我的建议结合联合收割机的两个关键问题的不确定性和异构性与上下文感知CPS建模和设计是新的。这种新方法将对研究界产生有意义的影响，并导致知识向工业转移。特别是，我打算从卫生保健和交通领域中选择案例研究，这将是对加拿大的重大贡献。

MOTIVATION***In our everyday living experience we come across invisible computers that are embedded in devices that we use, such as smart phones and automobiles. These computers are called embedded systems. It has been recognized that to serve the society better it is necessary to lift this paradigm to a higher level, where a network of embedded computers may control physical processes with feedback loops. The term Cyber-Physical Systems (CPS) refers to such systems. Application domains of CPS include healthcare, transportation, and critical infrastructure management. Because their ubiquitous nature affects the way we experience life, CPS must be built to be predictable and dependable. ***LONG TERM OBJECTIVE***Laws of physics, that inherently include continuous time and concurrency, govern the real world, as opposed to the traditional discrete sequential computing in the current computing platforms. It is necessary to create a unified theory to deal with heterogeneity, uncertainty, contextual control and adaptation while keeping human-in-the-loop. A new model of computation that is faithful to the theory is needed, both for implementation and verification purposes.***SCIENTIFIC APPROACH***The research explores a holistic approach for building a predictable CPS operating in uncertain contexts. ***1. Uncertainty, which may be introduced by actuators, sensors, human behaviors, and corrupted communication mediums, must be reduced to a level where it is tolerated. Temporal uncertainty, which arises when the discrete time of the cyber world meets the continuous time of the physical world, must be overcome. Models of physical-cyber entities which portray their heterogeneous characteristics and their interactions amidst uncertainties must be built.***2. A component-based formal hierarchical architecture for CPS is envisaged for taming heterogeneity and localizing uncertainty propagation in the design. A formally defined component type will have interface types to regulate dependable context-dependent interactions. Different interaction types, as suggested by real CPS examples, will be studied to refine and enrich interface types. ***3. A Context-aware Labeled Transition System, to be defined, will serve as the Model of Computation (MoC) for CPS components and subsystems. Composition methods will be constrained by contract types at component interfaces and satisfaction of contextual situations.***SIGNIFICANCE OF THE WORK***Many research groups across the world are active in CPS research. I believe that my proposal to combine the two key issues uncertainty and heterogeneity with context-awareness in CPS modeling and design is new. This new approach will have a meaningful impact on the research community, and lead to transfer of knowledge to industry. In particular, my intended work on the case studies, selected from Health Care and Transportation domains, will be a significant contribution to Canada.**