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

动机***在我们的日常生活经验中，我们会遇到嵌入在我们使用的设备（如智能手机和汽车）中的隐形计算机。这些计算机被称为嵌入式系统。人们已经认识到，为了更好地为社会服务，有必要将这种范式提升到一个更高的水平，在这个水平上，嵌入式计算机网络可以用反馈回路控制物理过程。术语信息物理系统（CPS）指的是这样的系统。CPS的应用领域包括医疗保健、运输和关键基础设施管理。因为它们无处不在的特性影响着我们体验生活的方式，所以CPS必须是可预测和可靠的。***长期目标***物理定律，固有地包括连续时间和并发性，支配着现实世界，而不是当前计算平台中传统的离散顺序计算。有必要建立一个统一的理论来处理异质性、不确定性、语境控制和适应，同时保持人类在循环中。为了实现和验证的目的，需要一种忠实于理论的新的计算模型。***科学方法***本研究探索了在不确定环境下建立可预测的CPS的整体方法。* * * 1。不确定性可能由执行器、传感器、人类行为和损坏的通信媒介引入，必须降低到可以容忍的水平。当网络世界的离散时间与物理世界的连续时间相遇时产生的时间不确定性必须克服。必须建立物理-网络实体的模型，以描述它们的异质特征和它们在不确定性中的相互作用。设想了一种基于组件的正式分层体系结构，用于驯服设计中的异构性和本地化不确定性传播。正式定义的组件类型将具有接口类型，以规范可靠的依赖于上下文的交互。根据实际的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.**