Independent procedures that are used together for checking that a product, service, or system meets requirements and specifications and that it fulfills its intended purpose.
Event
IUBT 2017
The 7th International Symposium on Internet of Ubiquitous and Pervasive Things (IUPT 2017)
To be held in conjunction with Ambient Systems, Networks and Technologies Conference (ANT'17)
Submitted by Anonymous on October 17th, 2016
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
Cyber-physical systems (CPS) encompass the next generation of computerized control for countless aspects of the physical world and interactions thereof. The typical engineering process for CPS reuses existing designs, models, components, and software from one version to the next. For example, in automotive engineering, it is common to reuse significant portions of existing model-year vehicle designs when developing the next model-year vehicle, and such practices are common across CPS industries, from aerospace to biomedical. While reuse drastically enhances efficiency and productivity, it leads to the possibility of introducing unintended mismatches between subcomponents' specifications. For example, a 2011 US National Highway Traffic Safety Administration (NHTSA) recall of over 1.5 million model-year 2005-2010 vehicles was due to the upgrade of a physical transmission component that was not appropriately addressed in software. A mismatch between cyber and physical specifications may occur when a software or hardware upgrade (in effect, a cyber or physical specification change) is not addressed by an update (in effect, a matching specification change) in the other domain. This research will develop new techniques and software tools to detect automatically if cyber-physical specification mismatches exist, and then mitigate the effects of such mismatches at runtime, with the overall goal to yield more reliable and safer CPS upon which society increasingly depends. The detection and mitigation methods developed will be evaluated in an energy CPS testbed. While the evaluation testbed is in the energy domain, the methods are applicable to other CPS domains such as automotive, aerospace, and biomedical. The educational goals will bridge gaps between computer science and electrical engineering, preparing a diverse set of next-generation CPS engineers by developing education platforms to enhance CPS engineering design and verification skills.
The proposed research is to develop new techniques and tools to automatically identify and mitigate the effects of cyber-physical specification mismatches. There are three major research objectives. The first objective is to identify cyber-physical specification mismatches. To identify mismatches, a detection problem will be formalized using the framework of hybrid input/output automata (HIOA). Offline algorithms will be designed to find candidate specifications from models and implementations using static and dynamic analyses, and then identify candidate mismatches. The second objective is to monitor and assure safe CPS upgrades. As modern CPS designs are complex, it may be infeasible to determine all specifications and mismatches between all subcomponents at design time. Runtime monitoring and verification methods will be developed for inferred specifications to detect mismatches at runtime. When they are identified, a runtime assurance framework building on supervisory control and the Simplex architecture will assure safe CPS runtime operation. The third objective is to evaluate safe CPS upgrades in an example CPS. The results of the other objectives and their ability to ensure safe CPS upgrades will be evaluated in an energy CPS testbed, namely an AC electrical distribution microgrid that interfaces DC-producing renewables like photovoltaics to AC.
Award Number
Display Videos in Hero
Off
Institution
University of Texas at Arlington
Lead PI
Taylor Johnson
Performance Period
-
Sponsor
National Science Foundation
Submitted by Taylor Johnson on October 3rd, 2016
Motivated by the fact that the 2014 Ebola outbreak is the largest in history and there is a pressing need to understand how to improve delivery of care with the right technological interventions at the right place, this Rapid Response Research is aimed at realizing a human-in-the-loop medical cyber-physical system (CPS) for monitoring patients, insuring compliance with relevant safety protocols, and collecting data for advancing multidisciplinary research on infectious disease control. The ultimate goal is to enhance safety of Ebola workers by minimizing their contact with potentially contaminated surfaces and materials through integration of methods and technologies to realize smart and connected treatment clinics. This project could impact the response to infectious disease outbreaks by augmenting existing treatment clinics with cost-effective, modular, reconfigurable and
open-design CPS technologies. The project will train a new cadre of engineering students, researchers and innovators to be
sensitive to societal needs and national priorities by involving K-Gray, undergraduate and graduate students in all aspects of the project, especially at the co-ideation and co-design stages. The project will bring together a multidisciplinary team of engineers, scientists, technologists, medical experts, and humanitarian aid workers to develop holistic solutions to infectious disease control. The broader impacts also include operational cost savings in treatment clinics by reducing the need and use of the personal protective equipment and preserve resources such as water by reducing consumption.
In order to prevent, detect and respond to current Ebola outbreak and future similar infectious disease outbreaks, this research plan has the following interconnected aims: (1) contribute new knowledge, methods, and tools to better understand the operational procedures in an infectious disease treatment clinic, (2) design, implement and validate a treatment ward augmented with a medical CPS for patient monitoring, (3) apply intuitive control interfaces and data visualization tools for practical human-robot interaction, (4) realize traded, coordinated and collaborative shared control techniques for safe and effective mobile robot navigation inside a treatment facility, (5) assess acceptability and effectiveness of the technology among health care workers and patients. The team will develop a self-contained, modular and reconfigurable system composed of a connected sensor network for patient monitoring and a mobile robot platform for telemedicine that will primarily focus on the interoperability and integration of existing standardized
hardware and software systems to realize a testbed for verification and validation of a medical CPS. Medical, emergency response and humanitarian aid experts will be engaged to critically assess user-experiences and acceptability among medical staff to develop pathways for fielding the system in a treatment clinic. This RAPID project will lead the way in designing the next generation of human-in-the-loop medical CPS for empowering health care workers worldwide in treating patients during infectious disease outbreaks.
Award Number
Display Videos in Hero
Off
Institution
Worcester Polytechnic Institute
Lead PI
Taskin Padir
Performance Period
-
Sponsor
National Science Foundation
Co-PIs (text)
Sonia Chernova
Michael Gennert
Jeanine Skorinko
Submitted by Taskin Padir on September 28th, 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.
Award Number
Display Videos in Hero
Off
Institution
University of Southern California
Lead PI
Laurent Itti
Performance Period
-
Sponsor
National Science Foundation
Submitted by Laurent Itti on September 23rd, 2016
This project addresses urgent challenges in high confidence validation and verification of automotive vehicles due to on-going and anticipated introduction of advanced, connected and autonomous vehicles into mass production. Since such vehicles operate across both physical and cyber domains, faults can occur in traditional physical components, in cyber components (i.e., algorithms, processors, networks, etc.), or in both. Thus, advanced vehicles need to be tested for both physical and cyber-related fault conditions. The goal of this project is to develop theory, methods, and novel tools for generating and optimizing test trajectories and data inputs that can uncover both physical and cyber faults of future automotive vehicles. The level of vehicle reliability and safety achieved for current vehicles is remarkable considering their mass production, low cost, and wide range of operating conditions. If successful, the research advances made in this project will enable achieving similar levels of reliability and safety for future vehicles relying on advanced driver assistance technologies, connectivity and autonomy. The project will advance the field of cyber-physical systems, in general, and their lifecycle management, in particular. The validation and verification theory and methodology for cyberphysical systems will be expanded for uncovering anomalies and faults, especially using comprehensive case-based and optimization-based techniques for test scenario generation.
The theoretical advances and case studies will contribute to the state-of-the-art in optimal control theory, game theory, information theory, data collection and processing, autonomous and connected vehicles, and automotive control. Sampling-based vehicle data acquisition and vehicle-aware data management strategies will be developed which can be applied more broadly, e.g., to cloud-based vehicle prognostics / conditional maintenance and mobile health-monitoring devices. Finally, approaches for efficient on-board data collection and aggregation will be implemented in a Cyber-physical system (CPS) Black Box prototype. The development of a vehicle-aware data management system (VDMS) will be pursued, leading to optimized use of data mining and compression inside the CPS Black Box to aggressively reduce the communication and computational costs. Synergistically with theoretical and methodological advances, automotive case studies will be undertaken with both realistic simulations and real experiments in collaboration with an industrial partner (AVL).
Award Number
Display Videos in Hero
Off
Co-PIs
Ella Atkins
Institution
University of Michigan Ann Arbor
Lead PI
Ilya V. Kolmanovsky
Performance Period
-
Sponsor
National Science Foundation
Co-PIs (text)
Barzan Mozafari
Mark Oliver
Submitted by Ilya V. Kolmanovsky on September 23rd, 2016
Errors in cyber-physical systems can lead to disastrous consequences. Classic examples date back to the Therac-25 radiation incidents in 1987 and the Ariane 5 rocket crash in 1996. More recently, Toyota's unintended acceleration bug was caused by software errors, and certain cars were found vulnerable to attacks that can take over key parts of the control software, allowing attackers to even disable the brakes remotely. Pacemakers have also been found vulnerable to attacks that can cause deadly consequences for the patient. To reduce the chances of such errors happening, this project investigates the application of a technique called Foundational Verification to cyber-physical systems.
In Foundational Verification, the system being developed is proved correct, in full formal detail, using a proof assistant. The main intellectual merit of the proposal is the attainment of previously unattainable levels of safety for cyber-physical systems because proofs in Foundational Verification are carried out in complete detail. To ensure that the techniques in this project are practical, they are evaluated within the context of a real flying quadcopter. The project's broader significance and importance is the improved correctness, safety and security of cyber-physical systems. In particular, this project lays the foundation for ushering in a new level of formal correctness for cyber-physical systems. Although the initial work focuses on quadcopters, the concepts, ideas, and research contributions have the potential for transformative impact on other kinds of systems, including power-grid software, cars, avionics and medical devices (from pacemakers and insulin pumps to defibrillators and radiation machines).
Award Number
Display Videos in Hero
Off
Co-PIs
Ryan Kastner
Institution
University of California-San Diego
Lead PI
Sorin Lerner
Performance Period
-
Sponsor
National Science Foundation
Co-PIs (text)
Miroslav Krstic
Submitted by Sorin Lerner on September 23rd, 2016
Computation is everywhere. Greeting cards have processors that play songs. Fireworks have processors for precisely timing their detonation. Computers are in engines, monitoring combustion and performance. They are in our homes, hospitals, offices, ovens, planes, trains, and automobiles. These computers, when networked, will form the Internet of Things (IoT). The resulting applications and services have the potential to be even more transformative than the World Wide Web. The security implications are enormous. Internet threats today steal credit cards. Internet threats tomorrow will disable home security systems, flood fields, and disrupt hospitals. The root problem is that these applications consist of software on tiny low-power devices and cloud servers, have difficult networking, and collect sensitive data that deserves strong cryptography, but usually written by developers who have expertise in none of these areas. The goal of the research is to make it possible for two developers to build a complete, secure, Internet of Things applications in three months.
The research focuses on four important principles. The first is "distributed model view controller." A developer writes an application as a distributed pipeline of model-view-controller systems. A model specifies what data the application generates and stores, while a new abstraction called a transform specifies how data moves from one model to another. The second is "embedded-gateway-cloud." A common architecture dominates Internet of Things applications. Embedded devices communicate with a gateway over low-power wireless. The gateway processes data and communicates with cloud systems in the broader Internet. Focusing distributed model view controller on this dominant architecture constrains the problem sufficiently to make problems, such as system security, tractable. The third is "end-to-end security." Data emerges encrypted from embedded devices and can only be decrypted by end user applications. Servers can compute on encrypted data, and many parties can collaboratively compute results without learning the input. Analysis of the data processing pipeline allows the system and runtime to assert and verify security properties of the whole application. The final principle is "software-defined hardware." Because designing new embedded device hardware is time consuming, developers rely on general, overkill solutions and ignore the resulting security implications. The data processing pipeline can be compiled into a prototype hardware design and supporting software as well as test cases, diagnostics, and a debugging methodology for a developer to bring up the new device. These principles are grounded in Ravel, a software framework that the team collaborates on, jointly contributes to, and integrates into their courses and curricula on cyberphysical systems.
Award Number
Display Videos in Hero
Off
Co-PIs
Mark Horowitz
Dan Boneh
Dawson Engler
Keith Winstein
Institution
Stanford University
Lead PI
Philip Levis
Performance Period
-
Sponsor
National Science Foundation
Submitted by Philip Levis on September 23rd, 2016
Event
ANT-17
The 8th International Conference on Ambient Systems, Networks and Technologies (ANT-17)
The goal of the ANT-2017 conference is to provide an international forum for scientists, engineers, and managers in academia, industry, and government to address recent research results and to present and discuss their ideas, theories, technologies, systems, tools, applications, work in progress and experiences on all theoretical and practical issues arising in the ambient systems paradigm, infrastructures, models, and technologies that have significant contributions to the advancement of amb
Submitted by Anonymous on September 15th, 2016