The paper addresses the issue of reliability of complex embedded control systems in the safety-critical environment. In this paper, we propose a novel approach to design controller that (i) guarantees the safety of nonlinear physical systems, (ii) enables safe system restart during runtime, and (iii) allows the use of complex, unverified controllers (e.g., neural networks) that drive the physical systems towards complex specifications. We use abstraction-based controller synthesis approach to design a formally verified controller that provides application and system-level fault tolerance along with safety guarantee. Moreover, our approach is implementable using commercial-off-the-shelf (COTS) processing unit. To demonstrate the efficacy of our solution and to verify the safety of the system under various types of faults injected in applications and in the underlying real-time operating system (RTOS), we implemented the proposed controller for the inverted pendulum and three degree-of-freedom (3-DOF) helicopter.
@cite_37: The recently discovered 'W32.Stuxnet' worm has drastically changed the perception that systems managing critical infrastructure are invulnerable to software security attacks. Here we present an architecture that enhances the security of safety-critical cyber-physical systems despite the presence of such malware. Our architecture uses the property that control systems have deterministic real-time) execution behavior to detect an intrusion within 0.6 μs while still guaranteeing the safety of the plant. We also show that even if an attacker is successful (or gains access to the operating system's administrative privileges), the overall state of the physical system still remains safe.
@cite_3: Embedded systems in safety-critical environments demand safety guarantees while providing many useful services that are too complex to formally verify or fully test. Existing application-level fault-tolerance methods, even if formally verified, leave the system vulnerable to errors in the real-time operating system (RTOS), middleware, and microprocessor. We introduce the System-Level Simplex Architecture, which uses hardware software co-design to provide fail-operational guarantees for both logical application-level faults, as well as faults in previously dependent layers including the RTOS and microprocessor. We also provide an end-to-end design process for the System-Level Simplex Architecture where the AADL architecture description is automatically constructed and checked and the VHDL hardware code is generated.To show the efficacy of System-Level Simplex design, we apply the approach to both a classic inverted pendulum and a cardiac pacemaker. We perform fault-injection tests on the inverted pendulum design which demonstrate robustness in spite of software controller and operating system faults. For the pacemaker, we contrast the provided safety guarantees with those of a previous-generation pacemaker.
@cite_17: Unmanned Aerial Vehicles (UAVs) are increasingly demanded in civil, military and research purposes. However, they also possess serious threats to the society because faults in UAVs can lead to physical damage or even loss of life. While increasing their intelligence, for example, adding vision-based sense-and-avoid capability, has a potential to reduce the safety threats, increased software complexity and the need for higher computing performance create additional challenges -- software bugs and transient hardware faults -- that must be addressed to realize intelligent and safe UAV systems. In this paper, we present a fault tolerant system design for UAVs. Our proposal is to use two heterogeneous hardware and software platforms with distinct reliability and performance characteristics: High-Assurance (HA) and High-Performance (HP) platforms. The HA platform focuses on simplicity and verifiability in software and uses a simple and transient fault tolerant processor, while the HP platform focuses on intelligence and functionality in software and uses a complex and highperformance processor. During the normal operation, the HP platform is responsible for controlling the UAV. However, if it fails due to transient hardware faults or software bugs, the HA platform will take over until the HP platform recovers. We have implemented the proposed design on an actual UAV using a low-cost Arduino and a high-performance Tegra TK1 multicore platform. Our case-studies show that our design can improve safety without compromising performance and intelligence of the UAV.
Some Simplex-based designs such as System-Level Simplex @cite_3 , Secure System Simplex Architecture (S3A) @cite_37 , and other variants @cite_17 run the safety controller and the decision logic on an isolated, dedicated hardware unit. By doing so, the trusted components are protected from the faults in the complex subsystem. However, exercising System-Level Simplex design on most COTS multicore platforms SoC (system on chip) is challenging. The majority of commercial multicore platforms is not designed to achieve strong inter-core fault isolation due to the high-degree of hardware resource sharing. For instance, a fault occurring in a core with the highest privilege level may compromise power and clock configurations of the entire platform. To achieve full isolation and independence, one has to utilize two separate boards systems. In contrast, the approach proposed in this paper needs only one processor and tolerates system-level faults.