  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.
