The formalization of system engineering models and approaches.
Event
VMCAI 2017
18th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI 2017) VMCAI provides a forum for researchers from the communities of Verification, Model Checking, and Abstract Interpretation, facilitating interaction, cross-fertilization, and advancement of hybrid methods that combine these and related areas. Scope
Submitted by Anonymous on October 5th, 2016

Dear colleagues,

First of all, it is a distinct pleasure to introduce a stable version of the shiny new KeYmaera X theorem prover for hybrid systems.

http://keymaeraX.org/

If you're around beautiful Cyprus in November, please also come to the KeYmaera X tutorial at FM 2016

http://keymaerax.org/tutorial/FM-2016.html

We will be demonstrating how to conduct hybrid systems verification with KeYmaera X as well as a reasonable subset of its new features.

Submitted by Anonymous on October 5th, 2016
Equipment operation represents one of the most dangerous tasks on a construction sites and accidents related to such operation often result in death and property damage on the construction site and the surrounding area. Such accidents can also cause considerable delays and disruption, and negatively impact the efficiency of operations. This award will conduct research to improve the safety and efficiency of cranes by integrating advances in robotics, computer vision, and construction management. It will create tools for quick and easy planning of crane operations and incorporate them into a safe and efficient system that can monitor a crane's environment and provide control feedback to the crane and the operator. Resulting gains in safety and efficiency will reduce fatal and non-fatal crane accidents. Partnerships with industry will also ensure that these advances have a positive impact on construction practice, and can be extended broadly to smart infrastructure, intelligent manufacturing, surveillance, traffic monitoring, and other application areas. The research will involve undergraduates and includes outreach to K-12 students. The work is driven by the hypothesis that the monitoring and control of cranes can be performed autonomously using robotics and computer vision algorithms, and that detailed and continuous monitoring and control feedback can lead to improved planning and simulation of equipment operations. It will particularly focus on developing methods for (a) planning construction operations while accounting for safety hazards through simulation; (b) estimating and providing analytics on the state of the equipment; (c) monitoring equipment surrounding the crane operating environment, including detection of safety hazards, and proximity analysis to dynamic resources including materials, equipment, and workers; (d) controlling crane stability in real-time; and (e) providing feedback to the user and equipment operators in a "transparent cockpit" using visual and haptic cues. It will address the underlying research challenges by improving the efficiency and reliability of planning through failure effects analysis and creating methods for contact state estimation and equilibrium analysis; improving monitoring through model-driven and real-time 3D reconstruction techniques, context-driven object recognition, and forecasting motion trajectories of objects; enhancing reliability of control through dynamic crane models, measures of instability, and algorithms for finding optimal controls; and, finally, improving efficiency of feedback loops through methods for providing visual and haptic cues.
Off
Pennsylvania State University
-
National Science Foundation
John Messner
Submitted by Chinemelu Anumba on September 24th, 2016
The automotive industry finds itself at a cross-roads. Current advances in MEMS sensor technology, the emergence of embedded control software, the rapid progress in computer technology, digital image processing, machine learning and control algorithms, along with an ever increasing investment in vehicle-to-vehicle (V2V) and vehicle-to-infrastructure (V2I) technologies, are about to revolutionize the way we use vehicles and commute in everyday life. Automotive active safety systems, in particular, have been used with enormous success in the past 50 years and have helped keep traffic accidents in check. Still, more than 30,000 deaths and 2,000,000 injuries occur each year in the US alone, and many more worldwide. The impact of traffic accidents on the economy is estimated to be as high as $300B/yr in the US alone. Further improvement in terms of driving safety (and comfort) necessitates that the next generation of active safety systems are more proactive (as opposed to reactive) and can comprehend and interpret driver intent. Future active safety systems will have to account for the diversity of drivers' skills, the behavior of drivers in traffic, and the overall traffic conditions. This research aims at improving the current capabilities of automotive active safety control systems (ASCS) by taking into account the interactions between the driver, the vehicle, the ASCS and the environment. Beyond solving a fundamental problem in automotive industry, this research will have ramifications in other cyber-physical domains, where humans manually control vehicles or equipment including: flying, operation of heavy machinery, mining, tele-robotics, and robotic medicine. Making autonomous/automated systems that feel and behave "naturally" to human operators is not always easy. As these systems and machines participate more in everyday interactions with humans, the need to make them operate in a predictable manner is more urgent than ever. To achieve the goals of the proposed research, this project will use the estimation of the driver's cognitive state to adapt the ASCS accordingly, in order to achieve a seamless operation with the driver. Specifically, new methodologies will be developed to infer long-term and short-term behavior of drivers via the use of Bayesian networks and neuromorphic algorithms to estimate the driver's skills and current state of attention from eye movement data, together with dynamic motion cues obtained from steering and pedal inputs. This information will be injected into the ASCS operation in order to enhance its performance by taking advantage of recent results from the theory of adaptive and real-time, model-predictive optimal control. The correct level of autonomy and workload distribution between the driver and ASCS will ensure that no conflicts arise between the driver and the control system, and the safety and passenger comfort are not compromised. A comprehensive plan will be used to test and validate the developed theory by collecting measurements from several human subjects while operating a virtual reality-driving simulator.
Off
University of Southern California
-
National Science Foundation
Submitted by Laurent Itti on September 23rd, 2016
As information technology has transformed physical systems such as the power grid, the interface between these systems and their human users has become both richer and much more complex. For example, from the perspective of an electricity consumer, a whole host of devices and technologies are transforming how they interact with the grid: demand response programs; electric vehicles; "smart" thermostats and appliances; etc. These novel technologies are also forcing us to rethink how the grid interacts with its users, because critical objectives such as stability and robustness require effective integration among the many diverse users in the grid. This project studies the complex interweaving of humans and physical systems. Traditionally, a separation principle has been used to isolate humans from physical systems. This principle requires users to have preferences that are well-defined, stable, and quickly discoverable. These assumptions are increasingly violated in practice: users' preferences are often not well-defined; unstable over time; and take time to discover. Our project articulates a new framework for interactions between physical systems and their users, where users' preferences must be repeatedly learned over time while the system continually operates with respect to imperfect preference information. We focus on the area of power systems. Our project has three main thrusts. First, user models are rethought to reflect the fact this new dynamic view of user preferences, where even the users are learning over time. The second thrust focuses on developing a new system model that learns about users, since we cannot understand users in a "single-shot"; rather, repeated interaction with the user is required. We then focus on the integration of these two new models. How do we control and operate a physical system, in the presence of the interacting "learning loops", while mediating between many competing users? We apply ideas from mean field games and optimal power flow to capture, analyze, and transform the interaction between the system and the ongoing preference discovery process. Our methods will yield guidance for market design in power systems where user preferences are constantly evolving. If successful, our project will usher in a fundamental change in interfacing physical systems and users. For example, in the power grid, our project directly impacts how utilities design demand response programs; how smart devices learn from users; and how the smart grid operates. In support of this goal, the PIs intend to develop avenues for knowledge transfer through interactions with industry. The PIs will also change their education programs to reflect a greater entanglement between physical systems and users.
Off
Stanford University
-
National Science Foundation
Submitted by Ramesh Johari on September 23rd, 2016
This project develops advanced cyber-physical sensing, modeling, control, and optimization methods to significantly improve the efficiency of algal biomass production using membrane bioreactor technologies for waste water processing and algal biofuel. Currently, many wastewater treatment plants are discharging treated wastewater containing significant amounts of nutrients, such as nitrogen, ammonium, and phosphate ions, directly into the water system, posing significant threats to the environment. Large-scale algae production represents one of the most promising and attractive solutions for simultaneous wastewater treatment and biofuel production. The critical bottleneck is low algae productivity and high biofuel production cost. The previous work of this research team has successfully developed an algae membrane bioreactor (A-MBR) technology for high-density algae production which doubles the productivity in an indoor bench-scale environment. The goal of this project is to explore advanced cyber-physical sensing, modeling, control, and optimization methods and co-design of the A-MBR system to bring the new algae production technology into the field. The specific goal is to increase the algal biomass productivity in current practice by three times in the field environment while minimizing land, capital, and operating costs. Specifically, the project will (1) adapt the A-MBR design to address unique new challenges for algae cultivation in field environments, (2) develop a multi-modality sensor network for real-time in-situ monitoring of key environmental variables for algae growth, (3) develop data-driven knowledge-based kinetic models for algae growth and automated methods for model calibration and verification using the real-time sensor network data, and (4) deploy the proposed CPS system and technologies in the field for performance evaluations and demonstrate its potentials. This project will demonstrate a new pathway toward green and sustainable algae cultivation and biofuel production using wastewater, addressing two important challenging issues faced by our nation and the world: wastewater treatment and renewable energy. It will provide unique and exciting opportunities for mentoring graduate students with interdisciplinary training opportunities, involving K-12 students, women and minority students. With web-based access and control, this project will convert the bench-scale and pilot scale algae cultivation systems into an exciting interactive online learning platform to educate undergraduate and high-school students about cyber-physical system design, process control, and renewable biofuel production.
Off
University of Maryland College Park
-
National Science Foundation
Submitted by Piya Pal on September 23rd, 2016
Laboratory-on-a-chip (LoC) technology is poised to improve global health through development of low-cost, automated point-of-care testing devices. In countries with few healthcare resources, clinics often have drugs to treat an illness, but lack diagnostic tools to identify patients who need them. To enable low-cost diagnostics with minimal laboratory support, this project will investigate domain-specific LoC programming language and compiler design in conjunction with device fabrication technologies (process flows, sensor integration, etc.). The project will culminate by building a working LoC that controls fluid motion through electronic signals supplied by a host PC; a forensic toxicology immunoassay will be programmed in software and executed on the device. This experiment will demonstrate benefits of programmable LoC technology including miniaturization (reduced reagent consumption), automation (reduced costs and uncertainties associated with human interaction), and general-purpose software-programmability (the device can execute a wide variety of biochemical reactions, all specified in software). Information necessary to reproduce the device, along with all software artifacts developed through this research effort, will be publicly disseminated. This will promote widespread usage of software-programmable LoC technology among researchers in the biological sciences, along with public and industrial sectors including healthcare and public health, biotechnology, water supply management, environmental toxicity monitoring, and many others. This project designs and implements a software-programmable cyber-physical laboratory-on-a-chip (LoC) that can execute a wide variety of biological protocols. By integrating sensors during fabrication, the LoC obtains the capability to send feedback in real-time to the PC controller, which can then make intelligent decisions regarding which biological operations to execute next. To bring this innovative and transformative platform to fruition, the project tackles several formidable research challenges: (1) cyber-physical LoC programming models and compiler design; (2) LoC fabrication, including process flows and cyber-physical sensor integration; and (3) LoC applications that rely on cyber-physical sensory feedback and real-time decision-making. By constructing a working prototype LoC, and programming a representative feedback-driven forensic toxicology immunoassay, the project demonstrates that the proposed system can automatically execute biochemical reactions that require a closed feedback loop. Expected broader impacts of the proposed work include reduced cost and increased reliability of clinical diagnostics, engagement with U.S. companies that use LoC technology, training of graduate and undergraduate students, increased engagement and retention efforts targeting women and underrepresented minorities, student-facilitated peer-instruction at UC Riverside, a summer residential program for underrepresented minority high-school students at the University of Tennessee, collaborations with researchers at the Oak Ridge National Laboratory, and creation, presentation, and dissemination of tutorial materials to promote the adoption and use of software-programmable LoCs among the wider scientific community.
Off
University of Tennessee - Knoxville
-
National Science Foundation
Submitted by Philip Rack on September 23rd, 2016
Electricity usage of buildings (including offices, malls and residential apartments) represents a significant portion of a nation's energy expenditure and carbon footprint. Buildings are estimated to consume 72% of the total electricity production in the US. Unfortunately, however, 30% of this energy consumption is wasted. Virtual energy assessment is an approach that can optimize building energy efficiency and minimize waste at a low cost with minimal expert intervention. A virtual energy audit includes a thorough and near real time analysis of different sources of building energy usage, individualized energy footprints of load appliances and devices, and proactive identification of energy holes and air leakages. This project builds a low cost solution that combines the use of non-intrusive single point energy monitoring and low cost IR cameras to provide continuous energy audits. The system will provide continuous virtual audit reports to the landlords or residential users. The system will be deployed in low-income neighborhoods in Baltimore City, Maryland, where poor insulation problems are assumed to be fiscally insurmountable and low cost solutions to determining these issues is important for the landlords. To develop a scalable low cost virtual energy auditing system, this breakthrough research pursues the interfaces of smart building sensing, computing and actuation. The project will be executed under three main research thrust areas. First, it utilizes an autonomous discovery, profiling and rule-based predictive model to capture the relationship between disaggregated power measures and a device's actual usage patterns to pinpoint any abnormal consumption. Second, the PIs develop zero-energy far-infrared imaging sensors for low cost low frequency heat map scanning and air leakage detection. Third, the project engineers and evaluates cyber-physical building sensing system with a control level design perspective for virtual energy auditing that drives the realization of deep energy savings and building efficiency. Additionally, the PIs with collaboration from Constellation will host building energy education projects and workshop where undergraduate, high school, and underrepresented group of students would understand how to design and program energy meters and smart plugs.
Off
University of Maryland Baltimore County
-
National Science Foundation
Nilanjan Banerjee
Ryan Robucci
Submitted by Anonymous on September 22nd, 2016
Assistive machines - like powered wheelchairs, myoelectric prostheses and robotic arms - promote independence and ability in those with severe motor impairments. As the state- of-the-art in these assistive Cyber-Physical Systems (CPSs) advances, more dexterous and capable machines hold the promise to revolutionize ways in which those with motor impairments can interact within society and with their loved ones, and to care for themselves with independence. However, as these machines become more capable, they often also become more complex. Which raises the question: how to control this added complexity? A new paradigm is proposed for controlling complex assistive Cyber-Physical Systems (CPSs), like robotic arms mounted on wheelchairs, via simple low-dimensional control interfaces that are accessible to persons with severe motor impairments, like 2-D joysticks or 1-D Sip-N-Puff interfaces. Traditional interfaces cover only a portion of the control space, and during teleoperation it is necessary to switch between different control modes to access the full control space. Robotics automation may be leveraged to anticipate when to switch between different control modes. This approach is a departure from the majority of control sharing approaches within assistive domains, which either partition the control space and allocate different portions to the robot and human, or augment the human's control signals to bridge the dimensionality gap. How to best share control within assistive domains remains an open question, and an appealing characteristic of this approach is that the user is kept maximally in control since their signals are not altered or augmented. The public health impact is significant, by increasing the independence of those with severe motor impairments and/or paralysis. Multiple efforts will facilitate large-scale deployment of our results, including a collaboration with Kinova, a manufacturer of assistive robotic arms, and a partnership with Rehabilitation Institute of Chicago. The proposal introduces a formalism for assistive mode-switching that is grounded in hybrid dynamical systems theory, and aims to ease the burden of teleoperating high-dimensional assistive robots. By modeling this CPS as a hybrid dynamical system, assistance can be modeled as optimization over a desired cost function. The system's uncertainty over the user's goals can be modeled via a Partially Observable Markov Decision Processes. This model provides the natural scaffolding for learning user preferences. Through user studies, this project aims to address the following research questions: (Q1) Expense: How expensive is mode-switching? (Q2) Customization Need: Do we need to learn mode-switching from specific users? (Q3) Learning Assistance: How can we learn mode-switching paradigms from a user? (Q4) Goal Uncertainty: How should the assistance act under goal uncertainty? How will users respond? The proposal leverages the teams shared expertise in manipulation, algorithm development, and deploying real-world robotic systems. The proposal also leverages the teams complementary strengths on deploying advanced manipulation platforms, robotic motion planning and manipulation, and human-robot comanipulation, and on robot learning from human demonstration, control policy adaptation, and human rehabilitation. The proposed work targets the easier operation of robotic arms by severely paralyzed users. The need to control many degrees of freedom (DoF) gives rise to mode-switching during teleoperation. The switching itself can be cumbersome even with 2- and 3-axis joysticks, and becomes prohibitively so with more limited (1-D) interfaces. Easing the operation of switching not only lowers this burden on those already able to operate robotic arms, but may open use to populations to whom assistive robotic arms are currently inaccessible. This work is clearly synergistic: at the intersection of robotic manipulation, human rehabilitation, control theory, machine learning, human-robot interaction and clinical studies. The project addresses the science of CPS by developing new models of the interaction dynamics between the system and the user, the technology of CPS by developing new interfaces and interaction modalities with strong theoretical foundations, and the engineering of CPS by deploying our algorithms on real robot hardware and extensive studies with able-bodied and users with sprinal cord injuries.
Off
Carnegie Mellon University
-
National Science Foundation
Submitted by Siddhartha Srinivasa on September 22nd, 2016
Infrastructure networks are the foundation of the modern world. Their continued reliable and efficient function without exhausting finite natural resources is critical to the security, continued growth and technological advancement of the United States. Currently these systems are in a state of rapid flux due to a collision of trends such as growing populations, expanding integration of information technology, and increasing motivation to adopt sustainable practices. These trends beget both exciting potential benefits and dangerous challenges. Added sensing, communication, and computational capabilities hold the promise of increased reliability, efficiency and sustainability from "smart" infrastructure systems. At the same time, new technologies such as renewable energy resources in power systems, autonomous vehicles, and software defined communication networks, are testing the limits of current operational and market policies. The rapidly changing suite of system components can cause new, unforeseen interactions that can lead to instability, performance deterioration, or catastrophic failures. Achieving the full benefits of these systems will require a shift from the existing focus on approaches that analyze each aspect of interest in isolation, to a more holistic view that encompasses all of the relevant factors such as stability, robustness, performance and efficiency, and takes into account the presence of human participants. This project provides a research roadmap to construct analysis, design and control tools that ensure the seamless integration of computational algorithms, physical components and human interactions in next generation infrastructure systems. Although there has been a great deal of research on stability questions in large scale distributed systems, there has been little effort directed toward questions of performance, robustness and efficiency in these systems, especially those with heterogeneous components and human participants. This research employs coupled oscillator systems as a common modeling framework to (i) characterize stability and performance of infrastructure systems, and (ii) develop distributed controllers that guarantee performance, efficiency and robustness by isolating disturbances and optimizing performance objectives. Practical solutions require that the theory be tightly integrated with the economic mechanisms necessary to incentivize users to enhance system stability, efficiency and reliability; therefore the work will also include the design of economic controls. In order to ground the mathematical foundations, theory and algorithms described above, the results will be applied to three target infrastructure networks where coupled oscillator models have played a foundational role in design and control: power, communication, and transportation systems. This approach allows the development of cross-cutting, fundamental principles that can be applied across problem specific boundaries and ensures that the research makes an impact on these specific infrastructure networks. This project will also incorporate concepts into existing undergraduate and graduate courses.
Off
Cornell University
-
National Science Foundation
Submitted by Ao Tang on September 22nd, 2016
Subscribe to Modeling