Abstracts

Rance Cleaveland

Back-to-Back, and Back Again: Model-Based Testing of Control Software using Reactis®

Abstract: Current formal methods focus on mathematical proof as a means for establishing that a system is correct with respect to a formal specification. This perspective can limit the applicability of formal methods, since the development of such proofs remains a very difficult task requiring specialized expertise, even with computer assistance. This presentation argues that formal-specification approaches that support both proof and testing as V&V technologies can enhance the practical usefulness of formal methods. It then shows how this observation can be put into practice in the context of model-based testing of automotive control software, in which the so-called back-to-back testing strategy for software is supported using the Reactis® test-generation tool for Simulink® / Stateflow® models of control systems.

Biography: Rance Cleaveland is a Professor of Computer Science at the University of Maryland at College Park; he is currently, since 2018, also serving as Division Director for Computing and Communication Foundations at the National Science Foundation. Prior to joining the UMD faculty in 2005, he held professorships at the State University of New York at Stony Brook and at North Carolina State University (NCSU). He is a co-founder of Reactive Systems, Inc., a company that makes model-based testing tools for embedded software, and a past recipient of National Young Investigator Awards from the National Science Foundation and the Office of Naval Research and the Alcoa Engineering Research Achievement prize from NCSU. He has also won undergraduate teaching awards from UMD and NCSU. He has published over 150 papers in the areas of software verification and validation, formal methods, cyber-physical systems, model checking, software and system specification formalisms, verification tools, and embedded-software testing. Cleaveland received B.S. degrees in Mathematics and Computer Science from Duke University in 1982 and M.S. and Ph.D. degrees from Cornell University in 1985 and 1987, respectively.

Taylor Johnson

Semantic Segmentation Neural Network Verification

Abstract: This presentation will discuss recent work in verifying robustness specifications for neural networks used in semantic segmentation, a typical computer vision task. In image classification, an image is provided as an input, and the output should be a class/category/label representing what appears in the image, for instance finding the class of 1 for a picture of a digit one. Semantic segmentation is a generalization of image classification, where each pixel in the input image is assigned a class, so the output is an image of the same height and width as the input, but over the set of classes instead of color values. For example, in a typical scene observed by cameras on an autonomous vehicle, the input may be an image of a street, and the output is every pixel assigned to a particular class, such as roadway, street sign, pedestrian, sidewalk, vehicle, etc. We will discuss our initial attempts applying formal verification methods to verify robustness specifications of neural networks used for semantic segmentation.

Biography: Taylor Johnson is an Associate Professor of Computer Science at Vanderbilt University. Prof. Johnson's research group, the Verification and Validation for Intelligent and Trustworthy Autonomy Laboratory (VeriVITAL), recently has been focused on verification of autonomous cyber-physical systems (CPS), supported by projects from AFOSR, DARPA, NSF, and ONR.

Chuchu Fan

Building Dependable Autonomous Systems through Learning Certified Decisions and Control

Abstract: The introduction of machine learning (ML) and artificial intelligence (AI) creates unprecedented opportunities for achieving full autonomy. However, learning-based methods in building autonomous systems can be extremely brittle in practice and are not designed to be verifiable. In this talk, I will present our recent progress on the DSTA project where we combine ML with formal methods and control theory to enable the design of provably dependable and safe autonomous systems. I will introduce our techniques to generate safety certificates and certified decision and control for complex autonomous systems, even when the systems have multiple agents, follow nonlinear and nonholonomic dynamics, and need to satisfy high-level specifications.

Biography: Chuchu Fan is the Wilson assistant professor of Aeronautics and Astronautics at MIT. Before joining MIT in 2020, she was a postdoctoral researcher in the Department of Computing and Mathematical Sciences at the California Institute of Technology. She received her Ph.D. in 2019 from the Department of Electrical and Computer Engineering at the University of Illinois at Urbana-Champaign, and her Bachelor's degree from Tsinghua University in 2013. She is currently leading the reliable autonomous system lab (Realm Lab) at MIT. Her group studies how to use rigorous mathematics, including formal methods, machine learning, and control theory for the design, analysis, and verification of safe autonomous systems. She is the recipient of the 2020 ACM Doctoral Dissertation Award.

Susu Xu

Towards a Self-adaptive Smart City: Collaboratively Integrating Sensing, Learning and Actuation for Large-scale Urban Monitoring

Abstract: With increasing populations and demand of high-quality urban services, there is an urgent need of building a “self-adaptive” city which can autonomously adapt its monitoring and management strategies for urban infrastructure systems under constantly changing dynamics. The recent rapid development of sensor networks and 5G technologies are enabling large-scale multi-source data and real-time multi-agent control. But the large-scale and interdependent physical infrastructure systems pose challenges to data-driven monitoring and management strategies. For instances, how to design low-cost paradigms for large-scale and complex infrastructure sensing, how to capture and analyze the physical dynamic interplay between infrastructure systems from the noisy and incomplete data, how to timely react to changes of urban dynamics, and more importantly, how to automate the process of sensing, learning and actuation to improve the quality of the urban services.

In this talk, I will introduce a framework that collaboratively integrates resource-aware sensing, physics-informed learning and incentive mechanisms for large-scale urban monitoring and management. First, I will talk about my works on urban crowdsensing systems. The system utilizes low-cost sensors mounted on individual mobile devices and vehicles to automatically sense spatio-temporal urban information, and learn real-time underlying urban dynamics (e.g., human mobility, air quality, traffic congestion, road deterioration, etc.). Then I will introduce my new theory and algorithm on incentivizing large-scale vehicle mobilities and human activities to timely react to the detected changes in urban systems and maintain a long-term optimal urban monitoring system. I will introduce the first deployed vehicular urban crowdsensing system built on more than 200 taxis in China, which have already run a total mobile mileage of 418,000km and collected half-billion urban data points. Further, I will briefly mention my research on physics-informed learning and distributed learning algorithms development for efficient understanding of large-scale urban systems.

Biography: Dr. Susu Xu is an assistant professor at Department of Civil Engineering, Stony Brook University. She received her Ph.D. in Civil Engineering and Master in Machine Learning from Carnegie Mellon University, her bachelor’s degree from Tsinghua University. She has been postdoctoral research fellow at Stanford University and research scientist at the AI research team in Qualcomm Technologies. Her research focuses on collaboratively integrating crowdsensing, physics-informed machine learning, and incentive mechanisms for enabling self-adaptive smart urban infrastructure systems and improving the efficiency, robustness, and sustainability of urban services. She received the Best Paper Award at the IEEE International Conference of Machine Learning and Applications (ICMLA) in 2018, and the champion of NeurIPS 2018 Adversarial Vision Challenge. She is also the recipient of 2019 MIT CEE Rising Star and Dowd Fellowship.