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

动机 在我们的日常生活经验中，我们遇到了嵌入到我们使用的设备中的隐形计算机，如智能手机和汽车。这些计算机被称为嵌入式系统。人们已经认识到，为了更好地服务于社会，有必要将这一范例提升到更高的水平，其中嵌入式计算机网络可以通过反馈回路来控制物理过程。术语网络物理系统(CPS)指的是这样的系统。CPS的应用领域包括医疗保健、交通运输和关键基础设施管理。因为它们无处不在的性质影响着我们体验生活的方式，所以CP必须被构建为可预测和可靠的。 长期目标 物理定律本质上包括连续时间和并发，它支配着现实世界，而不是当前计算平台中的传统离散顺序计算。有必要建立一个统一的理论来处理异质性、不确定性、语境控制和适应，同时保持人在循环中。无论是出于实施还是验证的目的，都需要一个忠于理论的新的计算模型。 科学方法 这项研究探索了一种在不确定环境下建立可预测的CPS的整体方法。 1.执行器、传感器、人类行为和被破坏的通信媒介可能带来的不确定性，必须降低到可以容忍的水平。当网络世界的离散时间与物理世界的连续时间相遇时，产生的时间不确定性必须被克服。必须建立物理-网络实体的模型，描述它们的异质特征以及它们在不确定因素中的相互作用。 2.提出了一种基于组件的CPS形式化层次体系结构，用于抑制设计中的异构性和局部化不确定性传播。正式定义的组件类型将具有用于规范可靠的上下文相关交互的接口类型。根据实际CPS实例的建议，将研究不同的交互类型，以提炼和丰富界面类型。 3.待定义的上下文感知标签转换系统将作为CPS组件和子系统的计算模型(MOC)。组合方法将受到组件接口上的约定类型和上下文情况的满足程度的约束。 这部作品的意义 世界各地的许多研究小组都活跃在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.