The MathWorks推出新產品Simulink設計驗證工具(Simulink Design Verfier)，這項新產品能夠搭配Prover Technology公司的Prover Plug-In技術，針對Simulink和Stateflow模型，進行測試並確保設計的正確性。The MathWorks台灣區總代理鈦思科技表示，使用Simulink設計驗證工具後，嵌入式系統的開發人員(尤其是複雜或攸關安全的系統)，能夠自動產生可滿足產業標準規範的測試實例，例如某些規範會要求的修改條件/判定覆蓋(MC/DC)等；同時，在開發過程之中，也能夠在早期研發階段就發現設計錯誤，以避免事後高昂的修改成本。

「模擬」是模型化基礎設計(Model-Base Design)過程中關鍵的一環，它可以讓工程師深入了解系統的行為、找出最佳表現的參數值，以及確保設計出來的結果和預先所想的相同。Simulink設計驗證工具採用最新以formal methods為基礎的測試與驗證技術，可大幅減少需以人工方式來建立所有模型和驗證的需求。工程師可自動產生符合覆蓋率目標或使用者自定目標的測試輸入(test inputs) ，所產生的測試輸入也可與量測到的資料作結合，因此可針對所有模型、規範和真實的情境進行模擬測試。為了把設計目標和模型測試做更緊密的結合，工程人員可直接在Simulink或Stateflow的模型裡把設計目標加入，Simulink設計驗證工具會利用數學方式證明設計是否符合這些設計目標，一旦不符標準，便提供和規範相抵觸的反例。結果就是，工程師可以更輕易的找出設計中的錯誤，以及和規範或設計目標相牴觸的部份，在以前，這些錯誤是很難用非系統的方式找到的。

The MathWorks的設計自動化行銷部執行長Paul Barnard表示：「巳經有愈來愈多的嵌入式系統利用模型化基礎設計來進行開發，一路從研發到原型化開發專案，再到產品量產階段。這一連串的步驟，極需驗證、有效性和測試工具的配合，而這些正是Simulink設計驗證工具可以勝任的部份。」

Simulink設計驗證工具和Prover Technology的Prover Plug-In proof engine相互搭配，能夠自動地產生測試實例和反例。同時，它也能利用自動的數學式合理法則，探討模型實現路徑，由此來證明設計特性。此類有系統的分析可以補充模擬上的不足，並深入了解系統的行為。