CRII: CPS: Safe Cyber-Physical Systems Upgrades

pdf

Abstract:

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. Technically, the 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 cyber-physical specification mismatches, a mismatch 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 to identify candidate mismatches. Preliminary results in the first objective include the Hynger tool that instruments the MathWorks’ Simulink/Stateflow models to produce traces for the Daikon dynamic analysis tool, where a cyber-physical mismatch was identified automatically in a CPS case study [1]. Future enhancements will build on our intermediate representation of hybrid automata in HyST for modeling and verifying CPS [2]. 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 mismatches are identified at runtime, a runtime assurance framework building on supervisory control and the Simplex architecture will assure safe CPS runtime operation [3]. The third objective is to evaluate the detection and mitigation methods to enable safe upgrades in energy CPS. Specifically, the results of the other objectives and their ability to ensure safe CPS upgrades will be evaluated in an energy CPS testbed, consisting of an AC electrical distribution microgrid that interfaces DC-producing renewables like photovoltaics to AC. While the results will be applied to an energy CPS testbed, cyber-physical mismatches occur across CPS industries, and the methods, tools, and techniques can be extended to other safety-critical CPS domains such as aerospace, automotive, and biomedical, which are prone to cyber-physical defects due to specification mismatches.

References:

[1] T. T. Johnson, S. Bak, and S. Drager, “Cyber-physical specification mismatch identification with dynamic analysis,” in International Conference on Cyber-Physical Systems (ICCPS), 2015. [Online]. Available: http://verivital.com/hynger/
[2] S. Bak, S. Bogomolov, and T. T. Johnson, “HyST: A source transformation and translation tool for hybrid automaton models,” in Proc. of the 18th Intl. Conf. on Hybrid Systems: Computation and Control (HSCC). ACM, 2015. [Online]. Available: http://verivital.com/hyst/
[3] S. Bak, T. T. Johnson, M. Caccamo, and L. Sha, “Real-time reachability for verified simplex design,” in IEEE Real-Time Systems Symposium (RTSS). Rome, Italy: IEEE Computer Society, Dec. 2014.

  • formal methods
  • hybrid systems
  • Safety
  • software engineering
  • University of Texas at Arlington
  • CPS Domains
  • Energy
  • Critical Infrastructure
  • Energy Sector
  • Transportation
  • CPS Technologies
  • Architectures
  • Foundations
  • Modeling
  • Validation and Verification
  • 2015
  • National CPS PI Meeting 2015
  • Abstract
  • Poster
  • Academia
  • 2015 CPS PI MTG Videos, Posters, and Abstracts
Submitted by Taylor Johnson on