FRET: A Formal Requirements Elicitation Tool
Requirement formalization and verification tools are essential in designing safety-critical CPS and achieving a level of confidence in system correctness. In this talk, I present the FRET framework for the elicitation, formalization, and understanding of requirements. System requirements are entered in a specialized natural language and can be defined in a hierarchical fashion. FRET helps understanding and review of semantics by utilizing a variety of forms for each requirement: natural language description, formal mathematical logics (based on Metric Temporal Logic), and a graphical notation. Additionally, I present the connection of FRET to modeling environments and compositional verification tools, and demonstrate its application to complex systems.
Anastasia Mavridou is a Computer Scientist in the Robust Software Engineering group at the NASA Ames Research Center. Previously, she worked as a PostDoctoral Researcher at the Institute of Software Integrated Systems at Vanderbilt University. She received her PhD in 2016 from Ecole Polytechnique Federale de Lausanne (EPFL), Switzerland. Her research interests revolve around rigorous system design, formal modeling and analysis of systems with a focus on correct-by-construction techniques.
Joint ECE and CPSRC Seminar:Safety-Critical Control of Dynamic Robotic Systems
Science fiction has long promised a world of robotic possibilities: from humanoid robots in the home, to wearable robotic devices that restore and augment human capabilities, to swarms of autonomous robotic systems forming the backbone of the cities of the future, to robots enabling exploration of the cosmos. With the goal of ultimately achieving these capabilities on robotic systems, this talk will present a unified optimization-based control framework for realizing dynamic behaviors in an efficient, provably correct and safety-critical fashion. The application of these ideas will be demonstrated experimentally on a wide variety of robotic systems, including swarms of rolling and flying robots with guaranteed collision-free behavior, bipedal and humanoid robots capable of achieving dynamic walking and running behaviors that display the hallmarks of natural human locomotion, and robotic assistive devices aimed at restoring mobility. The ideas presented will be framed in the broader context of seeking autonomy on robotic systems with the goal of getting robots into the real-world—a vision centered on combining able robotic bodies with intelligent artificial minds.
Aaron D. Ames is the Bren Professor of Mechanical and Civil Engineering and Control and Dynamical Systems at the California Institute of Technology. He received a B.S. in Mechanical Engineering and a B.A. in Mathematics from the University of St. Thomas in 2001, and he received a M.A. in Mathematics and a Ph.D. in Electrical Engineering and Computer Sciences from UC Berkeley in 2006. Dr. Ames served as a Postdoctoral Scholar in Control and Dynamical Systems at Caltech from 2006 to 2008, and began is faculty career at Texas A&M University in 2008. Prior to joining Caltech, he was an Associate Professor in Mechanical Engineering and Electrical & Computer Engineering at the Georgia Institute of Technology. At UC Berkeley, he was the recipient of the 2005 Leon O. Chua Award for achievement in nonlinear science and the 2006 Bernard Friedman Memorial Prize in Applied Mathematics. Dr. Ames received the NSF CAREER award in 2010, and is the recipient of the 2015 Donald P. Eckman Award recognizing an outstanding young engineer in the field of automatic control. His research interests span the areas of robotics, nonlinear control and hybrid systems, with a special focus on applications to bipedal robotic walking—both formally and through experimental validation. His lab designs, builds and tests novel bipedal robots, humanoids and prostheses with the goal of achieving human-like bipedal robotic locomotion and translating these capabilities to robotic assistive devices. The application of these ideas range from increased autonomy in robots to improving the locomotion capabilities of the mobility impaired.
Internet privacy: Towards more transparency
Internet privacy became a hot topic with the radical growth of Online Social Networks (OSN) and attendant publicity about various leakages. For several years, we examined aggregation of user’s information by a steadily decreasing number of entities as unrelated websites are browsed. I’ll present results from several studies on leakage of personally identifiable information (PII) via Online Social Networks and popular non-OSN sites. Linkage of information gleaned from different sources presents a challenging problem to technologists, privacy advocates, government agencies, and the multibillion dollar online advertising industry. Economics might hold the key in increasing transparency of the largely hidden exchange of data in return for access of so-called free services. I’ll also talk briefly about transient online social Networks.
Balachander Krishnamurthy is a lead inventive scientist at AT&T Labs-Research. His focus of research is in the areas of Internet privacy, transparency, and fairness in ML algorithms, and Internet measurements. He has authored and edited ten books, published over one hundred technical papers, holds seventy five patents, and has given invited talks in thirty five countries.
He co-founded the successful ACM Internet Measurement Conference in 2000 and in 2013 the Conference on Online Social Networks and is involved in the Data Transparency Lab efforts to fund privacy research. He has been on the thesis committee of several PhD students, collaborated with over eighty researchers worldwide, and given tutorials at several industrial sites and conferences.
Decentralized Control of Stochastic Dynamical Cyber-Physical Systems
Many important cyber-physical systems of great current interest are decentralized, consisting of many agents, and uncertainties. Designing decentralized control policies is a challenging task because it involves inducing coordination amongst the controllers without knowing all the states of individual agents. We develop new methods to design decentralized control laws for such systems that perform as well as an optimal centralized policy. Three particular systems that we illustrate these methods on are real-time communication networks, video delivery, and the smart grid. Motivated by real-time networking, we consider multihop stochastic networks serving multiple flows in which packets have hard deadlines. We address the design of packet scheduling, transmit power control, and routing policies that maximize any specified weighted average of the timely throughputs, i.e., the throughput of packets delivered within their deadlines, of the multiple flows. We determine a tractable linear program whose solution yields an optimal routing, scheduling, and power control policy, when nodes have average-power constraints. The optimal policy is fully decentralized, with decisions regarding any packet’s transmission scheduling, transmit power level, and routing, based solely on the age and location of that packet. This resolves a fundamental obstacle that arises whenever one attempts to optimally schedule networks.
Rahul Singh is part of the Deep Learning Group at Intel. He received the B.Tech. degree in Electrical Engineering from Indian Institute of Technology, Kanpur in 2009, the M.S. degree in Electrical Engineering from the University of Notre Dame, in 2011, and the Ph.D. degree in Electrical and Computer Engineering from the Department of Electrical and Computer Engineering, Texas A&M University, College Station, in 2015. He was a Postdoctoral Researcher at the Laboratory for Information and Decision Systems (LIDS), Massachusetts Institute of Technology, and a Data Scientist at Encored, Inc.
Mobile Actuator and Sensor Networks: from CPS to CHS
Robotics will continue to be a hot topic in many years to come in this “big data, cloud computing, machine learning, virtual reality age”. This talk starts by first introducing a new angle for emerging multi-robot control research opportunities - treating robots as a network of moving actuators and/or moving sensors (MAS-net) that can communicate with each other, forming a bigger closed-loop controlled physical system or process, known as CPS (cyber-physical systems). Then I will further discuss the next step towards CHS: cyber-human systems, that extends our horizon of research attacks. I will share my belief that “Cyber-Human Systems” (CHS) will be a hot topic in the next 10-20 years as human (individual, team, society/community), computer (fixed, mobile and surrounds), and environment (physical, mixed and virtual) fuse.
YangQuan Chen earned his Ph.D. from Nanyang Technological University, Singapore, in 1998. He had been a faculty of Electrical Engineering at Utah State University from 2000-12. He joined the School of Engineering, University of California, Merced in summer 2012 teaching “Mechatronics”, “Engineering Service Learning” and “Unmanned Aerial Systems” for undergraduates; “Fractional Order Mechanics”, “Nonlinear Controls” and “Advanced Controls: Optimality and Robustness” for graduates. His research interests include mechatronics for sustainability, cognitive process control, small multi-UAV based cooperative multi-spectral “personal remote sensing”, applied fractional calculus in controls, modeling and complex signal processing; distributed measurement and control of distributed parameter systems with mobile actuator and sensor networks.