Deep reinforcement learning (DRL) methods can solve complex continuous control tasks in simulated environments by taking actions based solely on state observations at each decision point. Because of the dynamics involved, individual snapshots of real-world sensor measurements afford only partial state observability, so it is typical to use a history of observations to improve training and policy performance. Such intertemporal information can be further exploited using a recurrent neural network (RNN) to reduce the dimensionality of the dynamic state representation. However, using RNNs as an internal part of a DRL network presents challenges of its own; and even then, the improvements in resulting policies are usually limited. To address these shortcomings, we propose using gated feature extraction to improve DRL training of real-world robots. Specifically, we use an untrained gated recurrent unit (GRU) to encode a low-dimension representation of the state observation sequence before passing it to the DRL training procedure. In addition to dimensionality reduction, this allows us to unroll the RNN by encoding the observations cumulatively as they are collected, thereby avoiding same-length input requirements, and train the RL network on the raw observations at the current step combined with the GRU-encoding of the preceding steps. Our simulation experiments employ gated feature extraction with the TD3 algorithm. Our results show that the GRU-encoded state observations improve the training speed and execution performance of the TD3 algorithm, improving the learned policies in all 19 test cases, exceeding the maximum achieved reward by over 38% in 8 and doubling the maximum achieved reward in three, while also outperforming a baseline implementation of SAC in 17 out of 19 environments. Moreover, the greatest improvement is seen in real-world experiments, where our approach successfully learns to balance a pendulum as well as a complex quadrupedal locomotion task. In contrast, the standard TD3 algorithm not only does not show any learning progress at all, but also repeatedly damages the hardware.

Deep Reinforcement Learning (DRL) faces challenges bridging the sim-to-real gap to enable real-world applications. In contrast to the simulated environments used in conventional DRL training, real-world systems are non-linear and evolve in an asynchronous fashion; sensors and actuators have limited precision; communication channels are noisy; and many components introduce variable delays. While these issues are known to many researchers, published methods for systematically tackling the problem of DRL training under these conditions without using simulation are sparse in the field. To this end, this paper proposes a non-blocking and asynchronous DRL training architecture for non-linear, real-time dynamical systems tailored to handling variable delays. Compared to conventional DRL training, we: (i) decouple the RL loop into separate processes run independently at their own frequencies, (ii) further decouple collection of transition tuples$(s_{t}, at_{t}, s_{t+1})$via asynchronous and independent streaming of both actions and observations, and (iii) mitigate the effects of delays and increase sample efficiency by providing delay-length measurements to the training loop and regular retraining of the DRL network. This allows the action step time to be tuned to find an optimal control frequency for a given system, and handles streamed observations that arrive with random delays and independently of action timing. We demonstrate the efficacy of this architecture with a physical implementations of a commodity-grade swing-up pendulum and a quadrupedal robot. Our architecture achieves the best results balancing the pendulum for almost entire length of the episode, compared to conventional blocking approaches which fail to learn effective policies. Our results show that these techniques scale to more complex tasks such as quadrupedal locomotion.

We present an approach to verifying the codesign of software and hardware. Our approach verifies that a reference design, perhaps a straightforward software implementation, is equivalent to a design combining software and reconfigurable hardware, possibly using runtime reconfiguration. Our approach combines symbolic simulation with equivalence checking to compare symbolic output expressions. Whilst our implementation uses C-style software and streaming hardware based on Maxeler designs, our approach is modular and could generalize to other software or hardware inputs. We evaluate our approach by applying it to several kernels, including one used for geoengineering.

PCI Express is a modern, high-performance communication protocol implementing sophisticated features to meet today's performance demands. Although an off-chip protocol, PCI Express implements many principles of future on-chip communication architectures. It is a highly complex protocol that is hard to verify formally. We present the application of a new approach to the PCI Express transaction and data link layers. The methodology is based on a series of model transformation steps and revises the traditional modeling and verification workflow for designing on-chip protocols. Major parts of PCI Express, including performance-related optimizations and fault-tolerance features, are modeled incrementally to control the complexity and composed to a single model. The work has been accomplished in the Isabelle/HOL theorem prover. By restricting the models to an executable subset of the specification language, we have been able to combine the advantages of specifying in a theorem prover with the advantages of executable models in a functional programming language.

PCI Express is a modern, high-performance communication protocol implementing highly sophisticated features to meet today's performance demands. Although an off-chip protocol, PCI Express implements many principles of future on-chip communication architectures. It is a highly complex protocol which is naturally hard to verify formally. We recently proposed a new methodology, based on a series of model transformation steps, to revise the traditional modelling and verification workflow for designing on-chip protocols. We present the application of the new approach to the PCI Express transaction layer. The work has been accomplished in the Isabelle/HOL theorem prover. By restricting the models to an executable subset of the specification language, we have been able to combine the advantages of specifying in a theorem prover with the advantages of executable models in a functional programming language.

Modern computer systems rely more and more on on-chip communication protocols to exchange data. To meet performance requirements these protocols have become highly complex, which usually makes their formal verification infeasible with reasonable time and effort. We present a new refinement approach to on-chip communication protocols that combines design and verification together, interleaving them hand-in-hand. Our modeling framework consists of design steps and design transformations formalized as finite state machines. Given a verified design step, transformations are used to extend the system with advanced features. A design transformation ensures that the extended design is correct if the previous system is correct. This approach is illustrated by an arbiter-based master-slave communication system inspired by the AMBA high-performance bus architecture. Starting with a sequential protocol design, it is extended with pipelining and burst transfers. Transformations are generated from design constraints providing a basis for correctness-by-design of the derived system.

We formalize the correctness of a fault-tolerant scheduler in a time-triggered architecture. Where previous research elaborated on real-time protocol correctness, we extend this work to gate-level hardware. This requires a sophisticated analysis of analog bit-level synchronization and transmission. Our case-study is a concrete automotive bus controller (ABC), inspired by the FlexRay standard. For a set of interconnected ABCs, vulnerable to sudden failure, we prove at gate-level, that all operating ABCs are synchronized tightly enough such that messages are broadcast correctly. This includes formal arguments for startup, failures, and reintegration of nodes at arbitrary times. To the best of our knowledge, this is the first effort tackling fault-tolerant scheduling correctness at gate-level.

The mission of the Verisoft project is (i) to develop techniques, which permit the pervasive formal verification of computer systems comprising hardware, system software, communication systems, and applications, (ii) to apply these techniques in an industrial context to verify prototypical systems. One such application is an emergency call, which is automatically placed on the mobile phone net after the sensors of a car have detected that it was involved in a crash. The application runs on a system of several electronic control units (ECUs). The local application programs of the ECUs run on top of a simple real time operating system kernel like described in the OSEKTime standard. ECUs are connected via a FlexRay bus. We outline the structure of an overall correctness proof for such a parallel system from the gate to the kernel level for the communication system hardware one has to combine existing correctness proofs for components of time triggered architectures (e.g. clock synchronization) and arguments about hardware correctness into a single theorem. Results on processor, driver, and kernel correctness can to a large extent be imported from existing research in the Verisoft project. worst case execution time bounds are derived with advanced industrial tools based on abstract interpretation.