Using S-TaLiRo on industrial size automotive models

摘要: In Model Based Development (MBD) of embedded systems, it is often desirable to verify or falsify certain formal specifications. In some cases it is also desirable to find the range of specification parameters for which the specification does not hold on the system. We illustrate these methods on a challenge problem from the automotive industry on a high-fidelity, industrial scale engine model.