Scenario-Based Behavioral Nonexistent Consistency Checking for Cyber-Physical Systems

Cyber-Physical Systems (CPS) play an important role in the safety-critical systems. It is very significant to verify whether some concerned behaviors exist in a CPS. Hybrid interface automata, extension of a non-hybrid version, are used to model a CPS. A scenario, described by MARTE sequence diagram, specifies the concerned behaviors. An algorithm is given for bounded checking the behavioral nonexistent consistency, namely, the behaviors specified by a scenario all do not exist in a hybrid interface automaton. The idea of the algorithm is, firstly, encoding the behavioral nonexistent consistency to an unconstrained dynamic programming, secondly, solving the unconstrained dynamic programming by a genetic algorithm. The algorithm can search the results on the real domain, and be applied to nonlinear as well as linear hybrid systems.