在基于模型設(shè)計的開發(fā)過程中，一定要拿正確的模型去生成代碼。

有人要問：什么樣的模型才算得上正確的模型？

我認(rèn)為：

至少，正確的模型應(yīng)該是經(jīng)過充分驗證的。

除了“充分驗證”，還應(yīng)該滿足什么條件呢？

我能想到的就是“可驗證”。

“可驗證”也是充分驗證的前提。

模型的“可驗證”以后會專門介紹，本文就說說模型中代碼生成之前可以做哪些驗證。按照模型是否需要運(yùn)行來劃分，可以把驗證分為靜態(tài)驗證和動態(tài)驗證兩大類。

M靜態(tài)驗證

靜態(tài)驗證有評審、靜態(tài)檢查、形式化驗證等方式。

評審是質(zhì)量體系要求的

通常我們模型畫完之后，需要通過評審的方式去評審模型是否實現(xiàn)了相應(yīng)的需求。那么，評審發(fā)生的時刻應(yīng)該如何把握？是否在畫完模型之后緊跟著就去做評審呢？我個人認(rèn)為，如果有工具可以幫我們實現(xiàn)靜態(tài)檢查，我們?yōu)槭裁床幌茸鲮o態(tài)檢查呢？先做靜態(tài)檢查的好處是把可以通過工具發(fā)現(xiàn)的軟件缺陷在評審之前消除掉，這樣可以避免在評審的時候在此類問題上浪費(fèi)時間。

靜態(tài)檢查

目前MATLAB通過Simulink Verification & Validation（以下簡稱SLVnV）提供了Model Advisor，可以實現(xiàn)建模標(biāo)準(zhǔn)的靜態(tài)檢查，實現(xiàn)起來也不困難，并且工具還具有可定制功能，可以在SLVnV提供的諸多檢查項里挑選適合自己開發(fā)團(tuán)隊的檢查集，也有可能有一些檢查是Model Advisor沒有提供的，這種情況下，也可以通過編寫MATLAB程序的方式定制檢查項。

形式化驗證

MATLAB提供了Simulink Design Verifier（以下簡稱SLDV）產(chǎn)品，可以對模型進(jìn)行形式化驗證。SLDV可以檢查模型中是否有整數(shù)溢出，或者是否有死邏輯。這兩類錯誤都是很容易被評審和功能測試錯過的錯誤，其實，軟件里一旦發(fā)現(xiàn)有這兩類錯誤，復(fù)現(xiàn)或者定位這兩類錯誤都非常困難，而SLDV可以通過分析模型的給出發(fā)生或者可能發(fā)生錯誤的環(huán)節(jié)。另外，需要注意的是，在模型評審或者功能測試過程中，我們都可能發(fā)現(xiàn)一些軟件缺陷，發(fā)現(xiàn)這些缺陷之后，我們需要修改模型，模型經(jīng)過修改可能會再次引入數(shù)據(jù)溢出或者死邏輯之類的錯誤，所以建議做功能測試之后，再次使用SLDV檢查一下模型。

M動態(tài)驗證

動態(tài)驗證主要有功能測試。功能測試可以分為單元級功能測試和集成級功能測試兩個階段。如果系統(tǒng)比較大，集成級功能測試還會繼續(xù)劃分為組件級集成測試和系統(tǒng)級集成測試。

單元級功能測試

也就是我們經(jīng)常提到的單元測試，單元測試的測試用例需要用戶根據(jù)需求編寫，寫完測試用例就是執(zhí)行測試過程，測試過程的執(zhí)行要盡量自動化。這個階段的測試工作量非常大，通?；ㄔ趩卧獪y試上的時間會明顯大于建模的時間，這往往是很多開發(fā)者難以接受的，很多人從心理上沒有這個準(zhǔn)備，一般認(rèn)為模型畫完就接近大功告成，所以不會計劃很多時間在模型測試上，這個想法是非常危險的。當(dāng)然，這個階段的測試是否完善可以通過“測試覆蓋率”這個數(shù)據(jù)來把握。覆蓋率沒有達(dá)到預(yù)定的目標(biāo)就要繼續(xù)增加測試用例。

測試覆蓋率應(yīng)該從兩個層面去度量：

一需求覆蓋率，測試用例所覆蓋的需求比例；

一結(jié)構(gòu)覆蓋率，測試用例所覆蓋的軟件實現(xiàn)的分支。

對于工具，Simulink只能從結(jié)構(gòu)上度量哪些分支測過哪些分支沒測過，需求覆蓋率通常需要測試者自己去把握。對于結(jié)構(gòu)覆蓋率，我們有條件覆蓋（Condition Coverage）、判定覆蓋（Decision Coverage）、MC/DC覆蓋等。

集成級功能測試

集成測試的目的和單元測試是不同的，集成測試要求做單元測試結(jié)束之后才可以進(jìn)行。集成測試主要測試不同單元模塊之間從接口上、調(diào)度上是否有問題，有時候集成測試也可以發(fā)現(xiàn)不同單元模塊之間需求上的沖突。集成測試不會有結(jié)構(gòu)覆蓋率要求。

集成測試的實現(xiàn)方式有模型上的集成測試，也可能會結(jié)合硬件進(jìn)行測試，比如我們經(jīng)常提到的快速原型，是否要結(jié)合硬件要取決于是否有條件和是否有必要這樣做，這里不做展開。

到此，如果模型經(jīng)過了各種靜態(tài)驗證，再經(jīng)過足夠的動態(tài)驗證，我們可以認(rèn)為模型已經(jīng)正確了吧？

接下來，就可以對正確的模型進(jìn)行代碼生成工作了。

當(dāng)然，上述驗證活動都是建立在“模型可驗證”的基礎(chǔ)上的，模型的“可驗證”如何去把握，這我們后面再專門討論。