Test Automation/Model Checking

Model-based representations of cyber-physical systems are typically composed of sub-systems and components that are modelled in different formalisms. Discrete-event components may interact with continuous components in almost arbitrary ways.

This composition of a system model from components in varying formalisms poses some challenges for model-based testing and model checking, which are based on automated analysis of the underlying components. The solution to this problem, offered by Verified System's RT-Tester Model-Based Test Case Generator (RTT-MBT), is to abstract continuous behaviour using discrete-event abstractions which are expressed as state machines. The overall cyber-physical system is then represented as the composition of discrete-event components only. RTT-MBT automatically reasons about this net of components via SMT solving.

A key question to this approach is how the continuous model shall be abstracted to allow for proper reasoning about the system behaviour. RTT-MBT, as used in INTO-CPS, supports three different kinds of abstractions for continuous signals: based on intervals, based on the derivative of the signal values, and based on interval abstractions specifically generated from concrete simulations. Using this approach, both LTL model checking and test case generation can be performed for the kinds of models supported by INTO-CPS.