Abstract
The objective of this research is to prove that cyber-physical systems are safe before they are deployed. The approaches the research investigates are extensions of approaches used to test communications protocols. The problems with cyber-physical systems are that 1) they are much more complicated than communications protocols, 2) time is a more critical component of these systems, and 3) in a competitive environment there are likely to be many implementations that must interoperate.
The complexity of communications protocols is reduced by using a layered architecture. Each layer provides a well defined service to the next layer. This research is developing multi-dimensional architectures that reflect the different ways that the cyber-physical system interacts with the physical world. The techniques are evaluated on a driver-assisted merge protocol. An architecture for the merge protocol has four dimensions organized as stacks for communications, external sensors, vehicle monitoring and control, and timing. This architecture will also be useful during standardization.
Timing increases verification complexity by increasing the number of potential execution paths. The research conducted in this project explores how to reduce the number of paths by synchronizing clocks and using simultaneous operations. This approach is reasonable because of the timing accuracy now available with GPS. A two step verification process is used that creates an unambiguous model of the cyber-physical system, first proving that the model is safe, then checking that each implementation conforms to the model. This reduces the number and cost of tests for a three-party merge protocol. Specifically, assuming there are N implementation versions for different manufacturers and models, this approach reduces the number of necessary interaction tests, which would be cubic in N, to a single model verification and N conformance tests.
Nicholas Maxemchuk
Nicholas F. Maxemchuk
Education
· Ph.D. Doctor of Philosophy, Systems Engineering, University of Pennsylvania, May 1975.
· M.S. Moore School of Electrical Engineering, University of Pennsylvania, May 1970.
· B.S. Bachelor of Electrical Engineering, The City College of New York, June 1968. (Graduated Magna Cum Laude).
Academic Experience
· 2001 - Present Full Professor Columbia University
· 2008 - Present Chief Researsher IMDEA Networks, Madrid
· University of Melbourne, Visiting Academic Oct. 99.
· Opponent: KTH Sweden, June 1997.
· Department Visiting Committee, Comp. Sci., University of Texas at Austin 1989-92.
Non-Academic Experience
· 2009-2012 Consultant NYC MTA
· 2008 Chief Scientist Telcordia
· 2007-2010 Consultant Bell Labs, Murray Hill, NJ
· Technical Advisory Board - start-upEnrichnet 2000-2002
· 1996 - 2001 Technology Leader AT&T Research Labs
· Technical Advisory Board start-up - BrightLink Networks 1998->2001
· 1984 - 1996 Department Head AT&T Bell Laboratories
· 1976 - 1984 MTS Bell Labs
· 1968 - 1976 MTS RCA David Sarnoff Res. Cntr.
Current Membership in Professional Organizations
· IEEE, Eta Kappa Nu and Tau Beta Pi
Honors and Awards
· 2006 IEEE Koji Kobayashi Award for Computer and Communications
· 1997 William R. Bennett Prize Paper Award for S. Low, N. F. Maxemchuk, S. Paul, "Anonymous Credit Cards and Its Collusion Analysis," IEEE Trans. on Networking, dec. 1996, vol. 4, no.6, pp 809-816
· 1996 R&D 100 Award for "Document Copying Deterrent System"
· 1989 Elected Fellow of the IEEE
· 1988 Leonard G. Abraham Prize Paper Award, for N. F. Maxemchuk, "Routing in the Manhattan Street Network," IEEE Trans. on Commun., May 1987, vol. COM-35, no. 5, pp. 503-512., also s elected for IEEE ComSoc 50th anniv. iss.
· Selected for IEEE ComSoc 50th anniv. iss., and included in the DQDB standard, E. L. Hahne, A. K. Choudhury, N. F. Maxemchuk, "DQDB Networks With and Without Bandwidth Balancing," IEEE Trans. on Commun., Vol. 40, No. 7, July 1992, pp 1192-1204
Performance Period: 10/01/2013 - 09/30/2016
Institution: Columbia University
Sponsor: National Science Foundation
Award Number: 1329593
Abstract
Implantable Cardiac Defibrillators (ICDs) are at the forefront of preventing sudden death in patients suffering from ventricular arrhythmias. ICDs have evolved into complex Cyber-Physical Systems (CPS)which tightly sensing, hardware, and software to diagnose arrythmias based on electrogram signals and control cardiac excitation. These devices are life-critical, yet the Verification and Validation (V&V) techniques used for establishing their safety have remained somewhat informal, and rely largely on extensive unit testing.
There have been a number of exciting developments in formal verification technologies. This proposal introduces these techniques into the ICD verification process, and will demonstrate their suitability for application in other medical devices. The project will develop a model-based framework for ICDs, and will apply formal verification techniques, such as model checking and reachability analysis, to high-fidelity cardiac electrophysiological models that capture the electrical excitation induced by the ICD's control software. Through extensive collaboration with FDA research staff, the proposal will demonstrate the effectiveness of formal verification technology and suitability in medical device applications.
Performance Period: 12/01/2014 - 08/31/2019
Institution: SUNY at Stony Brook
Sponsor: National Science Foundation
Award Number: 1445770
Abstract
Trustworthy operation of next-generation complex power grid critical infrastructures requires mathematical and practical verification solutions to guarantee the correct infrastructural functionalities. This project develops the foundations of theoretical modeling, synthesis and real-world deployment of a formal and scalable controller code verifier for programmable logic controllers (PLCs) in cyber-physical settings. PLCs are widely used for control automation in industrial control systems. A PLC is typically connected to an engineering workstation where engineers develop the control logic to process the input values from sensors and issue control commands to actuators. The project focuses on protecting infrastructures against malicious control injection attacks on PLCs, such as Stuxnet, that inject malicious code on the device to drive the underlying physical platform to an unsafe state. The broader impact of this proposal is highly significant. It offers potential for real-time security for critical infrastructure systems covering sectors such as energy and manufacturing.
The project's intellectual merit is in providing a mathematical and practical verification framework for cyber-physical systems through integration of offline formal methods, online monitoring solutions, and power systems analysis. Offline formal methods do not scale for large-scale platforms due to their exhaustive safety analysis of all possible system states, while online monitoring often reports findings too late for preventative action. This project takes a hybrid approach that dynamically predicts the possible next security incidents and reports to operators before an unsafe state is encountered, allowing time for response. The broader impact of this project is in providing practical mathematical analysis capabilities for general cyber-physical safety-critical infrastructure with potential direct impact on our national security. The research outcomes are integrated into education modules for graduate, undergraduate, and K-12 classrooms.
Saman Zonouz
Saman Zonouz is an Associate Professor at Georgia Tech in the Schools of Cybersecurity and Privacy (SCP) and Electrical and Computer Engineering (ECE). Saman directs the Cyber-Physical Security Laboratory (CPSec). His research focuses on security and privacy research problems in cyber-physical systems including attack detection and response capabilities using techniques from systems security, control theory and artificial intelligence. His research has been awarded by Presidential Early Career Awards for Scientists and Engineers (PECASE), the NSF CAREER Award in Cyber-Physical Systems (CPS), Significant Research in Cyber Security by the National Security Agency (NSA), and Faculty Fellowship Award by the Air Force Office of Scientific Research (AFOSR). His research group has disclosed several security vulnerabilities with published CVEs in widely-used industrial controllers such as Siemens, Allen Bradley, and Wago. Saman is currently a Co-PI on President Biden’s American Rescue Plan $65M Georgia AI Manufacturing (GA-AIM) project. Saman was invited to co-chair the NSF CPS PI Meeting as well as the NSF CPS Next Big Challenges Workshop. Saman has served as the chair and/or program committee member for several conferences (e.g., IEEE Security and Privacy, CCS, NDSS, DSN, and ICCPS). Saman obtained his Ph.D. in Computer Science from the University of Illinois at Urbana-Champaign.
Performance Period: 01/01/2015 - 12/31/2017
Institution: Rutgers University New Brunswick
Sponsor: National Science Foundation
Award Number: 1446471
Abstract
The project investigates a formal verification framework for artificial pancreas (AP) controllers that automate the delivery of insulin to patients with type-1 diabetes (T1D). AP controllers are safety critical: excessive insulin delivery can lead to serious, potentially fatal, consequences. The verification framework under development allows designers of AP controllers to check that their control algorithms will operate safely and reliably against large disturbances that include patient meals, physical activities, and sensor anomalies including noise, delays, and sensor attenuation. The intellectual merits of the project lie in the development of state-of-the-art formal verification tools, that reason over mathematical models of the closed-loop including external disturbances and insulin-glucose response. These tools perform an exhaustive exploration of the closed loop system behaviors, generating potentially adverse situations for the control algorithm under verification. In addition, automatic techniques are being investigated to help AP designers improve the control algorithm by tuning controller parameters to eliminate harmful behaviors and optimize performance. The broader significance and importance of the project are to minimize the manual testing effort for AP controllers, integrate formal tools in the certification process, and ultimately ensure the availability of safe and reliable devices to patients with type-1 diabetes. The framework is made available to researchers who are developing AP controllers to help them verify and iteratively improve their designs. The team is integrating the research into the educational mission by designing hands-on courses to train undergraduate students in the science of Cyber-Physical Systems (CPS) using the design of AP controllers as a motivating example. Furthermore, educational material that explains the basic ideas, current challenges and promises of the AP concept is being made available to a wide audience that includes patients with T1D, their families, interested students, and researchers.
The research is being carried out collaboratively by teams of experts in formal verification for Cyber-Physical Systems, control system experts with experience designing AP controllers, mathematical modeling experts, and clinical experts who have clinically evaluated AP controllers. To enable the construction of the verification framework from the current state-of-the-art verification tools, the project is addressing major research challenges, including (a) building plausible mathematical models of disturbances from available clinical datasets characterizing human meals, activity patterns, and continuous glucose sensor anomalies. The resulting models are integrated in a formal verification framework; (b) simplifying existing models of insulin glucose response using smaller but more complex delay differential models; (c) automating the process of abstracting the controller implementation for the purposes of verification; (d) producing verification results that can be interpreted by control engineers and clinical researchers without necessarily understanding formal verification techniques; and (e) partially automating the process of design improvements to potentially eliminate severe faults and improve performance. The framework is evaluated on a set of promising AP controller designs that are currently under various stages of clinical evaluation.
Sriram Sankaranarayanan
Sriram Sankaranarayanan is an assistant professor of Computer Science
at the University of Colorado, Boulder. His research interests include
automatic techniques for reasoning about the behavior of computer and
cyber-physical systems. Sriram obtained a PhD in 2005 from Stanford
University where he was advised by Zohar Manna and Henny Sipma.
Subsequently he worked as a research staff member at NEC
research labs in Princeton, NJ. He has been on the faculty at CU
Boulder since 2009. Sriram has been the recipient of awards including
the President's Gold Medal from IIT Kharagpur (2000), Siebel
Scholarship (2005), the CAREER award from NSF (2009) and the Dean's
award for outstanding junior faculty for the College of Engineering at
CU Boulder (2012).
Performance Period: 10/01/2014 - 09/30/2017
Institution: University of Colorado at Boulder
Sponsor: National Science Foundation
Award Number: 1446900
Abstract
This project develops a theoretical framework as well as software tools to support testing and verification of a Cyber-Physical System (CPS) within a Model-Based Design (MBD) process. The theoretical bases of the framework are stochastic optimization methods, and robustness notions of formal specification languages. The project's research comprises three components: development of conditions on the algorithms and on the structure of the CPS for inferring finite-time guarantees on the randomized testing process; the study of testing methods that can support modular and compositional system design; and investigation of appropriate notions of conformance between two system models and between a model and its implementation on a computational platform. All of these components are needed to support testing and verification in all the stages of an MBD process as well as to support component reuse, incremental system improvements and modular design. The evaluation of the framework is driven by the problems of verifying automotive control systems and medical devices.
As safety-critical CPS become ubiquitous, the need for design methods that guarantee correct system functionality and performance becomes more urgent. Certification and government agencies need dependable testing and verification tools to incorporate in certification standards and procedures. The concrete benefits to the society are both in terms of reduced catastrophic design errors in new products and in terms of reduced economic costs for new product development. The former increases the confidence in new technologies while the latter improves the competitiveness of the companies that utilize such technologies. The theoretical results of this project are being incorporated into software tools for testing, verification and validation of complex CPS. The evaluation focus of the project on verifying infusion pumps and automotive control software ultimately helps in avoiding harmful losses due to errors in these safety-critical systems. The use of any software tool that is based on formal or semi-formal methods requires engineers with solid training on these technologies. This proposal puts forward an education curriculum for developing new courses that introduce formal and semi-formal methods for CPS at all levels of higher education, i.e., undergraduate, graduate and continuing education. Particular attention is devoted into on-line continuing education of practicing engineers who must acquire new MBD skills.
Performance Period: 08/15/2014 - 07/31/2019
Sponsor: National Science Foundation
Award Number: 1350420
Abstract
This project aims to achieve key technology, infrastructure, and regulatory science advances for next generation medical systems based on the concept of medical application platforms (MAPs). A MAP is a safety/security-critical real-time computing platform for: (a) integrating heterogeneous devices and medical IT systems, (b) hosting application programs ("apps") that provide medical utility through the ability to both acquire information and update/control integrated devices, IT systems, and displays. The project will develop formal architectural and behavioral specification languages for defining MAPs, with a focus on techniques that enable compositional reasoning about MAP component interoperability and safety. These formal languages will include an extensible property language to enable the specification of real-time, quality-of-service, and attributes specific to medical contexts that can be leveraged by code generation, testing, and verification tools.
The project will work closely with a synergistic team of clinicians, device industry partners, regulators, and medical device interoperability and safety standard organizations to develop an open source MAP innovation platform to enable key stakeholders within the nation's health care ecosphere to identify, prototype, and evaluate solutions to key technology and regulatory challenges that must be overcome to develop a commodity market of regulated MAP components. Because MAPs provide pre-built certified infrastructure and building blocks for rapidly developing multi-device medical applications, this research has the potential to usher in a new paradigm of medical system that significantly increases the pace of innovation, lowers development costs, enables new functionality by aggregating multiple devices into a system of systems, and achieves greater system safety.
Performance Period: 10/01/2012 - 09/30/2016
Institution: Kansas State University
Sponsor: National Science Foundation
Award Number: 1239534
Abstract
The objective of this project is to create a focused cyber-physical design environment to accelerate the development of miniature medical devices in general and swallowable systems in particular. The project develops new models and tools including a web-based integrated simulation environment,capturing the interacting dynamics of the computational and physical components of devices designed to work inside the human body, to enable wider design space exploration, and, ultimately, to lower the barriers which have thus far impeded system engineering of miniature medical devices. Currently, a few select individuals with deep domain expertise create these systems. The goal is to open this field to a wider community and at the same time create better designs through advanced tool support. The project defines a component model and corresponding domain-specific modeling language to provide a common framework for design capture, design space exploration, analysis and automated synthesis of all hardware and software artifacts. The project also develops a rich and extensible component and design template library that designers can reuse. The online design environment will provide early feedback and hence, it will lower the cost of experimentation with alternatives. The potential benefit is not just incremental (in time and cost), but can lead to novel ideas by mitigating the risk of trying unconventional solutions.
Trends in consumer electronics such as miniaturization, low power operation, and wireless technologies have enabled the design of miniature devices that hold the potential to revolutionize medicine. Transformational societal public health benefits (e.g., early diagnosis of colorectal cancer or prevention of heart failure) are possible through less invasive and more accurate diagnostic and interventional devices. By eliminating large incisions in favor of natural orifices or small ports, these medical devices can increase diagnostic screening effectiveness and reduce pain and recovery time. Furthermore, if successful, the proposed scientific approach can be extended to any other application, wherever size, power efficiency, and high confidence are stringent requirements. The educational plan of the project is centered on the web-based design environment that will also contain an interface for high school students to experiment with medical cyber-physical devices in a virtual environment. Students will be able to build medical devices from a library of components, program them using an intuitive visual programming language and operate them in various simulated environments. A Summer Camp organized in the framework of this project will enhance students learning experience with real hands-on experimentation in a lab.
Performance Period: 12/01/2012 - 11/30/2016
Institution: Vanderbilt University
Sponsor: National Science Foundation
Award Number: 1239355
Project URL
Abstract
Wireless body area sensing networks (WBANs) have the potential to revolutionize health care in the near term and enhance other application domains including sports, entertainment, military and emergency situations. These WBANs represent a novel cyber-physical system that unites engineering systems, the natural world and human individuals. The coupling of bio-sensors with a wireless infrastructure enables the real-time monitoring of an individual's health, environment and related behaviors continuously, as well as the provision of real-time feedback with nimble, adaptive, and personalized interventions. Recent technological advances in low power integrated circuits, signal processing and wireless communications have enabled the design of tiny, low cost, lightweight, intelligent medical devices, sensors and networking platforms that have the potential to make the concept of truly pervasive wireless sensor networks a reality. To develop the WBANs of the future, this breakthrough research will pursue the interfaces of sensing, communication and control.
This project aims to investigate energy and delay sensitive sensing, communication, decision-making and control for health monitoring application of wireless body area networks. In these systems, sensors with varying accuracy observe heterogeneous source signals that must be processed and communicated and used for inference and decision-making purposes. All of these operations must be carried out in the presence of constraints on power and energy resources at the sensors, limited communication and computational abilities and with low end-to-end delay between the sensing of information to its eventual utilization. In this project, a global (end-to end) perspective is adopted that optimizes network operation to improve the information quality and enhance the lifetime of the network, focusing in particular on optimal use of sensor resources such as energy, new sensing and communication paradigms that balance information quality and energy expenditure, and real-time encoding and decoding methods that provide strict delay guarantees on information delivery. The proposed work will contribute to several research areas including optimal resource allocation at sensors, adaptive sensing methods, real-time encoding and decoding and event-based communication. The educational impact of the proposed research will come through the training of new information technology professionals and scientists with expertise in cross-disciplinary research, development of new courses based on the proposed research activity and continued efforts to include women and under-represented minorities in the research program.
Performance Period: 01/01/2015 - 12/31/2019
Institution: University of Southern California
Sponsor: National Science Foundation
Award Number: 1446901
Abstract
Buildings in the U.S. contribute to 39% of energy use, consume approximately 70% of the electricity, and account for 39% of CO2 emissions. Hence, developing green building architectures is an extremely critical component in energy sustainability. The investigators will develop a unified analytical approach for green building design that comprehensively manages energy sustainability by taking into account the complex interactions between these systems of systems, providing a high degree of security, agility and robust to extreme events. The project will serve to advance the general science in CPS, help bridge the gap between the cyber and civil infrastructure communities, educate students across different disciplines, include topics in curriculum development, and actively recruit underrepresented minority and undergraduate students. The main thesis of this research is that ad hoc green energy designs are often myopic, not taking into account key interdependencies between subsystems and users, and thus often lead to undesirable solutions. In fact, studies have shown that 28%-35% of LEED-certified buildings consumed more energy than their conventional counterparts, all of which calls for the development of a comprehensive analytical foundation for designing green buildings.
In particular, the investigators will focus on three interrelated thrust areas: (i) Integrated energy management for a single-building, where the goal is to jointly consider the complex interactions among building subsystems. The investigators will develop novel control schemes that opportunistically exploit the energy demand elasticity of the building subsystems and adapt to occupancy patterns, human comfort zones, and ambient environments. (ii) Managing multi-building interactions to develop (near) optimal distributed control and coordination schemes that provide performance guarantees. (iii) Designing for anomalous conditions such as extreme weather and malicious attacks, where power grid connections and/or cyber-networks are disrupted. The research will provide directions at developing an analytical foundation and cross-cutting principles that will shed insight on the design and control of not only building systems, but also general CPS systems. An important goal is to help bridge the gap between the networking, controls, and civil infrastructure communities by giving talks and publishing works in all of these forums. The investigators will disseminate the research findings to industry as well as offer education and outreach programs to the K-12 students in STEM disciplines. The investigators will also actively continue their already strong existing efforts in recruiting women and underrepresented minorities, as well as providing rich research experience to undergraduate REU students. This project will provide fertile training for students spanning civil infrastructure research, networking, controls, optimization, and algorithmic development. The investigators will also actively include the outcomes of the research in existing and new courses at both the Ohio State University and Virginia Tech.
Performance Period: 01/01/2015 - 12/31/2017
Sponsor: National Science Foundation
Award Number: 1446478
Abstract
The objective of this research is an injection of new modeling techniques into the area of Cyber-Physical Systems (CPSs). The approach is to design new architectures for domain-specific modeling tools in order to permit feedback from analysis, validation, and verification engines to influence how CPSs are designed. This project involves new research into the integration of existing, heterogeneous modeling languages in order to address problems in CPS design, rather than a single language for all CPS. Since many tools for analysis, validation, and verification focus on at most two of the three major components of CPS (communication, computation, and control), new paradigms in modeling are used to integrate tools early in the design process. The algorithms and software developed in this project run validation and verification tools on models, and then close the loop by using the tool outputs to automatically modify the system models. The satisfaction of design requirements in CPSs is critical for tomorrow's societal technologies such as smart buildings, home healthcare, and water management. Among the most compelling design requirements are those of safety, and CPSs for autonomous vehicles exemplify this well. By involving a full-sized autonomous vehicle in this project, the validation and verification of safety requirements is tied to a concrete platform that is broadly understood. By involving students in the design of behaviors of the vehicle, the project exposes scientists and engineers of tomorrow to societal-scale problems, and tools to address them.
Performance Period: 05/01/2013 - 04/30/2019
Sponsor: National Science Foundation
Award Number: 1253334
Project URL
Project URL