seminar

Design of Robotics and Embedded systems, Analysis, and Modeling Seminar (DREAMS)

Spring 2014

The Design of Robotics and Embedded systems, Analysis, and Modeling Seminar (DREAMS) occurs weekly on Tuesdays from 4.10-5.00 p.m. in 531 Cory Hall (Wang Room).

The Design of Robotics and Embedded systems, Analysis, and Modeling Seminar topics are announced to the DREAMS list, which includes the chessworkshop workgroup, which includes the chesslocal workgroup.

Information on the seminar series might be useful for potential speakers. If you have any questions about DREAMS, please contact Armin Wasicek. If you want to subscribe to our mailing list, please drop me a line.

Seminars from previous semesters can be found here.

Upcoming Seminar Talk

Schedule

Michel Maharbiz September 09, 2014
Sanjit Seshia September 30, 2014
Arne Hamann October 07, 2014
Ashutosh Saxena October 07, 2014
Yi-Chin Wu October 21, 2014
Dave Parker October 28, 2014
Martin Torngren November 04, 2014
Philip Koopman November 14, 2014
Klaus Doppler December 02, 2014 UPCOMING

Neural Dust and Neural Interfaces

Sep 09, 2014, 4.10-5pm, Michel Maharbiz, UC Berkeley.

Slides

Abstract

A major technological hurdle in neuroprosthetics is the lack of an implantable neural interface system that remains viable for a lifetime. I will discuss the basics of extracellular neural recording, discuss the state of the art in cortical neural recording and introduce Neural Dust, a concept developed with Elad Alon, Jose Carmena and Jan Rabaey, which aims to develop a tetherless method to remotely record action potentials from the mammalian cortex.

Bio:

Michel M. Maharbiz is an Associate Professor with the Department of Electrical Engineering and Computer Science at the University of California, Berkeley.

He received his Ph.D. from the University of California at Berkeley under Professor Roger T. Howe (EECS) and Professor Jay D. Keasling (ChemE); his work led to the foundation of Microreactor Technologies, Inc. which was acquired in 2009 by Pall Corporation. From 2003 to 2007, Michel Maharbiz was an Assistant Professor at the University of Michigan, Ann Arbor. He is the co-founder of Tweedle Technologies, Cortera Neurotech and served as vice-president for product development at Quswami, Inc. from July 2010 to June 2011.

Prof. Maharbiz is a Bakar Fellow and was the recipient of a 2009 NSF Career Award for research into developing microfabricated interfaces for synthetic biology. His group is also known for developing the world’s first remotely radio-controlled cyborg beetles. This was named one of the top ten emerging technologies of 2009 by MIT’s Technology Review (TR10) and was in Time Magazine’s Top 50 Inventions of 2009. Dr. Maharbiz has been a GE Scholar and an Intel IMAP Fellow. Professor Maharbiz’s current research interests include building micro/nano interfaces to cells and organisms and exploring bio-derived fabrication methods. Michel’s long term goal is understanding developmental mechanisms as a way to engineer and fabricate machines.


Formal Methods for Lab-Based MOOCs: Cyber-Physical Systems and Beyond

Sep 30, 2014, 4.10-5pm, Sanjit Seshia, UC Berkeley.

Slides

Abstract

The advent of massive open online courses (MOOCs) has placed a renewed focus on the development and use of computational aids for teaching and learning.
Lab-based courses, such as those in embedded systems and robotics, are particularly challenging. In this talk, I will describe our experience in designing a MOOC version of the introductory undergraduate course on embedded systems at UC Berkeley. A key component of this MOOC was the "virtual laboratory", where students perform lab exercises using custom designed virtual lab software with built-in automatic grading and feedback based on formal methods. I will describe the design and evaluation of CPSGrader, the auto-grading system, summarize results from the MOOC offering on edX, and sketch directions for future work.

This talk describes joint work with several collaborators including Alexandre Donze, Jeff Jensen, Garvit Juniwal, and Edward Lee.

Bio:

Sanjit A. Seshia is an Associate Professor in the Department of Electrical Engineering and Computer Sciences at the University of California, Berkeley. He received an M.S. and Ph.D. in Computer Science from Carnegie Mellon University, and a B.Tech. in Computer Science and Engineering from the Indian Institute of Technology, Bombay. His research interests are in dependable computing and computational logic, with a current focus on applying automated formal methods to problems in embedded systems, electronic design automation, computer security, and program analysis. His Ph.D. thesis work on the UCLID verifier and decision procedure helped pioneer the area of satisfiability modulo theories (SMT) and SMT-based verification. He is co-author of a widely-used textbook on embedded systems. His awards and honors include a Presidential Early Career Award for Scientists and Engineers (PECASE) from the White House, an Alfred P. Sloan Research Fellowship, and the School of Computer Science Distinguished Dissertation Award at Carnegie Mellon University.


Formal analysis of timing effects on closed-loop properties of cyber physical systems

Oct 07, 2014, 3.10-4pm, Arne Hamann, Robert Bosch GmbH, Stuttgart, Germany.

Slides

ROOM: 400 Hughes room

Abstract

The underlying theories of, both, control engineering and real-time systems engineering, assume idealized system abstractions that mutually neglect central aspects of the other discipline. Control engineering theory usually assumes jitter free sampling and insignificant (constant) input-output latencies disregarding complex real-world timing effects. Real-time systems theory, on the other hand, uses abstract performance models that neglect the functional behavior, and derives worst-case situations that have little expressiveness for control functionalities in physically dominated automotive systems. However, there is a lot to gain from a systematic co-engineering between both disciplines, increasing design efficiency and confidence.

In this talk an approach is presented that integrates state-of-the-art timing models into functional analysis. A general system model is presented and integrated into closed-loop reachability analysis using the hybrid system state space explorer SpaceEx. This enables a systematic co-engineering between both disciplines, increasing design efficiency and confidence. The approach is demonstrated based on an industrial example, the control software of an electro-mechanical braking system.

Bio:

Arne Hamann obtained his PhD in Computer Science in 2008 from the Technical University of Braunschweig, Germany. His PhD thesis was awarded the EDAA Outstanding Dissertation Award 2009 in the category “New directions in embedded system design and embedded software”. Currently, Arne Hamann is working for Bosch Corporate Research in the division of “Software-intensive Systems”. There, he acts as expert for real-time system design principles for physically dominated embedded systems. Additionally, he is in charge of an internal research project introducing novel model-centric system design methods into various business units within the Bosch Group. Arne Hamann is part of the AUTOSAR Timing Extensions Subgroup as well as the AUTOSAR Timing User Group. Additionally, he represents Bosch in the European ROS Industrial Consortium (RIC-EU). In the academic context, he currently serves as industrial advisory board member of the European COST action TACLe (Timing Analysis on Code Level) and program committee member of the EMSOFT and ECRTS conferences.


The Robo Brain Project: Learning Models for Perception, Planning and Language

Oct 07, 2014, 4.10-5pm, Ashutosh Saxena, Cornell University.

Slides

ROOM Change: 540AB DOP Center room!

Abstract

In this talk, I will present learning algorithms that start learning from large-scale unsupervised datasets, and through different forms of human feedback learn about concepts such as object affordances and basic physics. These representations and concepts are stored as a large graph in the robot brain. Through a few examples, I will show that such models are very effective in performing a variety of tasks including 3D scene labeling, human activity detection and anticipation, grasping, path planning, robot language, and so on.

Bio:

Ashutosh Saxena is an assistant professor in the Computer Science department at Cornell University. His research interests include machine learning, robotics and computer vision. He received his MS in 2006 and Ph.D. in 2009 from Stanford University, and his B.Tech. in 2004 from Indian Institute of Technology (IIT) Kanpur. He has also won best paper awards in 3DRR, RSS and IEEE ACE. He was named a co-chair of IEEE technical committee on robot learning. He was a recipient of National Talent Scholar award in India and Google Faculty award in 2011. He was named a Alred P. Sloan Fellow in 2011, named a Microsoft Faculty Fellow in 2012, received a NSF Career award in 2013, and received a Early Career Spotlight Award at RSS 2014.

He has also developed algorithms that enable robots (such as STAIR, POLAR and Kodiak) to perform household chores such as unload items from a dishwasher, place items in a fridge, arrange a disorganized house, etc. He has developed learning algorithms for perceiving environments from RGB-D sensors and infer semantic labels, object affordances for tasks such as activity detection and anticipation. Previously, Ashutosh has developed Make3D (http://make3d.cs.cornell.edu), an algorithm that converts a single photograph into a 3D model. Tens of thousands of users used this technology to convert their pictures to 3D. His work has received substantial amount of attention in popular press, including the front-page of New York Times, BBC, ABC, New Scientist Discovery Science, and Wired Magazine.


Enforcement of Opacity Security Properties Using Event Insertion

Oct 21, 2014, 4.10-5pm, Yi-Chin Wu, University of Michigan.

Slides

Abstract

Opacity is a confidentiality property that arises in the analysis of security properties in networked systems. It characterizes whether a "secret" of the system can be inferred by an intruder who knows the system model and partially observes the system behavior. The secret could for instance be a set of system states that should not be revealed to the intruder. The secret of the system is opaque if whenever the secret has occurred (i.e., the system has reached a secret state), there exists another "non-secret" behavior that is observationally equivalent to the intruder.

In this talk, I will first introduce the notions of opacity in the framework of Discrete Event Systems modeled as partially-observable and/or nondeterministic finite state automata. Then, I will focus on the control problem where we enforce opacity when the system is not opaque. Specifically, I will introduce the insertion mechanism, which places
an “insertion function” at the output of the system that changes the system’s output behavior by inserting additional observable events. Such an enforcement mechanism is applicable to systems whose dynamics cannot be modified, such as that of users querying at servers, and can provably enforce opacity. I will show the necessary and sufficient conditions for the existence of a valid insertion function that renders the system opaque. I will also show how we synthesize a valid insertion function when one exists. Finally, the talk will end with a case study that applies our results to the problem of enforcing location privacy in location based services.

Bio:

Yi-Chin Wu is currently a research fellow at the University of Michigan and a visiting scholar at UC Berkeley. She received her M.S. degree in 2011 and Ph.D. degree in 2014, both in EE: Systems at the University of Michigan. Her research interest lies at the intersection of network security, formal methods, and control engineering. Her Ph.D. thesis develops techniques for analyzing and enforcing opacity security properties in Discrete Event Systems.


Probabilistic Model Checking and Strategy Synthesis

Oct 28, 2014, 4.10-5pm, Dave Parker, University of Birmingham, UK.

Slides

Abstract

Probabilistic model checking is an automated technique to verify whether a probabilistic system, e.g., a robot operating in an unknown environment, satisfies a temporal logic property, e.g., "the minimum probability of completing the task within 15 minutes is above 0.98". Dually, we can also synthesise, from a model and a property specification, a strategy for controlling the system in order to satisfy or optimise the property.

This talk will give an overview of automated verification and strategy synthesis for probabilistic systems, and present some recent advances in this area, including: multi-objective model checking (to investigate trade-offs between several conflicting properties), extensions to stochastic game models (to model competitive or collaborative behaviour) and permissive strategy synthesis (to generate flexible and robust controllers). I will describe the tool support for these techniques, in the form of the probabilistic model checker PRISM and its extensions, and present results from the application of these techniques to examples such as robotic motion planning, dynamic power management controllers and task scheduling.

Bio:

Dave Parker is a Lecturer in Computer Science at the University of Birmingham and a Visiting Lecturer at the University of Oxford. His main research interests are in the area of formal verification, with a particular focus on the analysis of quantitative aspects such as probabilistic and real-time behaviour, and he has published over 90 papers in this area. Recent work includes efficient techniques for scalable verification (e.g. abstraction, compositionality), game-theoretic verification methods, and applications of these approaches to areas such as robotics, computer security and DNA computing. He leads development of the widely used probabilistic verification tool PRISM, regularly serves on the programme committees of international conferences (e.g. TACAS, CAV, SEFM, CONCUR, QEST) and frequently gives invited tutorials at summer-schools and workshops.


Roadmapping efforts for research, education and innovation in Cyber-Physical Systems (CPS)

Nov 04, 2014, 4.10-5pm, Martin Torngren, KTH, Stockholm, Sweden.

Slides

Abstract

The talk focuses on roadmapping efforts in the area of Cyber-Physical Systems (CPS). A characterization of CPS is first provided as a baseline, where CPS is related to concepts such as IoT, SoS and Big data. Two strands of roadmapping are then be covered.
1. Roadmapping at the European level. CyPhERS ("Cyber-Physical European Roadmap and Strategy"), a European FP7-project, aims at combining and expanding Europe's competence in Cyber-Physical Systems (CPS).
The project is developing a European strategic research and innovation agenda for CPS to ensure Europe's competitiveness. CyPhERS systematically surveyed, analyzed, and evaluated the significance of CPS for Europe. Currently comprehensive recommendations for action are developed that identify research priorities, support measures for cooperation, research funding policies, and training and standardization. The talk presents a characterization of CPS as well as the preliminary recommendations. 2. Education roadmapping. Education and training are closely related to the investigation and recommendations by CyPhERS. Dealing with the challenges of Cyber-Physical Systems also requires renewed education. An overview is provided of needs, efforts and guidelines for educating the CPS engineer of tomorrow. Implications for Curriculum design are presented and discussed.

Bio:

Martin Törngren has been a Professor in Embedded Control Systems at the Mechatronics division of the KTH Department of Machine Design since 2002. He has particular interest in Cyber-Physical Systems, model based engineering, architectural design, systems integration, and co-design of control applications and embedded systems. He has authored/co-authored more than 100 peer reviewed publications, and also been in charge of developing and leading graduate and continued education courses. He spent time as a post-doc at the EU-JRC, and recently returned from a 10 month sabbatical (2011/12) at Berkeley, University of California. In 1996 he co-founded the company Fengco Real-time Control AB, specializing in advanced tools for developers of embedded control systems and related consultancy. In 1994 he received the SAAB-Scania award for qualified contributions in distributed control systems, and in 2004 the ITEA achievement award 2004 for contributions in the EAST-EEA project. He served as the technical coordinator of the international iFEST ARTEMIS project with 21 partners (2010-2013).


A Case Study of Toyota Unintended Acceleration and Software Safety

Nov 14, 2014, 3.10-4pm, Philip Koopman, Carnegie Mellon University.

Slides

ROOM: 540 DOP Center room

Video of talk is here.

Abstract

Investigations into potential causes of Unintended Acceleration (UA) for Toyota vehicles have made news several times in the past few years. Some blame has been placed on floor mats and sticky throttle pedals. But, a jury trial verdict found that defects in Toyota's Electronic Throttle Control System (ETCS) software and safety architecture caused a fatal mishap. This verdict was based in part on pervasive computer hardware and software issues. This talk will outline key events in the still-ongoing Toyota UA story, and pull together the technical issues that have been discovered by NASA and other experts. The results paint a picture that should inform not only future designers of safety critical software for automobiles, but also all computer-based system designers.

Bio:

Prof. Philip Koopman has served as a testifying expert witness for automotive unintended acceleration cases, including the 2013 Bookout/Schwarz v. Toyota trial. Currently he is in the Electrical and Computer Engineering Department at Carnegie Mellon University. Previously, he was a submarine officer in the US Navy, an embedded CPU architect for Harris Semiconductor, and an embedded system researcher at United Technologies. His research interests focus on software robustness testing, autonomous vehicle software safety, and Cyber-Physical System education. He has conducted more than 140 design reviews of industry software projects including: automotive systems, rail systems, chemical process controls, electrical power components, elevators, lighting systems, heating & cooling equipment, power tools, and safety critical embedded networks. His book Better Embedded System Software describes how to deal with the types of problems that tend to occur in such systems.


tbd

Dec 02, 2014, 4.10-5pm, Klaus Doppler, Nokia Research.

Slides

Abstract

Bio:


This group has the following subpages:

You are not logged in 
Contact 
©2002-2014 U.C. Regents