Global Sources
電子工程專輯
 
電子工程專輯 > EDA/IP
 
 
EDA/IP  

The Mathworks為嵌入式軟體增加形式設計方法

上網時間: 2007年08月15日     打印版  Bookmark and Share  字型大小:  

關鍵字:測試覆蓋率  Design Verifier  Stateflow 

為了在基於Simulink模型的設計套件中增加形式設計方法,The Mathworks公司推出了Simulink Design Verifier工具,這款工具可為該公司的Simulink模擬平台和Stateflow設計與模擬工具所提供的模型產生測試和驗證特性。

Design Verifier是以形式驗證供應商Prover Technology公司所提供的Prover Plug-In驗證引擎為基礎所開發的。The Mathworks公司在日前舉行的第44屆設計自動化會議(DAC)上展示了這款新工具。

The Mathworks公司決定在現有的設計軟體中增加形式方法,以便為強調安全性應用的設備開發人員提供足夠的測試覆蓋率,Mathworks公司訊號處理和通訊部門的行銷總監Ken Karnofsky表示。最初用戶將會是嵌入式軟體開發人員,Karnofsky指出,不過他相信,長期來看,這種功能對於硬體和軟體設計者而言也都具有很大的吸引力。

形式方法可協助設計者“測試並發現很難僅用模擬方式捕捉到的錯誤。”The Mathworks公司設計自動化部門行銷總監Paul Barnard介紹,“你可以耗盡心力地執行模擬來嘗試捕捉每種情況,但形式方法卻能夠更早期就專注於這些狀況。”因此,我們必須將形式方法與模擬整合在一起,Barnard指出。

Design Verifier的測試產生功能可以幫助工程師獲得測試案例,以支援安全性至關重要的業界標準度量參數,如改進的條件/判定覆蓋率。用戶可以在Simulink或Stateflow中使用設計驗證模組直接定義客製的測試目標。例如,用戶可以決定產生只提供100%判定覆蓋率的測試。

Design Verifier的屬性驗證功能可以幫助用戶發現諸如遺漏要求和意外狀態等問題。舉例來說,用戶可以確定無法實現的模型覆蓋,如無法進入、交換條件無法產生以及子系統不能執行等狀態。

用戶還可以將Simulink或Stateflow模型上的屬性定義為?真或?誤,Barnard表示。雖然從技術上而言複雜性是沒有極限的,但該工具規定用於“元件尺寸合理的”模型,而不適合於具有上千個模組的模型,Barnard指出。

成功和失敗

Design Verifier也提供一份報告顯示哪些屬性通過,哪些屬性未通過。對於無法過關的屬性,工具可以產生反例。

為了使用Design Verifier來產生測試,用戶要提供模型,並指明所需的覆蓋和測試目標。除了測試向量以外,Design Verifier還能產生測試套件,包括‘訊號建構’模組中的測試輸入值和期望輸出值。針對錯誤的屬性,Design Verifier也會產生相同類型的測試條件。

Design Verifier工具庫中的驗證子系統模組可以幫助用戶使用Simulink和Stateflow建構並定義複雜的驗證目標和限制條件,而不至於影響模擬進行。Design Verifier功能可以在Matlab環境中以批次模式進行解釋和執行。

The Mathworks公司的Simulink Design Verifier目前可在Windows和Linux平台上執行。

圖:Simulink採用形式驗證方法,Design Verifier適用於產生測試並驗證屬性。
圖:Simulink採用形式驗證方法,Design Verifier適用於產生測試並驗證屬性。

作者:葛立偉




投票數:   加入我的最愛
我來評論 - The Mathworks為嵌入式軟體增加形式設...
評論:  
*  您還能輸入[0]個字
*驗證碼:
 
論壇熱門主題 熱門下載
 •   將邁入40歲的你...存款多少了  •  深入電容觸控技術就從這個問題開始
 •  我有一個數位電源的專利...  •  磷酸鋰鐵電池一問
 •   關於設備商公司的工程師(廠商)薪資前景  •  計算諧振轉換器的同步整流MOSFET功耗損失
 •   Touch sensor & MEMS controller  •  針對智慧電表PLC通訊應用的線路驅動器
 •   下週 深圳 llC 2012 關於PCB免費工具的研討會  •  邏輯閘的應用


EE人生人氣排行
 
返回頁首