Using S-TaLiRo on Industrial Size Automotive Models
Bardh Hoxha, Houssam Abbas, Georgios Fainekos · EPiC series in computing · 2018
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.