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

点击翻译按钮获取中文摘要

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.**