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

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

我認(rèn)為：

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

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

我能想到的就是“可驗(yàn)證”。

“可驗(yàn)證”也是充分驗(yàn)證的前提。

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

M靜態(tài)驗(yàn)證

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

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

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

靜態(tài)檢查

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

形式化驗(yàn)證

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

M動(dòng)態(tài)驗(yàn)證

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

單元級(jí)功能測(cè)試

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

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

一需求覆蓋率，測(cè)試用例所覆蓋的需求比例；

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

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

集成級(jí)功能測(cè)試

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

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

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

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

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