Building Automation System (BAS) is a complex distributed control system that is widely deployed in commercial, residential, industrial buildings for monitoring and controlling mechanical/electrical equipment. Through increasing industrial and technological advances, the control components of BAS are becoming increasingly interconnected. Along with potential benefits, integration also introduces new attack vectors, which tremendous increases safety and security risks in the control system. Historically, BAS lacks security design and relies on physical isolation and "security through obscurity". These methods are unacceptable with the "smart building" technologies. The industry needs to reevaluate the safety and security of the current building automation system, and design a comprehensive solution to provide integrity, reliability, and confidentiality on both system and network levels. This dissertation focuses on the system level in the effort to provide a reliable computing foundation for the devices and controllers. Leveraged on the preferred security features such as, robust modular design, small privilege code, and formal verifiability of microkernel architecture, this work describes a security enhanced operating system with built-in mandatory access control and a proxy-based communication framework for building automation controllers. This solution ensures policy-enforced communication and isolation between critical applications and non-critical applications in a potentially hostile cyber environment.

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: The large distributed electric power system is a hierarchical network involving the transportation of power from the sources of power generation via an intermediate densely connected transmission network to a large distribution network of end-users at the lowest level of the hierarchy. At each level of the hierarchy (generation/ trans- mission/ distribution), the system is managed and monitored with a combination of (a) supervisory control and data acquisition (SCADA); and (b) energy management systems (EMSs) that process the collected data and make control and actuation de- cisions using the collected data. However, at all levels of the hierarchy, both SCADA and EMSs are vulnerable to cyber attacks. Furthermore, given the criticality of the electric power infrastructure, cyber attacks can have severe economic and social con- sequences. This thesis focuses on cyber attacks on SCADA and EMS at the transmission level of the electric power system. The goal is to study the consequences of three classes of cyber attacks that can change topology data. These classes include: (i) unobservable state-preserving cyber attacks that only change the topology data; (ii) unobservable state-and-topology cyber-physical attacks that change both states and topology data to enable a coordinated physical and cyber attack; and (iii) topology- targeted man-in-the-middle (MitM) communication attacks that alter topology data shared during inter-EMS communication. Specically, attack class (i) and (ii) focus on the unobservable attacks on single regional EMS while class (iii) focuses on the MitM attacks on communication links between regional EMSs. For each class of attacks, the theoretical attack model and the implementation of attacks are provided, and the worst-case attack and its consequences are exhaustively studied. In particularly, for class (ii), a two-stage optimization problem is introduced to study worst-case attacks that can cause a physical line over ow that is unobservable in the cyber layer. The long-term implication and the system anomalies are demonstrated via simulation. For attack classes (i) and (ii), both mathematical and experimental analyses sug- gest that these unobservable attacks can be limited or even detected with resiliency mechanisms including load monitoring, anomalous re-dispatches checking, and his- torical data comparison. For attack class (iii), countermeasures including anomalous tie-line interchange verication, anomalous re-dispatch alarms, and external contin- gency lists sharing are needed to thwart such attacks. / Dissertation/Thesis / Masters Thesis Electrical Engineering 2015