Cyber-Physical Specification Mismatches

TL;DR

This paper introduces Hynger, an automated tool that uses dynamic analysis and invariant inference to identify unstated assumptions and specification mismatches in cyber-physical systems, enhancing safety and reliability.

Contribution

The paper presents Hynger, a novel tool that instruments Simulink/Stateflow models and integrates with Daikon to automatically detect specification mismatches in CPS.

Findings

Hynger successfully detects specification mismatches in case studies.

The approach identifies violations of assumed tolerances due to system changes.

Hynger demonstrates effectiveness in safety-critical CPS environments.

Abstract

Embedded systems use increasingly complex software and are evolving into cyber-physical systems (CPS) with sophisticated interaction and coupling between physical and computational processes. Many CPS operate in safety-critical environments and have stringent certification, reliability, and correctness requirements. These systems undergo changes throughout their lifetimes, where either the software or physical hardware is updated in subsequent design iterations. One source of failure in safety-critical CPS is when there are unstated assumptions in either the physical or cyber parts of the system, and new components do not match those assumptions. In this work, we present an automated method towards identifying unstated assumptions in CPS. Dynamic specifications in the form of candidate invariants of both the software and physical components are identified using dynamic analysis (executing and/or simulating the system implementation or model thereof). A prototype tool called Hynger (for HYbrid iNvariant GEneratoR) was developed that instruments Simulink/Stateflow (SLSF) model diagrams to generate traces in the input format compatible with the Daikon invariant inference tool, which has been extensively applied to software systems. Hynger, in conjunction with Daikon, is able to detect candidate invariants of several CPS case studies. We use the running example of a DC-to-DC power converter, and demonstrate that Hynger can detect a specification mismatch where a tolerance assumed by the software is violated due to a plant change. Another case study of an automotive control system is also introduced to illustrate the power of Hynger and Daikon in automatically identifying cyber-physical specification mismatches.