A cyber-physical system (CPS) is a system featuring a tight combination of, and coordination between, the system’s computational and physical elements. A large-scale CPS usually consists of several subsystems which are formed by networked sensors and actuators, and deployed in different locations. These subsystems interact with the physical world and execute specific monitoring and control functions. How to organize the sensors and actuators inside each subsystem and interconnect these physically separated subsystems together to achieve secure, reliable and real-time communication is a big challenge. In this thesis, we first present a TDMA-based low-power and secure real-time wireless protocol. This protocol can serve as an ideal communication infrastructure for CPS subsystems which require flexible topology control, secure and reliable communication and adjustable real-time service support. We then describe the network management techniques designed for ensuring the reliable routing and real-time services inside the subsystems and data management techniques for maintaining the quality of the sampled data from the physical world. To evaluate these proposed techniques, we built a prototype system and deployed it in different environments for performance measurement. We also present a light-weighted and scalable solution for interconnecting heterogeneous CPS subsystems together through a slim IP adaptation layer and a constrained application protocol layer. This approach makes the underlying connectivity technologies transparent to the application developers thus enables rapid application development and efficient migration among different CPS platforms. At the end of this thesis, we present a semi-autonomous robotic system called cyberphysical avatar. The cyberphysical avatar is built based on our proposed network infrastructure and data management techniques. By integrating recent advance in body-compliant control in robotics, and neuroevolution in machine learning, the cyberphysical avatar can adjust to an unstructured environment and perform physical tasks subject to critical timing constraints while under human supervision. / text

Cyber-Physical Systems (CPS) are systems of collaborating computational elements controlling physical entities via communication. Such systems involve control processes of physical entities and computational processes. The control complexities originated from the physical dynamics and systematic constraints are difficult for traditional control approaches (e.g., PID control) to handle without an exponential increase in design/test etc. costs. Model predictive control (MPC) predicts and produces optimized control inputs based on its predictive model according to a cost function under given constraints. This control scheme has some attractive features for CPSs: it handles constraints systematically, and generates behavior prediction with respective control inputs simultaneously. However, MPC approaches are computationally intensive, and the computation burden generally grows as a predictive model more closely approximates a nonlinear plant (in order to achieve more accurate behavior). The computational burden of predictive methods can be addressed through model reduction at the cost of higher divergence between prediction and actual behavior. This work introduces a metric called uncontrollable divergence, and proposes a mechanism using the metric to select the model to use in the predictive controller (assuming that a set of predictive models are available). The metric reveals the divergence between predicted and true states caused by return time and model mismatch. More precisely, a map of uncontrollable divergence plotted over the state space gives the criterion to judge where a specific model can outperform others. With this metric and the mechanism, this work designs a controller that switches at runtime among a set of predictive controllers in which respective models are deployed. The resulting controller is a hybrid predictive controller. In addition to design and runtime tools, this work also studies stability conditions for hybrid model predictive controllers in two approaches. One is average dwell time based, and it does not rely on the offline computation that studies the system properties. The other one uses a reference Lyapunov function instead of multiple Lyapunov functions derived from multiple predictive controllers. This approach implicitly depends on the offline numerical solutions of certain systematic properties. The term "boundedness" is preferable in this context since it accepts numerical error and approximations. Two examples, vertical takeoff and landing aerial vehicle control and ground vehicle control, are used to demonstrate the approach of hybrid MPC.

Cyber-Physical Systems (CPSs) are defined as the combination of computational elements with physical components. Systems that require communication, computation, and control are by definition CPSs. The complexity of these systems often grows exponentially as they incorporate more elements into their design. As such, many approaches to designing CPSs revolve around the development of Domain Specific Modeling Languages (DSMLs). DSMLs drastically reduce the development time for CPSs by abstracting elements of the development process to a high level. DSMLs can be constrained in such a way that it is impossible to construct structurally invalid models of CPSs. This allows designers to think abstractly and ignore time consuming low level implementation details. However, these methods do not prevent designers from constructing systems that can be invalid in other, more dynamic, ways. That is, structural constraints on a DSML for a CPS do not prevent constraint violations where some analysis must be performed on the system to verify that the constraint has been satisfied. In the state-of-the-art, it is violations on these dynamic constraints that modelers must spend their time designing around. Dynamic constraints can be incorporated into the framework of a DSML by integrating the concepts of automatic feedback control into the DSML with model transformations. The methodology that describes this new approach to Domain Specific Modeling (DSM) is called Dynamic Constraint Feedback (DCF). At a glance: first a DSML is created for a CPS. Next, an interface is developed for two-way interaction between the DSML and external tools. Third, an expert block that can perform analysis on the models is created. The expert block is responsible for determining constraint violations and solutions. Lastly, model transformations are generated based on expert block output and applied to the existing models. This process repeats until a solution is either found or declared to be unreachable.

CPS (Cyber-Physical Systems) enable a new class of applications that perceive their surroundings using raw data from sensors, monitor the timing of dynamic processes, and control the physical environment. Since failures and misbehaviors in application domains such as cars, medical devices, nuclear power plants, etc., may cause significant damage to life and/or property, CPS need to be safe and dependable. A conventional way of improving dependability is to use redundant hardware to replicate the whole (sub)system. Although hardware replication has been widely deployed in conventional mission-critical systems, it is cost-prohibitive to many emerging CPS application domains. Hardware replication also leads to limited system flexibility. This dissertation studies the problem of making CPS affordably dependable and develops a system-level framework that manages critical CPS resources including processors, networks, and sensors. Our framework called SAFER (System-level Architecture for Failure Evasion in Real-time applications) incorporates configurable software mechanisms and policies to tolerate failures of critical CPS resources while meeting their timing constraints. It supports adaptive graceful degradation, the effective use of different sensor modalities, and the fault-tolerant schemes of hot standby, cold standby, and re-execution. SAFER reliably and efficiently allocates tasks and their backups to CPU and sensor resources while satisfying network traffic constraints. It also fuses and (re)configures sensor data used by tasks to recover from system failures. The SAFER framework aims to guarantee the timeliness of different types of tasks that fall into one of four categories: (1) tasks with periodic arrivals, (2) tasks with continually varying periods, (3) tasks with parallel threads, and (4) tasks with self-suspensions. We offer the schedulability analyses and runtime support for such tasks with and without resource failures. Finally, the functionality of the proposed system is evaluated on a self-driving car using SAFER. We conclude that the proposed framework analytically satisfies timing constraints and predictably operates systems with and without resource failures, hence making CPS dependable and timely.

A Cyber-Physical System (CPS) has a tight integration of computation, networking and physicalprocess. It is a heterogeneous system that combines multi-domain consisting of both hardware andsoftware systems. Cyber subsystems in the CPS implement the control strategy that affects the physicalprocess. Therefore, software systems in the CPS are more complex. Visualization of a complex system provides a method of understanding complex systems byaccumulating, grouping, and displaying components of systems in such a manner that they may beunderstood more efficiently just by viewing the model rather than understanding the code. Graphicalrepresentation of complex systems provides an intuitive and comprehensive way to understand thesystem. OpenModelica is the open source development environment based on Modelica modeling andsimulation language that consists of several interconnected subsystems. OMEdit is one of the subsystemintegrated into OpenModelica. It is a graphical user interface for graphical modeling. It consists of toolsthat allow the user to create their own shapes and icons for the model. This thesis presents a methodology that provides an easy way of understanding the structure andexecution of programs written in the imperative language like C through graphical Modelica model.

Existing Building Automation Systems (BASs) and Building Automation Networks (BANs) have been shown to have serious cybersecurity problems. Due to the safety-critical and interconnected nature of building subsystems, local and network access control needs to be finer grained, taking into consideration the varying criticality of applications running on heterogeneous devices. In this paper, we present a secure communication framework for BASs that 1) enforces rich access control policy for operating system services and objects, leveraging a microkernel-based architecture; 2) supports fine-grained network access control on a per-process basis; 3) unifies the security control of inter-device and intra-device communication using proxy processes; 4) tunnels legacy insecure communication protocols (e.g., BACnet) through a secure channel, such as SSL, in a manner transparent to legacy applications. We implemented the framework on seL4, a formally verified microkernel. We conducted extensive experiments and analysis to compare the performance and effectiveness of our communication systems against a traditional Linux-based implementation of the same control scenario. Our experiments show that the communication performance of our system is faster or comparable to the Linux-based architecture in embedded systems.

Smart Cyber-Physical Systems (sCPS) are complex systems performing smart coordination that often require decentralized and network resilient operation. New development in the fields of the robotic systems, Industry 4.0 and autonomous vehicular system brings challenges that can be tackled with deployment of ensemble based sCPS, but require further refinement in terms of network resilience and data propagation. This thesis maps the use cases of the sCPS in the aforementioned domains, discusses requirements on the ensemble based architecture in terms of network properties, and proposes recommendations and technical means that help to design network aware ensemble based sCPS. The proposed solutions are evaluated by the means of target systems simulation using state of the art realistic network and vehicular simulators.

abstract: In this dissertation, two problems are addressed in the verification and control of Cyber-Physical Systems (CPS): 1) Falsification: given a CPS, and a property of interest that the CPS must satisfy under all allowed operating conditions, does the CPS violate, i.e. falsify, the property? 2) Conformance testing: given a model of a CPS, and an implementation of that CPS on an embedded platform, how can we characterize the properties satisfied by the implementation, given the properties satisfied by the model? Both problems arise in the context of Model-Based Design (MBD) of CPS: in MBD, the designers start from a set of formal requirements that the system-to-be-designed must satisfy. A first model of the system is created. Because it may not be possible to formally verify the CPS model against the requirements, falsification tries to verify whether the model satisfies the requirements by searching for behavior that violates them. In the first part of this dissertation, I present improved methods for finding falsifying behaviors of CPS when properties are expressed in Metric Temporal Logic (MTL). These methods leverage the notion of robust semantics of MTL formulae: if a falsifier exists, it is in the neighborhood of local minimizers of the robustness function. The proposed algorithms compute descent directions of the robustness function in the space of initial conditions and input signals, and provably converge to local minima of the robustness function. The initial model of the CPS is then iteratively refined by modeling previously ignored phenomena, adding more functionality, etc., with each refinement resulting in a new model. Many of the refinements in the MBD process described above do not provide an a priori guaranteed relation between the successive models. Thus, the second problem above arises: how to quantify the distance between two successive models M_n and M_{n+1}? If M_n has been verified to satisfy the specification, can it be guaranteed that M_{n+1} also satisfies the same, or some closely related, specification? This dissertation answers both questions for a general class of CPS, and properties expressed in MTL. / Dissertation/Thesis / Doctoral Dissertation Electrical Engineering 2015

abstract: Testing and Verification of Cyber-Physical Systems (CPS) is a challenging problem. The challenge arises as a result of the complex interactions between the components of these systems: the digital control, and the physical environment. Furthermore, the software complexity that governs the high-level control logic in these systems is increasing day by day. As a result, in recent years, both the academic community and the industry have been heavily invested in developing tools and methodologies for the development of safety-critical systems. One scalable approach in testing and verification of these systems is through guided system simulation using stochastic optimization techniques. The goal of the stochastic optimizer is to find system behavior that does not meet the intended specifications. In this dissertation, three methods that facilitate the testing and verification process for CPS are presented: 1. A graphical formalism and tool which enables the elicitation of formal requirements. To evaluate the performance of the tool, a usability study is conducted. 2. A parameter mining method to infer, analyze, and visually represent falsifying ranges for parametrized system specifications. 3. A notion of conformance between a CPS model and implementation along with a testing framework. The methods are evaluated over high-fidelity case studies from the industry. / Dissertation/Thesis / Doctoral Dissertation Computer Science 2017

abstract: Critical infrastructures in healthcare, power systems, and web services, incorporate cyber-physical systems (CPSes), where the software controlled computing systems interact with the physical environment through actuation and monitoring. Ensuring software safety in CPSes, to avoid hazards to property and human life as a result of un-controlled interactions, is essential and challenging. The principal hurdle in this regard is the characterization of the context driven interactions between software and the physical environment (cyber-physical interactions), which introduce multi-dimensional dynamics in space and time, complex non-linearities, and non-trivial aggregation of interaction in case of networked operations. Traditionally, CPS software is tested for safety either through experimental trials, which can be expensive, incomprehensive, and hazardous, or through static analysis of code, which ignore the cyber-physical interactions. This thesis considers model based engineering, a paradigm widely used in different disciplines of engineering, for safety verification of CPS software and contributes to three fundamental phases: a) modeling, building abstractions or models that characterize cyberphysical interactions in a mathematical framework, b) analysis, reasoning about safety based on properties of the model, and c) synthesis, implementing models on standard testbeds for performing preliminary experimental trials. In this regard, CPS modeling techniques are proposed that can accurately capture the context driven spatio-temporal aggregate cyber-physical interactions. Different levels of abstractions are considered, which result in high level architectural models, or more detailed formal behavioral models of CPSes. The outcomes include, a well defined architectural specification framework called CPS-DAS and a novel spatio-temporal formal model called Spatio-Temporal Hybrid Automata (STHA) for CPSes. Model analysis techniques are proposed for the CPS models, which can simulate the effects of dynamic context changes on non-linear spatio-temporal cyberphysical interactions, and characterize aggregate effects. The outcomes include tractable algorithms for simulation analysis and for theoretically proving safety properties of CPS software. Lastly a software synthesis technique is proposed that can automatically convert high level architectural models of CPSes in the healthcare domain into implementations in high level programming languages. The outcome is a tool called Health-Dev that can synthesize software implementations of CPS models in healthcare for experimental verification of safety properties. / Dissertation/Thesis / Ph.D. Computer Science 2012