Programming Abstractions for Data Stream Processing Systems
Rajeev Alur, University of Pennsylvania
Abstract: Decision making in emerging IoT systems often requires dynamic monitoring of a data stream to compute performance-related quantitative properties. We propose StreamQRE as a high-level declarative language for modular specifications of such policies. This language is rooted in the emerging theory of regular functions, and every policy described in this language can be compiled into a space-efficient streaming implementation. We describe a prototype system that is integrated within an SDN controller and show how it can be used to specify and enforce dynamic updates for traffic engineering. As another case study, we will discuss the application of StreamQRE to the design space exploration of alternative algorithms for cardiac arrhythmia detection. Finally, as a first step towards a rigorous programming methodology for distributed stream processing systems, we propose the model of data-trace transductions that generalizes both Kahn process networks and relational query processors and can specify computations over data streams with a rich variety of ordering and synchronization characteristics.
Finding Software Bugs Using Active Automata Learning
Frits Vaandrager, Radboud University, Netherlands
Abstract: Active automata learning is emerging as an effective technique for obtaining state machine models of software and hardware systems. In this lecture, I will present an overview of work at Radboud University in which we used automata learning to find standard violations and security vulnerabilities in implementations of network protocols such as TCP, TLS, and SSH. Also, I will discuss the application of automata learning to support refactoring of legacy embedded control software, and the theoretical challenges that we face to further scale the application of automata learning techniques.
The Future of Runtime Verification for Cyber-Physical Systems Development
Jim Kapinski, Toyota Motor North America (TMNA)
Abstract: Cyber-physical systems (CPS) are used in mission-critical applications, like automobiles, aircraft, and service robots, and the complexity and cost to develop these applications is growing sharply. Runtime verification (RV) technologies include powerful methods to automate critical aspects of the monitoring and testing activities performed throughout the development process, but these tools have been slow to gain traction in industry. This talk presents experiences in applying RV technologies to CPS development in an industrial setting and describes recent advancements, which include new tools to support the requirements engineering process and automated monitoring tools that capture system interfaces. The talk will also suggest directions for future research and predict future development processes that leverage RV technologies to create complex, reliable systems in a cost-efficient manner.